feat: heuristic rendering of commands in code blocks

doc/UsersGuide/Basic.lean

@@ -73,7 +73,7 @@ results in
 :::tactic "simp"
 :::
 
-
+{docstring Nat}
 
 # Index
 %%%

src/verso-manual/VersoManual/Docstring.lean

@@ -775,6 +775,10 @@ def Inline.leanFromMarkdown (hls : Highlighted) : Inline where
   name := ``Verso.Genre.Manual.leanFromMarkdown
   data := ToJson.toJson hls
 
+def Block.leanFromMarkdown (hls : Highlighted) : Block where
+  name := ``Verso.Genre.Manual.leanFromMarkdown
+  data := ToJson.toJson hls
+
 
 @[inline_extension leanFromMarkdown]
 def leanFromMarkdown.inlinedescr : InlineDescr where
@@ -798,8 +802,30 @@ def leanFromMarkdown.inlinedescr : InlineDescr where
       | .ok (hl : Highlighted) =>
         hl.inlineHtml "docstring-examples"
 
+@[block_extension leanFromMarkdown]
+def leanFromMarkdown.blockdescr : BlockDescr where
+  traverse _id _data _ := pure none
+  toTeX :=
+    some <| fun goI goB _ _ content => do
+      pure <| .seq <| ← content.mapM fun b => do
+        pure <| .seq #[← goB b, .raw "\n"]
+  extraCss := [highlightingStyle]
+  extraJs := [highlightingJs]
+  extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)]
+  extraCssFiles := [("tippy-border.css", tippy.border.css)]
+  toHtml :=
+    open Verso.Output Html in
+    open Verso.Doc.Html in
+    some <| fun _ _ _ data _ => do
+      match FromJson.fromJson? (α := Highlighted) data with
+      | .error err =>
+        HtmlT.logError <| "Couldn't deserialize Lean code while rendering inline HTML: " ++ err
+        pure .empty
+      | .ok (hl : Highlighted) =>
+        hl.blockHtml "docstring-examples"
+
 open Lean Elab Term in
-def tryElabInlineCodeTerm (str : String) : DocElabM Term := do
+def tryElabCodeTermWith (mk : Highlighted → String → DocElabM α) (str : String) : DocElabM α := do
   let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos
   let src :=
     if let some ⟨line, col⟩ := loc then s!"<docstring at {← getFileName}:{line}:{col}>"
