{- |
Module : Web.Hamlet
Description : Hamlet templates.
Copyright : (c) 2011 Cedric Staub
License : GPL-3
Maintainer : Cedric Staub <cstaub@ethz.ch>
Stability : experimental
Portability : non-portable
-}
{-# LANGUAGE
TypeFamilies, QuasiQuotes, TypeSynonymInstances,
PatternGuards, FlexibleInstances, CPP #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
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 Text.Blaze.Html (preEscapedToMarkup)
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
<div class="ui-layout-container">
<div class="ui-layout-north">
<div class="ui-layout-pane">
<div class="layout-pane-north">
<div class="ui-layout-pane-north">
<div id="introbar">
<div id="header-info">
Running
\ <a href=@{RootR}><span class="tamarin">Tamarin</span></a>
\ #{showVersion version}
\^{introTpl}
<div class="intropage">
<p>
\^{theoriesTpl theories}
<h2>Loading a new theory
<p>
You can load a new theory file from disk in order to work with it.
<form class=root-form enctype="multipart/form-data" action=@{RootR} method=POST>
Filename:
<input type=file name="uploadedTheory">
<div .submit-form>
<input type=submit value="Load new theory">
<p>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
<strong>No theories loaded!</strong>
$else
<table>
<thead>
<th>Theory name
<th>Time
<th>Version
<th>Origin
$forall tgroup <- processMap thmap
^{theoryTpl (head tgroup)}
$forall th <- ntail 4 tgroup
^{theoryTpl th}
<br>
|]
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
<tr>
<td>
<a href=@{OverviewR (fst th) TheoryHelp}>
\#{get thyName $ tiTheory $ snd th}
<td>#{formatTime defaultTimeLocale "%T" $ tiTime $ snd th}
$if tiPrimary (snd th)
<td>Original
$else
<td><em>Modified
<td>#{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
<h2>Threads
<p>
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
<strong>No threads registered!</strong>
$else
<table>
<thead>
<th>Request path
<th>Kill?
$forall th <- threads
<tr>
<td>#{th}
<td><a href="@{KillThreadR}?path=#{th}">Kill</a>
|]
-}
-- | Template for header frame (various information)
headerTpl :: TheoryInfo -> Widget
headerTpl info = [whamlet|
$newline never
<div class="layout-pane-north">
<div #header-info>
Running
\ <a href=@{RootR}><span class="tamarin">Tamarin</span></a>
\ #{showVersion version}
<div #header-links>
<a class=plain-link href=@{RootR}>Index</a>
<a class=plain-link href=@{DownloadTheoryR idx filename}>Download</a>
<ul #navigation>
<li><a href="#">Actions</a>
<ul>
<li><a target=_blank href=@{TheorySourceR idx}>Show source</a>
<li><a href="#">Options</a>
<ul>
<li><a id=graph-toggle href="#">Compact graphs</a>
<li><a id=seqnt-toggle href="#">Compress sequents</a>
|]
where
-- <li><a id=debug-toggle href="#">Debug pane</a>
-- <li><a href=@{TheoryVariantsR idx}>Show variants</a>
-- <li><a class=edit-link href=@{EditTheoryR idx}>Edit theory</a>
-- <li><a class=edit-link href=@{EditPathR idx (TheoryLemma "")}>Add lemma</a>
--
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)
<a class=save-link href=@{SaveTheoryR idx}>Save</a>
-}
-- | 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
<div .ui-layout-north>
^{headerTpl info}
<div .ui-layout-west>
<h1 .pane-head>Proof scripts
<div #proof-wrapper .scroll-wrapper>
<div #proof .monospace>
^{proofState}
<div .ui-layout-east>
<h1 .pane-head> Debug information
<div #debug-wrapper .scroll-wrapper>
<div #ui-debug-display>
<div .ui-layout-center>
<h1 #main-title .pane-head>Visualization display
<div #main-wrapper .scroll-wrapper tabindex=0>
<div #ui-main-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
<div id="logo">
<p>
<img src="/static/img/tamarin-logo-3-0-0.png">
<noscript>
<div class="warning">
Warning: JavaScript must be enabled for the <span class="tamarin">Tamarin</span> prover GUI to function properly.
<div class="intropage">
<p>
Authors:
\ <a href="http://people.inf.ethz.ch/meiersi">Simon Meier</a>,
\ <a href="https://www1.ethz.ch/infsec/people/benschmi">Benedikt Schmidt</a><br>
Contributors:
\ <a href="http://people.inf.ethz.ch/cremersc/index.html">Cas Cremers</a>,
\ <a href="http://cssx.ch">Cedric Staub</a>
<p>
<span class="tamarin">Tamarin</span> was developed at the
\ <a href="http://www.infsec.ethz.ch">Information Security Institute</a>,
\ <a href="http://www.ethz.ch">ETH Zurich</a>.
\ This program comes with ABSOLUTELY NO WARRANTY. It is free software, and
\ you are welcome to redistribute it according to its
\ <a href="/static/LICENSE" type="text/plain">LICENSE.</a>
<p>
More information about Tamarin and technical papers describing the underlying
\ theory can be found on the
\ <a href="http://www.infsec.ethz.ch/research/software/tamarin"><span class="tamarin">Tamarin</span>
\ webpage</a>.
|]
{-
-- | 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 = [whamlet|
$newline never
<form action=@{action} method=POST enctype=#{enctype}>
^{form}
<div .submit-form>
^{addHtml nonce}
<input type=submit value=#{label}>
<input type=button id=cancel-form value=Cancel>
|]
-}