{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE PatternGuards #-} {-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeSynonymInstances #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {- | Module : Web.Hamlet Description : Hamlet templates. Copyright : (c) 2011 Cedric Staub License : GPL-3 Maintainer : Cedric Staub Stability : experimental Portability : non-portable -} module Web.Hamlet ( rootTpl , overviewTpl ) where import Data.Label import Text.PrettyPrint.Html import Theory import Web.Theory import Web.Types import Yesod.Core import Data.List import qualified Data.Map as M import Data.Ord import Data.Time.Format import Data.Version (showVersion) import System.Locale import Paths_tamarin_prover (version) -- -- Templates -- {- -- | 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 [whamlet|^{body}|] -} -- | Template for root/welcome page. rootTpl :: TheoryMap -- ^ Map of loaded theories -> Widget -- rootTpl theories form enctype nonce = [whamlet| rootTpl theories = [whamlet| $newline never
Running \ Tamarin \ #{showVersion version} \^{introTpl}

\^{theoriesTpl theories}

Loading a new theory

You can load a new theory file from disk in order to work with it.

Filename:

Note: You can save a theory by downloading the source. |] -- | Template for listing theories. theoriesTpl :: TheoryMap -> Widget theoriesTpl thmap = [whamlet| $newline never $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 = [whamlet| $newline never
\#{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 = [whamlet| $newline never

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 = [whamlet| $newline never
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 = do let res = renderHtmlDoc $ theoryIndex renderUrl (tiIndex ti) (tiTheory ti) return [whamlet| $newline never #{preEscapedToMarkup res} |] -- | 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 [whamlet| $newline never
        ^{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 renderUrl info path = return $ [whamlet| $newline never #{htmlThyPath renderUrl info path} |] -- | Template for introduction. introTpl :: Widget introTpl = [whamlet| $newline never