@@ -832,10 +858,91 @@ def tryElabInlineCodeTerm (str : String) : DocElabM Term := do
       throwError m!"Didn't elaborate {stx} as term"
 
     let hls := (← highlight stx #[] (PersistentArray.empty.push tree))
+    mk hls str
 
-    logInfoAt (← getRef) m!"Elaborated {stx} -> {e}"
+open Lean Elab Term in
+def tryElabInlineCodeTerm : String → DocElabM Term :=
+  tryElabCodeTermWith fun hls str =>
     ``(Verso.Doc.Inline.other (Inline.leanFromMarkdown $(quote hls)) #[Verso.Doc.Inline.code $(quote str)])
 
+open Lean Elab Term in
+def tryElabBlockCodeTerm : String → DocElabM Term :=
+  tryElabCodeTermWith fun hls str =>
+    ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)])
+
+private def indentColumn (str : String) : Nat := Id.run do
+  let mut i : Option Nat := none
+  for line in str.split (· == '\n') do
+    let leading := line.takeWhile (·.isWhitespace)
+    if leading == line then continue
+    if let some i' := i then
+      if leading.length < i' then i := some leading.length
+    else i := some leading.length
+  return i.getD 0
+
+/-- info: 0 -/
+#guard_msgs in
+#eval indentColumn ""
+/-- info: 0 -/
+#guard_msgs in
+#eval indentColumn "abc"
+/-- info: 3 -/
+#guard_msgs in
+#eval indentColumn "   abc"
+/-- info: 3 -/
+#guard_msgs in
+#eval indentColumn "   abc\n\n   def"
+/-- info: 2 -/
+#guard_msgs in
+#eval indentColumn "   abc\n\n  def"
+/-- info: 2 -/
+#guard_msgs in
+#eval indentColumn "   abc\n\n  def\n    a"
+
+open Lean Elab Term in
+def tryElabBlockCodeCommand (str : String) : DocElabM Term := do
+    let loc := (← getRef).getPos?.map (← getFileMap).utf8PosToLspPos
+    let src :=
+      if let some ⟨line, col⟩ := loc then s!"<docstring at {← getFileName}:{line}:{col}>"
+      else s!"<docstring at {← getFileName} (unknown line)>"
+
+    let ictx := Parser.mkInputContext str src
+    let cctx : Command.Context := { fileName := ← getFileName, fileMap := FileMap.ofString str, tacticCache? := none, snap? := none, cancelTk? := none}
+
+    let mut cmdState : Command.State := {env := ← getEnv, maxRecDepth := ← MonadRecDepth.getMaxRecDepth, scopes := [{header := ""}]}
+    let mut pstate := {pos := 0, recovering := false}
+    let mut cmds := #[]
+
+    repeat
+      let scope := cmdState.scopes.head!
+      let pmctx := { env := cmdState.env, options := scope.opts, currNamespace := scope.currNamespace, openDecls := scope.openDecls }
+      let (cmd, ps', messages) := Parser.parseCommand ictx pmctx pstate cmdState.messages
+      cmds := cmds.push cmd
+      pstate := ps'
+      cmdState := {cmdState with messages := messages}
+
+      cmdState ← withInfoTreeContext (mkInfoTree := pure ∘ InfoTree.node (.ofCommandInfo {elaborator := `Manual.Meta.lean, stx := cmd})) do
+        match (← liftM <| EIO.toIO' <| (Command.elabCommand cmd cctx).run cmdState) with
+        | Except.error e => Lean.logError e.toMessageData; return cmdState
+        | Except.ok ((), s) => return s
+
+      if Parser.isTerminalCommand cmd then break
+
+    for msg in cmdState.messages.unreported do
+      logMessage msg
+
+    if cmdState.messages.hasErrors then
+      throwError "Errors found in command"
+
+    let mut hls := Highlighted.empty
+    for cmd in cmds do
+      hls := hls ++ (← highlight cmd cmdState.messages.toArray cmdState.infoState.trees)
+
+    hls := hls.deIndent (indentColumn str)
+
+    ``(Verso.Doc.Block.other (Block.leanFromMarkdown $(quote hls)) #[Verso.Doc.Block.code $(quote str)])
+
+
 
 open Lean Elab Term in
 def tryElabInlineCodeName (str : String) : DocElabM Term := do
@@ -875,6 +982,24 @@ def tryElabInlineCode (decls : List Name) (str : String) : DocElabM Term := do
         logWarning m!"Internal exception uncaught: {e.toMessageData}"
         ``(Verso.Doc.Inline.code $(quote str))
 
+open Lean Elab Term in
+def tryElabBlockCode (decls : List Name) (str : String) : DocElabM Term := do
+  match decls with
+  | decl :: decls =>
+    -- This brings the parameters into scope, so the term elaboration version catches them!
+    Meta.forallTelescopeReducing (← getConstInfo decl).type fun _ _ =>
+      tryElabBlockCode decls str
+  | [] =>
+    try
+      tryElabBlockCodeCommand str <|> tryElabBlockCodeTerm str
+    catch
+      | .error ref e =>
+        logWarningAt ref e
+        ``(Verso.Doc.Block.code $(quote str))
+      | e =>
+        logWarning m!"Internal exception uncaught: {e.toMessageData}"
+        ``(Verso.Doc.Block.code $(quote str))
+
 /--
 Heuristically elaborate Lean fragments in Markdown code. The provided names are used as signatures,
 from left to right, with the names bound by the signature being available in the local scope in
@@ -884,6 +1009,7 @@ def blockFromMarkdownWithLean (names : List Name) (b : MD4Lean.Block) : DocElabM
   Markdown.blockFromMarkdown b
     (handleHeaders := Markdown.strongEmphHeaders)
     (elabInlineCode := tryElabInlineCode names)
+    (elabBlockCode := tryElabBlockCode names)
 
 @[block_role_expander docstring]
 def docstring : BlockRoleExpander

src/verso-manual/VersoManual/Markdown.lean

@@ -136,7 +136,10 @@ private partial def blockFromMarkdownAux [Monad m] [AddMessageContext m] [MonadQ
   | .blockquote bs => do ``(Verso.Doc.Block.blockquote #[$[$(← bs.mapM blockFromMarkdownAux )],*])
   | .code _ _ _ strs => do
     let str := String.join strs.toList
-    ``(Verso.Doc.Block.code $(quote str))
+    if let some f := (← read).elabBlockCode then
+      f str
+    else
+      ``(Verso.Doc.Block.code $(quote str))
   | .ul _ _ items => do ``(Verso.Doc.Block.ul #[$[$(← items.mapM itemFromMarkdown)],*])
   | .ol _ i _ items => do
     let itemStx ← items.mapM itemFromMarkdown

src/verso/Verso/Code/Highlighted.lean

@@ -15,6 +15,41 @@ open Verso.Output Html
 open Lean (Json)
 open Std (HashMap)
 
+namespace SubVerso.Highlighting
+/--
+Remove n levels of indentation from highlighted code.
+-/
+partial def Highlighted.deIndent (n : Nat) (hl : Highlighted) : Highlighted :=
+  (remove hl).run' (some n)
+where
+  remove (hl : Highlighted) : StateM (Option Nat) Highlighted := do
+    match hl with
+    | .token t =>
+      set (none : Option Nat)
+      return .token t
+    | .span i x => .span i <$> remove x
+    | .seq xs => .seq <$> xs.mapM remove
+    | .text s =>
+      let mut s' := ""
+      let mut iter := s.iter
+      while h : iter.hasNext do
+        let c := iter.curr' h
+        iter := iter.next
+        match c with
+        | '\n' =>
+          set (some n)
+        | ' ' =>
+          if let some (i + 1) ← get then
+            set (some i)
+            continue
+        | _ => set (none : Option Nat)
+        s' := s'.push c
+      return .text s'
+    | .point p s => return .point p s
+    | .tactics gs x y hl => .tactics gs x y <$> remove hl
+
+end SubVerso.Highlighting
+
 
 namespace Verso.Code
 

src/verso/Verso/Output/Html.lean

@@ -283,6 +283,15 @@ info: Verso.Output.Html.tag
 #guard_msgs in
   #eval test
 
+def leanKwTest : Html := {{
+  <label for="foo">"Blah"</label>
+}}
+
+/-- info: Verso.Output.Html.tag "label" #[("for", "foo")] (Verso.Output.Html.text true "Blah") -/
+#guard_msgs in
+  #eval leanKwTest
+
+
 /-- error: 'br' doesn't allow contents -/
 #guard_msgs in
   #eval show Html from {{ <br>"foo" "foo"</br> }}