EXPERIMENT: produce Expr directly for Verso docs instead of term syntax

doc/UsersGuide/Basic.lean

@@ -1,7 +1,7 @@
 import VersoManual
 import UsersGuide.Markup
 
-open Verso.Genre Manual
+open Verso.Genre Manual InlineLean
 
 set_option pp.rawOnError true
 
@@ -42,7 +42,68 @@ All genres use the same markup syntax, and they can share extensions to the mark
 Mixing incompatible features results in an ordinary Lean type error.
 :::
 
-# Docstrings
+# The Manual Genre
+
+## Tables
+
+Tables can be written using the `table` directive.
+```
+:::table
+* * 1, 1
+  * 1, 2
+* * 2, 1
+  * 2, 2
+* * 3, 1
+  * 3, 2
+:::
+```
+produces
+:::table
+* * 1, 1
+  * 1, 2
+* * 2, 1
+  * 2, 2
+* * 3, 1
+  * 3, 2
+:::
+
+## Inline Lean Code
+
+The namespace `Verso.Genre.Manual.InlineLean` contains the `lean` code block:
+
+````
+```lean (name := twoPlusTwo)
+#check 2 + 2
+```
+````
+results in
+```lean (name := twoPlusTwo)
+#check 2 + 2
+```
+
+and
+
+````
+```leanOutput (name := twoPlusTwo)
+#check 2 + 2
+```
+````
+
+results in
+
+````
+```leanOutput twoPlusTwo
+2 + 2 : Nat
+```
+````
+results in
+```leanOutput twoPlusTwo
+2 + 2 : Nat
+```
+
+
+
+## Docstrings
 %%%
 tag := "docstrings"
 %%%
@@ -57,7 +118,7 @@ results in
 
 {docstring List.forM}
 
-## More Docstring Examples
+### More Docstring Examples
 %%%
 shortTitle := "More Docstrings"
 %%%
@@ -96,7 +157,7 @@ They include heuristic elaboration of code items in their Markdown that attempts
 
 {docstring Thunk}
 
-# Technical Terminology
+## Technical Terminology
 %%%
 shortTitle := "Glossary"
 tag := "tech-terms"

examples/textbook/DemoTextbook/Meta/Lean.lean

@@ -8,8 +8,9 @@ import VersoManual
 
 open Verso.Genre Manual
 open Verso.Doc Elab
+open DocElabM
 open Verso.ArgParse
-open Lean
+open Lean Meta
 
 namespace DemoTextbook
 
@@ -32,11 +33,14 @@ block_extension Block.savedImport (file : String) (source : String) where
 /--
 Lean code that is saved to the examples file.
 -/
-@[code_block_expander savedLean]
-def savedLean : CodeBlockExpander
+@[code_block_elab savedLean]
+def savedLean : CodeBlockElab
   | args, code => do
     let underlying ← InlineLean.lean args code
-    return #[← ``(Block.other (Block.savedLean $(quote (← getFileName)) $(quote (code.getString))) #[$underlying,*])]
+    let g ← genreExpr
+    let b := mkApp2 (.const ``Block.savedLean []) (toExpr (← getFileName)) (toExpr code.getString)
+    return mkApp3 (.const ``Block.other []) g b (← mkArrayLit (← blockType) [underlying])
+
 
 /--
 An import of some other module, to be located in the saved code. Not rendered.

src/multi-verso/MultiVerso/Slug.lean

@@ -10,7 +10,7 @@ set_option linter.missingDocs true
 
 namespace Verso.Multi
 open Verso.Method
-open Lean (ToJson FromJson)
+open Lean (ToJson FromJson ToExpr)
 open Std (HashSet)
 
 /-- The characters allowed in slugs. -/
@@ -71,7 +71,7 @@ theorem String.Pos.add_0_eq_size {c : Char} : (0 : String.Pos) + c = ⟨c.utf8Si
   show 0 + c.utf8Size = c.utf8Size
   simp
 
-instance : DecidablePred Slug.WF := fun str =>
+instance Slug.WF.decide : DecidablePred Slug.WF := fun str =>
   if h : str.toList.all (· ∈ Slug.validChars) then isTrue (by unfold Slug.WF; exact h) else isFalse h
 
 @[simp]
@@ -172,6 +172,11 @@ Converts a string to a slug.
 -/
 def ofString (str : String) : Slug := str.sluggify
 
+/--
+Converts a string to a slug, performing no conversion because the string is already a valid slug.
+-/
+def ofString' (str : String) (wf : WF str := by decide) : Slug := ⟨str, wf⟩
+
 /--
 Returns a slug that's not present in `used`, starting with `slug` and appending consecutive numbers
 until it becomes unique.

src/verso-manual/VersoManual.lean

@@ -148,12 +148,14 @@ block_extension Block.paragraph where
     some <| fun _ go _ _ content => do
       pure <| {{<div class="paragraph">{{← content.mapM go}}</div>}}
 
-@[directive_expander paragraph]
-def paragraph : DirectiveExpander
+open Lean.Meta in
+@[directive_elab paragraph]
+def paragraph : DirectiveElab
   | #[], stxs => do
-    let args ← stxs.mapM elabBlock
-    let val ← ``(Block.other Block.paragraph #[ $[ $args ],* ])
-    pure #[val]
+    let g ← DocElabM.genreExpr
+    let bt ← DocElabM.blockType
+    let args ← stxs.mapM elabBlock'
+    return Lean.mkApp3 (.const ``Block.other []) g (← mkAppM ``Block.paragraph #[]) (← mkArrayLit bt args.toList)
   | _, _ => Lean.Elab.throwUnsupportedSyntax
 
 

src/verso-manual/VersoManual/Basic.lean

@@ -16,7 +16,9 @@ import Verso.Output.Html
 import Verso.Output.TeX
 import Verso.BEq
 
-open Lean (Name Json NameMap ToJson FromJson)
+open Lean (Name Json NameMap ToJson FromJson ToExpr Expr)
+open Lean.ToExpr
+open Lean.Meta
 open Std (HashSet HashMap TreeSet)
 open Verso.Doc
 open Verso.Multi
@@ -59,7 +61,17 @@ instance : ToString Tag where
 instance : Coe String Tag where
   coe := .provided
 
-
+def Tag.toExpr (tag : Tag) : MetaM Expr := do
+  match tag with
+  | .provided x => return Expr.app (.const ``Tag.provided []) (ToExpr.toExpr x)
+  | Tag.internal x => return Expr.app (.const ``Tag.internal []) (ToExpr.toExpr x)
+  | Tag.external x =>
+    let str := ToExpr.toExpr x.toString
+    let p := Expr.app (.const ``Slug.WF []) str
+    -- Should always succeed; we just need to run this due to type erasure
+    let prf ← mkDecideProof p
+    let slug := Lean.mkApp2 (.const ``Slug.ofString' []) str prf
+    return Expr.app (.const ``Tag.external []) slug
 
 /-- When rendering multi-page HTML, should splitting pages follow the depth setting? -/
 inductive HtmlSplitMode where