{- | Module : Web.Hamlet Description : Hamlet templates. Copyright : (c) 2011 Cedric Staub License : GPL-3 Maintainer : Cedric Staub Stability : experimental Portability : non-portable -} {-# LANGUAGE TypeFamilies, QuasiQuotes, TypeSynonymInstances, PatternGuards, FlexibleInstances, CPP #-} {-# OPTIONS_GHC -fno-warn-orphans #-} module Web.Hamlet ( rootTpl , overviewTpl ) where import Theory import Web.Types import Web.Theory import Data.Label import Text.PrettyPrint.Html import Yesod.Core -- import Yesod.Form -- import Text.Hamlet import Control.Monad.IO.Class (liftIO) import Data.Ord import Data.List import Data.Time.Format import Data.Version (showVersion) import qualified Data.Map as M -- import qualified Data.Text as T import Text.Blaze.Html5 (preEscapedString) -- import Control.Monad.RWS (runRWST) import qualified Control.Exception as E import System.Locale import Paths_tamarin_prover (version) -- Quasi-quotation syntax changed from GHC 6 to 7, -- so we need this switch in order to support both #if __GLASGOW_HASKELL__ >= 700 #define HAMLET whamlet #else #define HAMLET $whamlet #endif -- -- Wrappers -- -- | Wrapper for @HtmlDoc@ values. wrapHtmlDoc :: HtmlDoc Doc -> Widget wrapHtmlDoc doc | null res = exceptionTpl err | otherwise = [HAMLET|#{preEscapedString res}|] where res = renderHtmlDoc doc err = "Trying to render document yielded empty string. This is a bug." -- | Run a ThHtml value, catch exceptions. wrapThHtml :: HtmlDoc Doc -> IO Widget wrapThHtml th = E.catch (return $ wrapHtmlDoc th) handleEx where -- handleEx :: HamletValue h => E.SomeException -> IO h handleEx :: E.SomeException -> IO Widget handleEx e = do putStrLn "----------------" putStrLn "Caught exception" putStrLn "----------------" print e return (exceptionTpl (show e)) -- -- Templates -- -- | Exception/error template. exceptionTpl :: String -> Widget exceptionTpl err = [HAMLET|

Caught exception! \#{err} |] {- -- | Simple template for serving sites which are loaded through -- AJAX instead of a normal request (no html/head/body tags). -- -- Note: Don't use ajaxLayout and defaultLayout together, use -- only one or the other. -- ajaxLayout :: Monad m => GenericWidget m () -> GenericHandler m RepHtml ajaxLayout w = error "ajaxLayout" $ fmap fst $ unGWidget w -- do -- (body, _, _) <- runRWST (unGWidget $ extractBody w) () 0 -- (body, _, _) <- unGWidget $ w -- () 0 -- hamletToRepHtml [HAMLET|^{body}|] -} -- | Template for root/welcome page. rootTpl :: TheoryMap -- ^ Map of loaded theories -> Widget -- rootTpl theories form enctype nonce = [whamlet| rootTpl theories = [whamlet|
Running \ Tamarin \ #{showVersion version} \^{introTpl}

\^{theoriesTpl theories}

Loading a new theory

Filename:

Note: You can save a theory by downloading the source. |] -- | Template for listing theories. theoriesTpl :: TheoryMap -> Widget theoriesTpl thmap = [whamlet| $if M.null thmap No theories loaded! $else
Theory name Time Version Origin $forall tgroup <- processMap thmap ^{theoryTpl (head tgroup)} $forall th <- ntail 4 tgroup ^{theoryTpl th}
|] where processMap = groupBy (\x y -> comparing tiName x y == EQ) . sortBy (comparing snd) . M.toList tiName = get thyName . tiTheory . snd ntail _ [] = [] ntail i (_:xs) | length xs <= i = xs | otherwise = ntail i xs -- | Template for single line in table on root page. theoryTpl :: (TheoryIdx, TheoryInfo) -> Widget theoryTpl th = [HAMLET|
\#{get thyName $ tiTheory $ snd th} #{formatTime defaultTimeLocale "%T" $ tiTime $ snd th} $if tiPrimary (snd th) Original $else Modified #{origin th} |] where origin (_, ti) = case tiOrigin ti of Local path -> path Upload name -> name Interactive -> "(interactively created)" -- | Template for listing threads. -- threadsTpl :: (HamletValue h, HamletUrl h ~ WebUIRoute) => [T.Text] -> h {- threadsTpl threads = [HAMLET|

Threads

This page lists all threads that are currently registered as \ evaluating a request within the server. This is meant for debugging \ lockups within the server. $if null threads No threads registered! $else
Request path Kill? $forall th <- threads
#{th} Kill |] -} -- | Template for header frame (various information) headerTpl :: TheoryInfo -> Widget headerTpl info = [HAMLET|
Running \ Tamarin \ #{showVersion version}
Index Download
  • Actions
    • Show source
    • Options
      • Compact graphs
      • Compress sequents |] where --
      • Debug pane --
      • Show variants --
      • Edit theory --
      • Add lemma -- idx = tiIndex info filename = get thyName (tiTheory info) ++ ".spthy" {- use this snipped to reactivate saving local theories localTheory (Local _) = True localTheory _ = False $if localTheory (tiOrigin info) Save -} -- | Template for proof state (tree) frame. proofStateTpl :: RenderUrl -> TheoryInfo -> IO Widget proofStateTpl renderUrl ti = wrapThHtml $ theoryIndex renderUrl (tiIndex ti) (tiTheory ti) -- | Framing/UI-layout template (based on JavaScript/JQuery) overviewTpl :: RenderUrl -> TheoryInfo -- ^ Theory information -> TheoryPath -- ^ Theory path to load into main -> IO Widget overviewTpl renderUrl info path = do proofState <- proofStateTpl renderUrl info mainView <- pathTpl renderUrl info path return [HAMLET|
        ^{headerTpl info}

        Proof scripts
        ^{proofState}

         Debug information

        Visualization display
        \^{mainView} |] -- | Theory path, displayed when loading main screen for first time. pathTpl :: RenderUrl -> TheoryInfo -- ^ The theory -> TheoryPath -- ^ Path to display on load -> IO Widget pathTpl _ info TheoryHelp = return [whamlet|

        Theory information

          Theory: #{get thyName $ tiTheory info}
        • Loaded at #{formatTime defaultTimeLocale "%T" $ tiTime info}
        • Origin: #{show $ tiOrigin info}

          Quick introduction