feat: allow markup in tutorial summaries (#703)

Author: david-christiansen

examples/tutorial-examples/TutorialExample/Data.lean

@@ -11,7 +11,7 @@ open Verso.Genre.Manual.InlineLean
 #doc (Tutorial) "Inductive Types" =>
 %%%
 slug := "inductive-types"
-summary := "describes inductive types"
+summary := inlines!"describes inductive types"
 exampleStyle := .inlineLean `Data
 %%%
 

examples/tutorial-examples/TutorialExample/HashMap.lean

@@ -14,7 +14,7 @@ open Verso.Genre.Manual InlineLean
 #doc (Tutorial) "Using `Std.HashMap`" =>
 %%%
 slug := "hashmap"
-summary := "describes hash maps"
+summary := inlines!"describes hash maps"
 exampleStyle := .inlineLean `HashMap
 %%%
 

examples/tutorial-examples/TutorialExample/RCases.lean

@@ -12,7 +12,7 @@ open Verso.Genre.Manual InlineLean
 #doc (Tutorial) "RCases" =>
 %%%
 slug := "rcases"
-summary := "is a tactic for case analysis"
+summary := inlines!"is a tactic for case analysis"
 exampleStyle := .inlineLean `RCases
 %%%
 

src/verso-manual/VersoManual/Basic.lean

@@ -1442,7 +1442,7 @@ instance : TeX.GenreTeX Manual (ReaderT ExtensionImpls IO) where
     impl goI goB id b.data content
   inline go i content := do
     let some id := i.id
-      | panic! "Inline {i.name} wasn't assigned an ID during traversal"
+      | panic! s!"Inline {i.name} wasn't assigned an ID during traversal"
     let some descr := (← readThe ExtensionImpls).getInline? i.name
       | panic! s!"Unknown inline {i.name} while rendering.\n\nKnown inlines: {(← readThe ExtensionImpls).inlineDescrs.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString)}"
     let some impl := descr.toTeX
@@ -1509,7 +1509,7 @@ instance : Html.GenreHtml Manual (ReaderT AllRemotes (ReaderT ExtensionImpls IO)
 
   inline go i content := do
     let some id := i.id
-      | panic! "Inline {i.name} wasn't assigned an ID during traversal"
+      | panic! s!"Inline {i.name} wasn't assigned an ID during traversal"
     let some descr := (← readThe ExtensionImpls).getInline? i.name
       | panic! s!"Unknown inline {i.name} with data {i.data} while rendering HTML.\n\nKnown inlines: {(← readThe ExtensionImpls).inlineDescrs.toArray |>.map (·.fst) |>.qsort (·.toString < ·.toString)}"
     let some impl := descr.toHtml

src/verso-tutorial/VersoTutorial.lean

@@ -467,8 +467,8 @@ def toSite (tuts : Tutorials) : EmitM Blog.Site := do
       let some m := tut.metadata
         | return none
       return some {
-        term := #[.link (← tut.title.mapM inlineToPage) s!"./{m.slug}/"],
-        desc := tut.metadata.map (.para #[.text <| ·.summary]) |>.toArray
+        term := #[.link (← tut.title.mapM inlineToPage) s!"./{m.slug}/g"],
+        desc := (← tut.metadata.mapM ((Block.para #[·]) <$> inlineToPage ·.summary)).toArray
       }
     return { t with
       metadata := none,

src/verso-tutorial/VersoTutorial/Basic.lean

@@ -34,7 +34,7 @@ inductive ExampleCodeStyle where
   The example code should be extracted to a Lean project from the tutorial.
   -/
   | inlineLean (moduleName : Lean.Name) (toolchain := defaultToolchain) (liveProject := some defaultLive)
-deriving BEq, DecidableEq, Inhabited, Repr, ToJson, FromJson
+deriving BEq, Hashable, DecidableEq, Inhabited, Repr, ToJson, FromJson
 
 open Manual (Tag InternalId) in
 /-- Metadata on tutorials. -/
@@ -46,10 +46,10 @@ structure Tutorial.PartMetadata where
   /-- The internal unique ID, which is automatically assigned during traversal. -/
   id : Option InternalId := none
   /-- A summary to show on the overview page. -/
-  summary : String
+  summary : Verso.Doc.Inline Manual
   /-- How should the code samples in this tutorial be extracted to a downloadable tarball? -/
   exampleStyle : ExampleCodeStyle
-deriving BEq, DecidableEq, Inhabited, Repr, ToJson, FromJson
+deriving BEq, Hashable, Inhabited, Repr, ToJson, FromJson
 
 /--
 Information that tracks the current context of traversal for a set of tutorials.
@@ -100,7 +100,7 @@ open Manual (ExtensionImpls)
 
 /-- The metadata to use for a tutorial when the user does not specify any. -/
 def defaultMetadata (p : Part Tutorial) : Tutorial.PartMetadata :=
-  { slug := p.titleString.sluggify.toString, summary := "", exampleStyle := .inlineLean `Main }
+  { slug := p.titleString.sluggify.toString, summary := inlines!"", exampleStyle := .inlineLean `Main }
 
 instance : TraversePart Tutorial where
   inPart p ctx :=
@@ -186,6 +186,9 @@ instance : Traverse Tutorial TraverseM where
     -- Next, assign a tag, prioritizing user-chosen external IDs
     «meta» := { «meta» with tag := ← withReader (TraversePart.inPart part) <| tagPart part «meta» (·.id) (·.tag) savePartXref }
 
+    -- Traverse the metadata's description
+    «meta» := { «meta» with summary := ← withReader (TraversePart.inPart part) <| Genre.traverseInline Manual «meta».summary }
+
     pure <|
       if «meta» == startMeta then none
       else pure { part with metadata := some «meta» }

src/verso/Verso/Doc/Concrete/InlineString.lean

@@ -24,7 +24,9 @@ syntax:max (name := inlinesLit) "inlines!" noWs str : term
 syntax:max (name := blocksLit) "blocks!" noWs str : term
 
 open Lean Elab Term in
-elab_rules : term
+elab_rules : term <= ty
+  | `(inlines!"") => do
+    elabTerm (← ``(Lean.Doc.Inline.empty)) ty
   | `(inlines!%$tk$s) => do
     let inls ← stringToInlines s
     let gTerm ← `(term|_%$tk)
@@ -33,7 +35,9 @@ elab_rules : term
       ⟨gTerm, g, .onlyIfDefined, .none⟩
       { highlightDeduplicationTable := .none }
       (.init (← `(foo))) <| inls.mapM (elabInline ⟨·⟩)
-    elabTerm (← ``(Inline.concat #[ $[$tms],* ] )) none
+    elabTerm (← ``(Inline.concat #[ $[$tms],* ] )) ty
+  | `(blocks!"") => do
+    elabTerm (← ``(Lean.Doc.Block.empty)) ty
   | `(blocks!%$tk$s) => do
     let inls ← stringToBlocks s
     let g ← Meta.mkFreshExprMVar (some (.const ``Verso.Doc.Genre []))
@@ -42,7 +46,7 @@ elab_rules : term
       ⟨gTerm, g, .onlyIfDefined, .none⟩
       { highlightDeduplicationTable := .none }
       (.init (← `(foo))) <| inls.mapM (elabBlock ⟨·⟩)
-    elabTerm (← ``(Block.concat #[ $[$tms],* ] )) none
+    elabTerm (← ``(Block.concat #[ $[$tms],* ] )) ty
 
 
 set_option pp.rawOnError true