-- An interface to construct Html data
-- (later: dedicated data type)
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE PatternGuards #-}
module Html
( code'
, showR
) where
import Memo
import JS
import Agda.Interaction.Response
import Agda.Interaction.Highlighting.Precise
import qualified Agda.Syntax.Concrete as C
import Agda.Syntax.Common
import Agda.Utils.Pretty (Doc, render, pretty)
import System.FilePath ((<.>))
import Data.List
import Data.Monoid
import Data.Function
import qualified Data.Map as Map
---------------------------------------------------------------
-- | Constructs the HTML displaying the code.
code'
:: (AreaID -> ResID -> Stmt ())
-> AgdaCode -- ^ The contents of the module.
-> CompressedFile -- ^ Highlighting information.
-> Memo Html
code' giveCode (unAgdaCode -> contents) info
= fmap mconcat
. mapM (\cs -> case cs of
(mi, (pos, _)) : _ -> annotate pos (maybe mempty id mi) (map (snd . snd) cs)
[] -> error "__IMPOSSIBLE__"
)
. groupBy ((==) `on` fst)
. map (\(pos, c) -> (Map.lookup pos infoMap, (pos, c)))
. zip [1..]
$ contents
where
infoMap = toMap (decompress info)
getHole "?" = Just ""
getHole ('{':'!':cs)
| ('}':'!':cs') <- reverse cs
= Just $ reverse cs'
getHole _ = Nothing
annotate :: Integer -> MetaInfo -> String -> Memo Html
annotate pos mi s
| Just h <- getHole s -- = stringToHtml "HOLE"
= do
(i2, thediv_) <- thediv'
(i1, tar) <- textarea' 30 1
return $
thediv_ [] <<
[ tar [] << h
, br
, button' "Give" (giveCode i1 i2)
]
{-
! [ theclass "interpreter"
, thetype "text"
, size $ show $ 3 + length h -- limit
, maxlength 1000
-- , identifier $ "tarea" ++ i
, value h -- $ if prompt == 'R' then "" else exp
]
-}
annotate pos mi s
= return $ anchor ! attributes << stringToHtml s
where
attributes
= [name (show pos)]
++ maybe [] link (definitionSite mi)
++ (case classes of
[] -> []
cs -> [theclass $ unwords cs])
classes
= maybe [] noteClasses (note mi)
++ otherAspectClasses (otherAspects mi)
++ maybe [] aspectClasses (aspect mi)
aspectClasses (Name mKind op) = kindClass ++ opClass
where
kindClass = maybe [] ((: []) . showKind) mKind
showKind (Constructor Inductive) = "InductiveConstructor"
showKind (Constructor CoInductive) = "CoinductiveConstructor"
showKind k = show k
opClass = if op then ["Operator"] else []
aspectClasses a = [show a]
otherAspectClasses = map show
-- Notes are not included.
noteClasses s = []
link (m, pos) = [href $ modToFile m ++ "#" ++ show pos]
where
modToFile :: C.TopLevelModuleName -> FilePath
modToFile m = render (pretty m) <.> "xml"
---------------------------------------------------------------
{-
instance IsString Html where
fromString = toHtml :: String -> Html
-}
showR :: Response -> Maybe Html
showR (Resp_Status s) = Just $ ("checked: " :: String) +++ show (sChecked s)
showR (Resp_DisplayInfo x) = Just $ showD x --a ++ " :displayinfo: " ++ b
showR (Resp_RunningInfo i x) = Just $ "runninginfo: " +++ show i +++ x
showR Resp_ClearRunningInfo = Just $ toHtml "clearRunningInfo"
--showR (Resp_HighlightingInfo h) = "highlightingInfo: " ++ show h
--showR (Resp_UpdateHighlighting (a,b)) = "highlighting: " ++ show (a,b)
showR (Resp_JumpToError f i) = Just $ "jumpToError" +++ f +++ show i
showR (Resp_InteractionPoints is) = Just $ "ipoints: " +++ show is
showR (Resp_GiveAction i s) = Just $ "give: " +++ show i +++ showG s
showR (Resp_MakeCaseAction ss) = Just $ "caseaction: " +++ ss
showR (Resp_MakeCase s ss) = Just $ "case: " +++ s +++ ss
showR (Resp_SolveAll x) = Just $ "solveAll: " +++ show x
showR _ = Nothing
instance HTML Doc where
toHtml = toHtml . render
showG :: GiveResult -> Html
showG (Give_String s) = toHtml s
showG Give_Paren = toHtml "give paren"
showG Give_NoParen = toHtml "give no paren"
showD :: DisplayInfo -> Html
showD x = case x of
Info_CompilationOk -> toHtml "compilation ok"
Info_Constraints s -> "constraints:" +++ s
Info_AllGoals s -> "all goals:" +++ s
Info_Error s -> "error:" +++ s
Info_Intro d -> "intro:" +++ d
Info_Auto s -> "auto:" +++ s
Info_ModuleContents d -> "module contents:" +++ d
Info_NormalForm d -> "normal form:" +++ d
Info_GoalType d -> "goal type:" +++ d
Info_CurrentGoal d -> "current goal:" +++ d
Info_InferredType d -> "inferred type:" +++ d
Info_Context d -> "context:" +++ d