fix: HTML and parser

src/leanblog/LeanDoc/Genre/Blog.lean

@@ -18,23 +18,23 @@ open LeanDoc Doc Elab
 
 @[role_expander htmlSpan]
 def htmlSpan : RoleExpander
-  | #[.named `«class» (.string classes)], stxs => do
+  | #[.named `«class» (.str classes)], stxs => do
     let args ← stxs.mapM elabInline
     let val ← ``(Inline.other (Blog.InlineExt.htmlSpan $(quote classes)) #[ $[ $args ],* ])
     pure #[val]
   | _, _ => throwUnsupportedSyntax
 
 @[directive_expander htmlDiv]
 def htmlDiv : DirectiveExpander
-  | #[.named `«class» (.string classes)], stxs => do
+  | #[.named `«class» (.str classes)], stxs => do
     let args ← stxs.mapM elabBlock
     let val ← ``(Block.other (Blog.BlockExt.htmlDiv $(quote classes)) #[ $[ $args ],* ])
     pure #[val]
   | _, _ => throwUnsupportedSyntax
 
 @[directive_expander blob]
 def blob : DirectiveExpander
-  | #[.anonymous (.name blobName)], stxs => do
+  | #[.anon (.name blobName)], stxs => do
     if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents"
     let actualName ← resolveGlobalConstNoOverloadWithInfo blobName
     let val ← ``(Block.other (Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
@@ -43,7 +43,7 @@ def blob : DirectiveExpander
 
 @[role_expander blob]
 def inlineBlob : RoleExpander
-  | #[.anonymous (.name blobName)], stxs => do
+  | #[.anon (.name blobName)], stxs => do
     if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents"
     let actualName ← resolveGlobalConstNoOverloadWithInfo blobName
     let val ← ``(Inline.other (Blog.InlineExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
@@ -52,15 +52,15 @@ def inlineBlob : RoleExpander
 
 @[role_expander label]
 def label : RoleExpander
-  | #[.anonymous (.name l)], stxs => do
+  | #[.anon (.name l)], stxs => do
     let args ← stxs.mapM elabInline
     let val ← ``(Inline.other (Blog.InlineExt.label $(quote l.getId)) #[ $[ $args ],* ])
     pure #[val]
   | _, _ => throwUnsupportedSyntax
 
 @[role_expander ref]
 def ref : RoleExpander
-  | #[.anonymous (.name l)], stxs => do
+  | #[.anon (.name l)], stxs => do
     let args ← stxs.mapM elabInline
     let val ← ``(Inline.other (Blog.InlineExt.ref $(quote l.getId)) #[ $[ $args ],* ])
     pure #[val]
@@ -69,7 +69,7 @@ def ref : RoleExpander
 
 @[role_expander page_link]
 def page_link : RoleExpander
-  | #[.anonymous (.name page)], stxs => do
+  | #[.anon (.name page)], stxs => do
     let args ← stxs.mapM elabInline
     let pageName := mkIdentFrom page <| docName page.getId
     let val ← ``(Inline.other (Blog.InlineExt.pageref $(quote pageName.getId)) #[ $[ $args ],* ])
@@ -109,7 +109,7 @@ structure LeanBlockConfig where
   name : Option Name := none
   error : Option Bool := none
 
-def takeNamed (name : Name) (args : Array RoleArgument) : Array Doc.Elab.RoleArgumentValue × Array RoleArgument := Id.run do
+def takeNamed (name : Name) (args : Array Arg) : Array ArgVal × Array Arg := Id.run do
   let mut matching := #[]
   let mut remaining := #[]
   for arg in args do
@@ -120,9 +120,9 @@ def takeNamed (name : Name) (args : Array RoleArgument) : Array Doc.Elab.RoleArg
     remaining := remaining.push arg
   (matching, remaining)
 
-def LeanBlockConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] (args : Array RoleArgument) : m LeanBlockConfig := do
+def LeanBlockConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] (args : Array Arg) : m LeanBlockConfig := do
   if h : 0 < args.size then
-    let .anonymous (.name contextName) := args[0]
+    let .anon (.name contextName) := args[0]
       | throwError s!"Expected context name, got {repr args[0]}"
     let (showArgs, args) := takeNamed `show <| args.extract 1 args.size
     let showArg ← takeVal `show showArgs >>= Option.mapM (asBool `show)
@@ -143,12 +143,12 @@ def LeanBlockConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [M
     }
   else throwError "No arguments provided, expected at least a context name"
 where
-  asName (name : Name) (v : Doc.Elab.RoleArgumentValue) : m Name := do
+  asName (name : Name) (v : ArgVal) : m Name := do
     match v with
     | .name b => do
       pure b.getId
     | other => throwError "Expected Boolean for '{name}', got {repr other}"
-  asBool (name : Name) (v : Doc.Elab.RoleArgumentValue) : m Bool := do
+  asBool (name : Name) (v : ArgVal) : m Bool := do
     match v with
     | .name b => do
       let b' ← resolveGlobalConstNoOverloadWithInfo b
@@ -245,9 +245,9 @@ structure LeanOutputConfig where
   name : Ident
   severity : Option MessageSeverity
 
-def LeanOutputConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] (args : Array RoleArgument) : m LeanOutputConfig := do
+def LeanOutputConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] (args : Array Arg) : m LeanOutputConfig := do
   if h : 0 < args.size then
-    let .anonymous (.name outputName) := args[0]
+    let .anon (.name outputName) := args[0]
       | throwError s!"Expected output name, got {repr args[0]}"
     let (severityArgs, args) := takeNamed `severity <| args.extract 1 args.size
     let severityArg ← takeVal `severity severityArgs >>= Option.mapM (asSeverity `severity)
@@ -260,7 +260,7 @@ def LeanOutputConfig.fromArgs [Monad m] [MonadInfoTree m] [MonadResolveName m] [
     }
   else throwError "No arguments provided, expected at least a context name"
 where
-  asSeverity (name : Name) (v : Doc.Elab.RoleArgumentValue) : m MessageSeverity := do
+  asSeverity (name : Name) (v : ArgVal) : m MessageSeverity := do
     match v with
     | .name b => do
       let b' ← resolveGlobalConstNoOverloadWithInfo b

src/leanblog/LeanDoc/Genre/Blog/Basic.lean

@@ -83,6 +83,8 @@ structure Blog.TraverseState where
   targets : Lean.NameMap Blog.Info.Target := {}
   refs : Lean.NameMap Blog.Info.Ref := {}
   pageIds : Lean.NameMap (List String) := {}
+  scripts : Lean.HashSet String := {}
+  stylesheets : Lean.HashSet String := {}
 
 
 def Blog : Genre where
@@ -137,11 +139,13 @@ where
 
 instance : BEq TraverseState where
   beq
-    | ⟨u1, t1, r1, p1⟩, ⟨u2, t2, r2, p2⟩ =>
+    | ⟨u1, t1, r1, p1, s1, s1'⟩, ⟨u2, t2, r2, p2, s2, s2'⟩ =>
       u1.toList.map (fun p => {p with snd := p.snd.toList}) == u2.toList.map (fun p => {p with snd := p.snd.toList}) &&
       t1.toList == t2.toList &&
       r1.toList == r2.toList &&
-      p1.toList == p2.toList
+      p1.toList == p2.toList &&
+      s1.toList == s2.toList &&
+      s1'.toList == s2'.toList
 
 
 namespace Traverse
@@ -151,19 +155,155 @@ open Doc
 @[reducible]
 defmethod Blog.TraverseM := ReaderT Blog.TraverseContext (StateT Blog.TraverseState IO)
 
+def highlightingStyle : String := "
+.hl.lean .keyword {
+  font-weight : bold;
+}
+
+.hl.lean .var {
+  font-style: italic;
+  position: relative;
+}
+
+.hover-container {
+    width: 0;
+    height: 0;
+    position: relative;
+    display: inline;
+}
+
+.hl.lean .token .hover-info {
+  display: none;
+  position: absolute;
+  background-color: #e5e5e5;
+  border: 1px solid black;
+  padding: 0.5em;
+  z-index: 200;
+}
+
+.hl.lean .token:hover .hover-info {
+  display: inline-block;
+  position: absolute;
+  top: 1em;
+  font-weight: normal;
+  font-style: normal;
+}
+
+.hl.lean .has-info:hover .hover-info {
+  display: inline-block;
+  position: absolute;
+  top: 1em;
+  font-weight: normal;
+  font-style: normal;
+}
+
+
+.hl.lean .token {
+  transition: all 0.25s; /* Slight fade for highlights */
+}
+
+.hl.lean .token.binding-hl {
+  background-color: #eee;
+  border-radius: 2px;
+  transition: none;
+}
+
+
+.hl.lean .has-info {
+  text-decoration-style: wavy;
+  text-decoration-line: underline;
+  text-decoration-thickness: 0.1rem;
+}
+
+.hl.lean .has-info .hover-info {
+  display: none;
+  position: absolute;
+  transform: translate(0.25rem, 0.3rem);
+  border: 1px solid black;
+  padding: 0.5em;
+  z-index: 300;
+}
+
+.hl.lean .has-info.error {
+  text-decoration-color: red;
+}
+
+.hl.lean .has-info.error:hover {
+  background-color: #ffb3b3;
+}
+
+.hl.lean .has-info.error .hover-info {
+  background-color: #ffb3b3;
+}
+
+.error pre {
+    color: red;
+}
+
+.hl.lean .has-info.warning {
+  text-decoration-color: yellow;
+}
+
+.hl.lean .has-info.warning .hover-info {
+  background-color: yellow;
+}
+
+.hl.lean .has-info.info {
+  text-decoration-color: blue;
+}
+
+.hl.lean .has-info.info .hover-info {
+  background-color: #4777ff;
+}
+
+.hl.lean .info {
+  display: none;
+}
+"
+
+def highlightingJs : String :=
+"window.onload = () => {
+    for (const c of document.querySelectorAll(\".hl.lean .token\")) {
+        if (c.dataset.binding != \"\") {
+            c.addEventListener(\"mouseover\", (event) => {
+                const context = c.closest(\".hl.lean\").dataset.leanContext;
+                for (const example of document.querySelectorAll(\".hl.lean\")) {
+                    if (example.dataset.leanContext == context) {
+                        for (const tok of example.querySelectorAll(\".token\")) {
+                            if (c.dataset.binding == tok.dataset.binding) {
+                                tok.classList.add(\"binding-hl\");
+                            }
+                        }
+                    }
+                }
+            });
+        }
+        c.addEventListener(\"mouseout\", (event) => {
+            for (const tok of document.querySelectorAll(\".hl.lean .token\")) {
+                tok.classList.remove(\"binding-hl\");
+            }
+        });
+    }
+}
+"
+
 instance : Traverse Blog Blog.TraverseM where
   part _ := pure ()
   block _ := pure ()
   inline _ := pure ()
   genrePart _ _ := pure none
-  genreBlock _ _ := pure none
+  genreBlock
+    | .highlightedCode .., _contents => do
+      modify fun st => {st with stylesheets := st.stylesheets.insert highlightingStyle, scripts := st.scripts.insert highlightingJs}
+      pure none
+    | _, _ => pure none
   genreInline
     | .label x, _contents => do
       -- Add as target if not already present
       if let none := (← get).targets.find? x then
         let path := (← read).path
         let htmlId := (← get).freshId path x
-        modify (fun st => {st with targets := st.targets.insert x ⟨path, htmlId⟩})
+        modify fun st => {st with targets := st.targets.insert x ⟨path, htmlId⟩}
       pure none
     | .ref _x, _contents =>
       -- TODO backreference

src/leanblog/LeanDoc/Genre/Blog/Generate.lean

@@ -24,6 +24,8 @@ def Generate.Context.templateContext (ctxt : Generate.Context) (params : Templat
   config := ctxt.config
   params := params
   path := ctxt.ctxt.path
+  builtInStyles := ctxt.xref.stylesheets
+  builtInScripts := ctxt.xref.scripts
 
 abbrev GenerateM := ReaderT Generate.Context IO
 

src/leanblog/LeanDoc/Genre/Blog/Template.lean

@@ -167,6 +167,8 @@ structure Context where
   config : Config
   path : List String
   params : Params
+  builtInStyles : Lean.HashSet String
+  builtInScripts : Lean.HashSet String
 
 end Template
 
@@ -197,6 +199,14 @@ def param [TypeName α] (key : String) : TemplateM α := do
     if let some v := val.get? (α := α) then return v
     else throw <| .wrongParamType key (TypeName.typeName α)
 
+def builtinHeader : TemplateM Html := do
+  let mut out := .empty
+  for style in (← read).builtInStyles do
+    out := out ++ {{<style>"\n"{{style}}"\n"</style>"\n"}}
+  for script in (← read).builtInScripts do
+    out := out ++ {{<script>"\n"{{script}}"\n"</script>"\n"}}
+  pure out
+
 namespace Params
 
 end Params

src/leanblog/LeanDoc/Genre/Blog/Theme.lean

@@ -63,6 +63,7 @@ def primary : Template := do
     <html>
       <head>
         <title>{{← param (α := String) "title"}}</title>
+        {{← builtinHeader}}
         <link rel="stylesheet" href="/static/style.css"/>
       </head>
       <body>

src/leandoc/LeanDoc/Doc.lean

@@ -95,14 +95,14 @@ instance [Repr g.Inline] : Repr (Inline g) where
 
 
 inductive ArgVal where
-  | name (x : String)
+  | name (x : Lean.Ident)
   | str (text : String)
   | num (n : Nat)
 deriving Repr
 
 inductive Arg where
   | anon (value : ArgVal)
-  | named (name : String) (value : ArgVal)
+  | named (name : Name) (value : ArgVal)
 deriving Repr
 
 structure ListItem (α : Type u) where

src/leandoc/LeanDoc/Doc/Elab.lean

@@ -70,20 +70,21 @@ def _root_.LeanDoc.Syntax.bold.expand : InlineExpander
     ``(Inline.bold #[$[$(← args.mapM elabInline)],*])
   | _ => throwUnsupportedSyntax
 
-def parseArgVal (val : TSyntax `arg_val) : DocElabM RoleArgumentValue := do
+def parseArgVal (val : TSyntax `arg_val) : DocElabM ArgVal := do
   match val with
-  | `(arg_val| $s:str) => pure <| .string s.getString
+  | `(arg_val| $s:str) => pure <| .str s.getString
   | `(arg_val| $x:ident) => pure <| .name x
-  | `(arg_val| $n:num) => pure <| .int <| n.getNat
-  | other => throwErrorAt other "Can't decode argument '{repr other}'"
+  | `(arg_val| $n:num) => pure <| .num <| n.getNat
+  | other => throwErrorAt other "Can't decode argument value '{repr other}'"
 
-def parseArgs (argStx : TSyntaxArray `argument) : DocElabM (Array RoleArgument) := do
+def parseArgs (argStx : TSyntaxArray `argument) : DocElabM (Array Arg) := do
   let mut argVals := #[]
   for arg in argStx do
-    match arg.raw with
+    dbg_trace "we got {repr arg}"
+    match arg with
     | `(argument|$v:arg_val) =>
-      argVals := argVals.push (.anonymous (← parseArgVal v))
-    | `(argument| $x:ident := $v) =>
+      argVals := argVals.push (.anon (← parseArgVal v))
+    | `(argument|$x:ident := $v) =>
       argVals := argVals.push (.named x.getId (← parseArgVal v))
     | other => throwErrorAt other "Can't decode argument '{repr other}'"
   pure argVals