wip: inductive ctors

.github/workflows/ci.yml

@@ -92,6 +92,7 @@ jobs:
             sourcecodepro
             sourcesanspro
             sourceserifpro
+            fvextra
 
       - name: Check `tlmgr` version
         run: tlmgr --version

doc/UsersGuide/Basic.lean

@@ -55,6 +55,10 @@ results in
 
 ## More Docstring Examples
 
+{docstring Lean.Syntax}
+
+{docstring List}
+
 {docstring String}
 
 {docstring Subtype}

src/verso-manual/VersoManual/Docstring.lean

@@ -231,7 +231,7 @@ set_option pp.fullNames false in
 #check List.nil
 
 open Meta in
-def DocName.ofName (c : Name) (showUniverses := true) (showNamespace := true) (openDecls : List OpenDecl := []) : MetaM DocName := do
+def DocName.ofName (c : Name) (ppWidth : Nat := 40) (showUniverses := true) (showNamespace := true) (openDecls : List OpenDecl := []) : MetaM DocName := do
   let env ← getEnv
   if let some _ := env.find? c then
     let ctx := {
@@ -246,12 +246,12 @@ def DocName.ofName (c : Name) (showUniverses := true) (showNamespace := true) (o
 
     let ⟨fmt, infos⟩ ← withOptions (·.setBool `pp.tagAppFns true) <|
       ppSignature c (showNamespace := showNamespace) (openDecls := openDecls)
-    let ttSig := Lean.Widget.TaggedText.prettyTagged (w := 40) fmt
+    let ttSig := Lean.Widget.TaggedText.prettyTagged (w := ppWidth) fmt
     let sig := Lean.Widget.tagCodeInfos ctx infos ttSig
 
     let ⟨fmt, infos⟩ ← withOptions (·.setBool `pp.tagAppFns true) <|
       ppName c (showUniverses := showUniverses) (showNamespace := showNamespace) (openDecls := openDecls)
-    let ttName := Lean.Widget.TaggedText.prettyTagged (w := 40) fmt
+    let ttName := Lean.Widget.TaggedText.prettyTagged (w := ppWidth) fmt
     let name := Lean.Widget.tagCodeInfos ctx infos ttName
 
     pure ⟨c, ← renderTagged none name ⟨{}, false⟩, ← renderTagged none sig ⟨{}, false⟩, ← findDocString? env c⟩
@@ -343,7 +343,7 @@ def DeclType.ofName (c : Name) : MetaM DeclType := do
         return .structure (isClass env c) (← DocName.ofName (showNamespace := true) ctor.name) info.fieldNames fieldInfo parents ancestors
 
       else
-        let ctors ← ii.ctors.mapM (DocName.ofName (showNamespace := false) (openDecls := openDecls))
+        let ctors ← ii.ctors.mapM (DocName.ofName (ppWidth := 60) (showNamespace := false) (openDecls := openDecls))
         let t ← inferType <| .const c (ii.levelParams.map .param)
         let t' ← reduceAll t
         return .inductive ctors.toArray (ii.numIndices + ii.numParams) (isPred t')
@@ -384,6 +384,9 @@ def inheritance (within : Name) (inheritance : Array Block.Docstring.ParentInfo)
   name := `Verso.Genre.Manual.Block.inheritance
   data := ToJson.toJson (within, inheritance)
 
+def constructorSignature (signature : Highlighted) : Block where
+  name := `Verso.Genre.Manual.Block.constructorSignature
+  data := ToJson.toJson signature
 
 end Block
 
@@ -449,21 +452,37 @@ def docstringStyle := r#"
   font-size: inherit;
   font-weight: bold;
 }
-.namedocs > .text > .constructors {
-  text-indent: -1ex;
+
+.namedocs > .text .constructor {
+  padding-left: 0.5rem;
+  padding-top: 0;
+  padding-right: 0;
+  padding-bottom: 0;
+  margin-top: 0.5rem;
+  margin-bottom: 1.5rem;
 }
-.namedocs > .text > .constructors > li {
+
+.namedocs > .text .constructor::before {
+  content: '| ';
   display: block;
+  font-family: var(--verso-code-font-family);
+  font-weight: bold;
+  float: left;
+  width: 0.5rem;
+  white-space: pre;
 }
-.namedocs > .text > .constructors > li::before {
-  content: '|';
-  width: 1ex;
-  display: inline-block;
-  font-size: larger;
+
+.namedocs > .text .constructor .name-and-type {
+  padding-left: 0.5rem;
+  float: left;
+  margin-top: 0;
 }
-.namedocs > .text > .constructors > li > .doc {
-  text-indent: 0;
+.namedocs > .text .constructor .docs {
+  clear: both;
+  padding-left: 1rem;
 }
+
+
 .namedocs .methods td, .namedocs .fields td {
   vertical-align: top;
 }
@@ -643,6 +662,25 @@ def fieldSignature.descr : BlockDescr where
         </section>
       }}
 
+@[block_extension Block.constructorSignature]
+def constructorSignature.descr : BlockDescr where
+  traverse _ _ _ := pure none
+  toTeX := some fun _goI goB _id _ contents => contents.mapM goB -- TODO
+  toHtml := some fun _goI goB _id info contents =>
+    open Verso.Doc.Html HtmlT in
+    open Verso.Output Html in do
+      let .ok signature := FromJson.fromJson? (α := Highlighted) info
+        | do Verso.Doc.Html.HtmlT.logError "Failed to deserialize docstring section data while generating HTML"; pure .empty
+
+      return {{
+        <div class="constructor">
+          <pre class="name-and-type hl lean">{{← signature.toHtml}}</pre>
+          <div class="docs">
+            {{← contents.mapM goB}}
+          </div>
+        </div>
+      }}
+
 open Verso.Genre.Manual.Markdown in
 @[block_extension Block.docstring]
 def docstring.descr : BlockDescr where
@@ -708,7 +746,6 @@ def docstring.descr : BlockDescr where
           <pre class="signature hl lean block">{{sig}}</pre>
           <div class="text">
             {{← contents.mapM goB}}
-            {{← moreDeclHtml name goB declType}}
           </div>
         </div>
       }}
@@ -718,37 +755,6 @@ def docstring.descr : BlockDescr where
   extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)]
   extraCssFiles := [("tippy-border.css", tippy.border.css)]
 where
