{- | 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 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 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 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 hamlet #else #define HAMLET $hamlet #endif -- -- Wrappers -- -- | Wrapper for @HtmlDoc@ values. wrapHtmlDoc :: HamletValue h => HtmlDoc Doc -> h 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 :: HamletValue h => HtmlDoc Doc -> IO h wrapThHtml th = E.catch (return $ wrapHtmlDoc th) handleEx where handleEx :: HamletValue h => E.SomeException -> IO h handleEx e = do putStrLn "----------------" putStrLn "Caught exception" putStrLn "----------------" print e return (exceptionTpl (show e)) -- -- Templates -- -- | Exception/error template. exceptionTpl :: HamletValue h => String -> h 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 = do (body, _, _) <- runRWST (unGWidget $ extractBody w) () 0 hamletToRepHtml [HAMLET|^{body}|] -- | Template for root/welcome page. rootTpl :: (HamletValue h, HamletUrl h ~ WebUIRoute, h ~ Widget ()) => TheoryMap -- ^ Map of loaded theories -> Widget () -- ^ Form widget (for loading new theories) -> Enctype -- ^ Form encoding type (for form) -> Html -- ^ Nonce field (for form) -> h rootTpl theories form enctype nonce = [HAMLET| \^{introTpl}

Currently loaded theories

\^{theoriesTpl theories}

Loading a new theory

^{form}

^{addHtml nonce}

Note: You can save a theory by downloading the source. |] -- | Template for listing theories. theoriesTpl :: (HamletValue h, HamletUrl h ~ WebUIRoute) => TheoryMap -> h theoriesTpl thmap = [HAMLET| $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 :: (HamletValue h, HamletUrl h ~ WebUIRoute) => (TheoryIdx, TheoryInfo) -> h 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 :: (HamletValue h, HamletUrl h ~ WebUIRoute) => TheoryInfo -- ^ Theory information -> h headerTpl info = [HAMLET|
Running \ tamarin prover \ #{showVersion version}
Index Download
  • Actions
    • Show source
    • Show variants
    • Edit theory
    • Add lemma
    • Options
      • Compact graphs
      • Compress sequents
      • Debug pane |] where 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 :: (HamletValue h, HamletUrl h ~ WebUIRoute) => TheoryInfo -- ^ Theory information -> IO h proofStateTpl = wrapThHtml . theoryIndex . tiTheory -- | Framing/UI-layout template (based on JavaScript/JQuery) overviewTpl :: (HamletValue h, HamletUrl h ~ WebUIRoute) => TheoryInfo -- ^ Theory information -> TheoryPath -- ^ Theory path to load into main -> IO h overviewTpl info path = do proofState <- proofStateTpl info mainView <- pathTpl 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 :: (HamletValue h, HamletUrl h ~ WebUIRoute) => TheoryInfo -- ^ The theory -> TheoryPath -- ^ Path to display on load -> IO h pathTpl info TheoryMain = return [HAMLET|

        Welcome!


        Theory information

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

          Quick introduction

          Left pane: Proof scripts display. You \ can select proof states and examine them further \ by clicking on them!

          Center pane: Visualization and \ information display relating to the currently \ selected item.

          Keyboard shortcuts: The interactive interface supports \ multiple keyboard shortcuts for convenience.

          • Keys j and k: Jump to the next/previous \ proof path within the currently focused lemma.
          • Keys J and K: Jump to the next/previous \ open goal within the currently focused lemma, or to the \ next/previous lemma if there are no more open goals in the current \ lemma.
          • Keys 1 to 9: Apply the proof method with \ the given number as shown in the applicable proof method section \ in the main view. |] pathTpl info path = wrapThHtml $ htmlThyPath (tiTheory info) path -- | Template for introduction. introTpl :: (HamletValue h, HamletUrl h ~ WebUIRoute) => h introTpl = [HAMLET|

            Welcome!

            About

            You are running the\ tamarin prover \ version #{showVersion version} in interactive mode.
            \ © 2010 - 2012 \ Benedikt Schmidt , Simon Meier , Cedric Staub , Information Security Institute , ETH Zurich

            This program comes with ABSOLUTELY NO WARRANTY. It is free software, and \ you are welcome to redistribute it according to its \ LICENSE. |] -- | Template for editing a theory. formTpl :: (HamletValue h, HamletUrl h ~ WebUIRoute, h ~ Widget ()) => WebUIRoute -- ^ Form action route -> String -- ^ Submit button label -> Widget () -- ^ Form widget -> Enctype -- ^ Form encoding type -> Html -- ^ Nonce field -> h formTpl action label form enctype nonce = [HAMLET|

            ^{form}
            ^{addHtml nonce} |]