mostly css files and restructuring output

Compile.hs

@@ -8,7 +8,9 @@ import Control.Applicative
 import Data.Monoid
 
 import Types
--- This is gonna be some ugly-ass HTML. Sorry Jesus.
+
+-- Consider allowing trailing commas or removing commas altogether
+-- as there's really no need for them.
 
 indent :: Int -> T.Text -> T.Text
 indent n = T.unlines . map (T.replicate (2 * n) " " <>) . T.lines
@@ -28,9 +30,14 @@ tag' tagName children =
 div :: T.Text -> [T.Text] -> T.Text
 div = tag "div"
 
+paragraph :: T.Text -> T.Text
+paragraph = tag' "p" . pure
+
 compileComment :: Comment -> T.Text
 compileComment (Comment mayName comm) =
-  div "comment" (maybe id ((:) . T.pack) mayName [T.pack comm])
+  div "comment"
+    (maybe id ((:) . div "name" . pure . T.pack) mayName
+      [div "node-content" [paragraph $ T.pack comm]])
 
 compileTheoremStatement :: TheoremStatement -> T.Text
 compileTheoremStatement (AssumeProve assumps results) =
@@ -46,7 +53,7 @@ maybeToList = maybe [] pure
 compileSuchThat :: SuchThat -> T.Text
 compileSuchThat (SuchThat conds mayProof) =
   div "suchthat"
-    (div "conditions" (map compileMaybeJustified conds)
+    (ul "conditions" (map compileMaybeJustified conds)
     : maybeToList ((div "justification" . pure . compileProof) <$> mayProof))
 
     {-
@@ -57,14 +64,18 @@ compileSuchThat (SuchThat conds mayProof) =
       (div "statement" [T.pack cond] :
         maybeToList (compileProof <$> mayLocalProof))
 -}
+
+ul = tag "ul"
+li = tag "li"
+
 compileBinder name bindings suchThat =
   div name (
-    div "bindings" (map (div "binding" . pure . T.pack) bindings) :
-    maybe [] (pure . compileSuchThat) suchThat
+    ul "bindings" (map (li "binding" . pure . T.pack) bindings) :
+    maybeToList (compileSuchThat <$> suchThat)
   )
 
 compileMaybeJustified (stmt, mayJustification) =
-  div "list-item"
+  li "list-item"
     (div "statement" [T.pack stmt] :
      maybeToList (compileProof <$> mayJustification))
 
@@ -75,7 +86,7 @@ compileStep (Cases cases) = div "cases" (map compileCase cases) where
 
 compileStep (Let bindings suchThat)  =
   div "let" (
-    div "bindings" (map compileMaybeJustified bindings)
+    ul "bindings" (map compileMaybeJustified bindings)
     : maybeToList (compileSuchThat <$> suchThat))
 
 compileStep (Take bindings suchThat) = compileBinder "take" bindings suchThat
@@ -85,10 +96,11 @@ compileStep (Claim stmt proof)       =
 
 compileStep (Suppose assumps results mayProof) =
   div "suppose" (
-    div "assumptions" (map (div "list-item" . pure . T.pack) assumps)
-    : div "results" (map (div "list-item" . pure . T.pack) results)
+    ul "assumptions" (map (li "list-item" . pure . T.pack) assumps)
+    : ul "results" (map (li "list-item" . pure . T.pack) results)
     : maybeToList (compileProof <$> mayProof))
-
+
+compileStep (CommentStep comment) = compileComment comment
 
 compileProof :: Proof -> T.Text
 compileProof (Simple proof) = div "proof simple-proof" [T.pack proof]
@@ -107,13 +119,35 @@ compileDecl (Macros macros) =
 
 compileDecl (Definition name clauses) =
   div "definition"
-    (div "name" [T.pack name] : map (either T.pack compileComment) clauses)
+    [ div "name" [T.pack name] 
+    , div "node-content" (map (either T.pack compileComment) clauses)
+    ]
 
 compile :: Document -> T.Text
 compile doc = tag' "html" [
-    tag' "head" [],
+    tag' "head" headContent,
     tag' "body" [
       T.intercalate "\n" $ map compileDecl doc
     ]
   ]
+  where
+  css href = "<link rel='stylesheet' type='text/css' href='" <> href <> "'>"
+  headContent =
+    [ css "proof.css"
+    , css "static/fonts/latinmodernroman_10regular_macroman/stylesheet.css"
+    , css "static/fonts/latinmodernroman_10bold_macroman/stylesheet.css"
+    , css "static/fonts/latinmodernroman_10italic_macroman/stylesheet.css"
+    , css "static/fonts/latinmodernromancaps_10regular_macroman/stylesheet.css"
+    , css "static/fonts/latinmodernromancaps_10regular_macroman/stylesheet.css"
+    , css "static/fonts/latinmodernromandemi_10regular_macroman/stylesheet.css"
+    , css "static/fonts/latinmodernromandemi_10oblique_macroman/stylesheet.css"
+    , "<script src='jquery.min.js'></script>"
+    , "<script type='text/javascript' src='http://cdn.mathjax.org/mathjax/latest/MathJax.js?config=TeX-AMS-MML_HTMLorMML'></script>"
+    , "<script type='text/x-mathjax-config'>"
+    , "  MathJax.Hub.Config({"
+    , "    tex2jax: {inlineMath: [['$','$'], ['\\\\(','\\\\)']]}"
+    , "  });"
+    , "</script>"
+    , "<script type='text/javascript' src='proof.js'></script>"
+    ]
 