-  md2html (goB) (str : String) : Verso.Doc.Html.HtmlT Manual (ReaderT ExtensionImpls IO) Verso.Output.Html :=
-    open Verso.Doc.Html in
-    open Verso.Output Html in do
-    let some md := MD4Lean.parse str
-      | HtmlT.logError "Markdown parsing failed for {str}"
-        pure <| Html.text true str
-    match md.blocks.mapM (blockFromMarkdown' · Markdown.strongEmphHeaders') with
-    | .error e => HtmlT.logError e; pure <| Html.text true str
-    | .ok blks => blks.mapM goB
-  moreDeclHtml name (goB)
-    | .inductive ctors _ _ =>
-      open Verso.Doc.Html in
-      open Verso.Output Html in do
-      pure {{
-        <h1>"Constructors"</h1>
-        <ul class="constructors">
-          {{← ctors.mapM fun c => do
-              pure {{
-                <li>
-                  <code class="hl lean inline">{{← c.signature.toHtml}}</code>
-                  {{← if let some d := c.docstring? then do
-                      pure {{<div class="doc">{{← md2html goB d}}</div>}}
-                    else pure Html.empty
-                  }}
-                </li>
-              }}
-          }}
-        </ul>
-      }}
-    | _ => pure .empty
-
   saveRef
       (id : InternalId) (name : Name)
       (subterm : Option (Doc.Inline Manual))
@@ -773,7 +779,7 @@ def Inline.leanFromMarkdown (hls : Highlighted) : Inline where
 
 @[inline_extension leanFromMarkdown]
 def leanFromMarkdown.inlinedescr : InlineDescr where
-  traverse id data _ := pure none
+  traverse _id _data _ := pure none
   toTeX :=
     some <| fun go _ _ content => do
       pure <| .seq <| ← content.mapM fun b => do
@@ -926,7 +932,7 @@ def docstring : BlockRoleExpander
 where
   getExtras (name : Name) (declType : Block.Docstring.DeclType) : DocElabM (Array Term) :=
     match declType with
-    | .structure (isClass := isClass) (constructor := constructor) (fieldInfo := fieldInfo) (parents := parents) .. => do
+    | .structure isClass constructor _ fieldInfo parents _ => do
       let ctorRow : Term ← do
         let header := if isClass then "Instance Constructor" else "Constructor"
         let sigDesc ←
@@ -961,6 +967,18 @@ where
           ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.fieldSignature $(quote i.fieldName) $(quote i.type) $(quote inheritedFrom) $(quote <| parents.map (·.parent))) #[$sigDesc,*])
         ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection $(quote header)) #[$fieldSigs,*])
       pure <| #[ctorRow] ++ parentsRow.toArray ++ [fieldsRow]
+    | .inductive ctors .. => do
+      let ctorSigs : Array Term ←
+        -- Elaborate constructor docs in the type's NS
+        ctors.mapM fun c => withTheReader Core.Context ({· with currNamespace := name}) do
+          let sigDesc ←
+            if let some docs := c.docstring? then
+              let some mdAst := MD4Lean.parse docs
+                | throwError "Failed to parse docstring as Markdown"
+              mdAst.blocks.mapM (blockFromMarkdownWithLean [name, c.name])
+            else pure (#[] : Array Term)
+          ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.constructorSignature $(quote c.signature)) #[$sigDesc,*])
+      pure #[← ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.docstringSection "Constructors") #[$ctorSigs,*])]
     | _ => pure #[]
 
 
@@ -1129,7 +1147,7 @@ def tactic : DirectiveExpander
       throwError "No `show` option provided, but the tactic has no user-facing token name"
     let some mdAst := tactic.docString >>= MD4Lean.parse
       | throwError "Failed to parse docstring as Markdown"
-    let contents ← mdAst.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders)
+    let contents ← mdAst.blocks.mapM (blockFromMarkdownWithLean [])
     let userContents ← more.mapM elabBlock
     pure #[← ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])]
 
@@ -1259,7 +1277,7 @@ def conv : DirectiveExpander
     let contents ← if let some d := tactic.docs? then
         let some mdAst := MD4Lean.parse d
           | throwError "Failed to parse docstring as Markdown"
-        mdAst.blocks.mapM (Markdown.blockFromMarkdown · Markdown.strongEmphHeaders)
+        mdAst.blocks.mapM (blockFromMarkdownWithLean [])
       else pure #[]
     let userContents ← more.mapM elabBlock
     let some toShow := opts.show

src/verso/Verso/Doc/Elab/Monad.lean

@@ -324,6 +324,9 @@ instance : Inhabited (DocElabM α) := ⟨fun _ _ => default⟩
 
 instance : AddErrorMessageContext DocElabM := inferInstanceAs <| AddErrorMessageContext (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
 
+instance [MonadWithReaderOf ρ TermElabM] : MonadWithReaderOf ρ DocElabM :=
+  inferInstanceAs <| MonadWithReaderOf ρ (ReaderT PartElabM.State (StateT DocElabM.State TermElabM))
+
 instance : MonadLift TermElabM DocElabM where
   monadLift act := fun _ st' => do return (← Term.withDeclName (← currentDocName) act, st')