Parse.hs

@@ -7,11 +7,22 @@ import Control.Monad
 import Prelude hiding (take)
 import Control.Applicative hiding (many, (<|>))
 
+import Data.Char (isSpace)
+
 type Parser a = forall s m u. (Stream s m Char) => ParsecT s u m a
 
+-- TODO: Make macros
+
 symbol :: String -> Parser String
 symbol s = string s <* spaces
 
+lineComment = do
+  try (char '%')
+  skipMany (satisfy (/= '\n'))
+
+whiteSpace = skipMany (simpleSpace <|> lineComment) where
+  simpleSpace = skipMany1 (satisfy isSpace) 
+
 literalText :: Parser String
 literalText = do
   string "[|"
@@ -21,23 +32,24 @@ comment :: Parser Comment
 comment = do
   symbol "comment"
   text1 <- literalText
+  whiteSpace
   text2 <- optionMaybe literalText 
   let (name, comm) = maybe (Nothing, text1) (\t2 -> (Just text1, t2)) text2 
   return $ Comment name comm
 
-listOf p = between (symbol "[") (symbol "]") ((p <* spaces) `sepBy` symbol ",")
+listOf p = between (symbol "[" *> whiteSpace) (symbol "]") ((p <* whiteSpace) `sepBy` symbol ",")
 
 definition :: Parser Declaration
 definition = do
   symbol "definition"
-  Definition <$> (literalText <* spaces)
+  Definition <$> (literalText <* whiteSpace)
              <*> listOf (fmap Left literalText <|> fmap Right comment)
 
 assumeProve :: Parser TheoremStatement
 assumeProve = do
   symbol "assume"
   assumptions <- listOf literalText
-  spaces
+  whiteSpace
   symbol "prove"
   results <- listOf literalText
   return (AssumeProve assumptions results)
@@ -47,7 +59,7 @@ theoremStatement = assumeProve
 
 maybeJustified :: Parser (MaybeJustified String)
 maybeJustified =
-  (,) <$> (literalText <* spaces)
+  (,) <$> (literalText <* whiteSpace)
       <*> optionMaybe (symbol "because" *> proof)
 
 suchThat :: Parser SuchThat
@@ -74,37 +86,37 @@ cases = do
   where
   oneCase = do
     symbol "case"
-    (,) <$> (literalText <* spaces) <*> proof
+    (,) <$> (literalText <* whiteSpace) <*> proof
 
 claim :: Parser Step
 claim = do
   symbol "claim"
-  Claim <$> (literalText <* spaces) <*> (optionMaybe proof)
+  Claim <$> (literalText <* whiteSpace) <*> (optionMaybe proof)
 
 suppose :: Parser Step
 suppose = do
   symbol "suppose"
   assumps <- listOf literalText
   symbol "then"
   results <- listOf literalText
-  spaces
+  whiteSpace
   Suppose assumps results <$> optionMaybe (symbol "because" *> proof)
 
 step :: Parser Step
-step = let_ <|> suppose <|> take <|> try cases <|> claim
+step = let_ <|> suppose <|> take <|> try (CommentStep <$> comment) <|> try claim <|> cases
 
 proof :: Parser Proof
 proof = try (fmap Simple literalText) <|> fmap Steps (listOf step)
 
 theorem :: Parser Declaration
 theorem = do
   symbol "theorem"
-  Theorem <$> (literalText <* spaces) <*> (theoremStatement <* spaces) <*> proof
+  Theorem <$> (literalText <* whiteSpace) <*> (theoremStatement <* whiteSpace) <*> proof
 
 macros = do
   symbol "macros"
   Macros <$> literalText
 
 document :: Parser [Declaration]
-document = (macros <|> theorem <|> definition) `sepBy` spaces
+document = (macros <|> theorem <|> definition) `sepBy` whiteSpace
 

Types.hs

@@ -26,6 +26,7 @@ data Step
   | Suppose [Text] [Text] (Maybe Proof)
   | Take [Text] (Maybe SuchThat)
   | Claim Statement (Maybe Proof)
+  | CommentStep Comment
   deriving Show
 
 data Declaration

vim/syntax/proof.vim

@@ -11,7 +11,11 @@ syn case match
 
 " Keywords
 syn keyword proofKeywords theorem definition claim cases let take assume prove macros comment because suppose then
+syn keyword proofListitem case
+
+" Matches
 syn match proofKeywords /such that/
+syn match	proofLineComment +^[ \t:]*%.*$+
 
 syn include @LATEX syntax/tex.vim
 syn region proofTexBlock start="\v\[\|" end="\v\|\]" keepend contains=@LATEX
@@ -20,5 +24,6 @@ syn region proofTexBlock start="\v\[\|" end="\v\|\]" keepend contains=@LATEX
 let b:current_syntax = "proof"
 
 hi def link proofKeywords Constant
-
+hi def link proofListitem Statement
+hi def link proofLineComment Comment