feat: super-basic support for manuals

Main.lean

@@ -10,6 +10,9 @@ import LeanDoc.Output.Html
 import LeanDoc.Doc.Concrete
 import LeanDoc.Doc.Lsp
 
+import LeanDoc.Genre.Blog
+import LeanDoc.Genre.Manual
+
 open LeanDoc Doc Output Html Concrete ToHtml Elab Monad
 open Lean Elab Term
 
@@ -23,7 +26,7 @@ def vanish : RoleExpander
 def rev : RoleExpander
   | _args, stxs => .reverse <$> stxs.mapM elabInline
 
-def html [Monad m] (doc : Doc .none) : m Html := Genre.none.toHtml {logError := fun _ => pure ()} () () doc
+def html [Monad m] (doc : Part .none) : m Html := Genre.none.toHtml {logError := fun _ => pure ()} () () doc
 
 def main : IO Unit := do
   IO.println <| Html.asString <| Html.embody <| ← html <| #doc (.none) "My wonderful document" =>

UsersGuide.lean

@@ -0,0 +1,8 @@
+import LeanDoc.Genre.Manual
+
+import UsersGuide.Basic
+
+
+open LeanDoc.Genre.Manual
+
+def main := manualMain (%doc UsersGuide.Basic)

UsersGuide/Basic.Lean

@@ -0,0 +1,11 @@
+import LeanDoc.Genre.Manual
+
+open LeanDoc.Genre
+
+#doc (Manual) "Documentation in Lean" =>
+
+Documentation can take many forms:
+
+ * References
+ * Tutorials
+ * Etc

lakefile.lean

@@ -15,10 +15,24 @@ lean_lib LeanBlog where
   srcDir := "src/leanblog"
   roots := #[`LeanDoc.Genre.Blog]
 
+lean_lib LeanManual where
+  srcDir := "src/manual"
+  roots := #[`LeanDoc.Genre.Manual]
+
 @[default_target]
 lean_exe «leandoc» where
   root := `Main
   -- Enables the use of the Lean interpreter by the executable (e.g.,
   -- `runFrontend`) at the expense of increased binary size on Linux.
   -- Remove this line if you do not need such functionality.
   supportInterpreter := true
+
+lean_lib UsersGuide where
+
+@[default_target]
+lean_exe usersguide where
+  root := `UsersGuide
+  -- Enables the use of the Lean interpreter by the executable (e.g.,
+  -- `runFrontend`) at the expense of increased binary size on Linux.
+  -- Remove this line if you do not need such functionality.
+  supportInterpreter := true

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

@@ -97,7 +97,7 @@ namespace Blog
 structure Post where
   date : Date
   authors : List String
-  content : Doc Blog
+  content : Part Blog
   draft : Bool
 deriving TypeName, Inhabited
 

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

@@ -89,7 +89,7 @@ def inPage (here : Page) (act : GenerateM α) : GenerateM α :=
   withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [here.name]}) act
 
 def inPost (here : Post) (act : GenerateM α) : GenerateM α :=
-  withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [c.ctxt.config.postName here.date here.content.content.titleString ]}) act
+  withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [c.ctxt.config.postName here.date here.content.titleString ]}) act
 
 
 
@@ -125,7 +125,7 @@ mutual
           if post.draft && !(← showDrafts) then continue
           inPost post <| do
             let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.postTemplate, id⟩
-            let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart post.content.content
+            let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart post.content
             ensureDir (← currentDir)
             IO.println s!"Generating post {← currentDir}"
             IO.FS.withFile ((← currentDir).join "index.html") .write fun h => do
@@ -142,7 +142,7 @@ mutual
           some <$> ps.mapM fun p =>
             theme.archiveEntryTemplate.render (.ofList [("post", ⟨.mk p, #[]⟩)])
         else pure none
-      let pageParams : Template.Params ← forPart txt.content
+      let pageParams : Template.Params ← forPart txt
       let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.pageTemplate, id⟩
       let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <|
         match postList with
@@ -164,7 +164,7 @@ def Site.generate (theme : Theme) (site : Site): GenerateM Unit := do
   let root ← currentDir
   ensureDir root
   let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.pageTemplate, id⟩
-  let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart site.frontPage.content
+  let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart site.frontPage
   let filename := root.join "index.html"
   IO.FS.withFile filename .write fun h => do
     h.putStrLn "<!DOCTYPE html>"

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

@@ -10,7 +10,7 @@ inductive Dir α where
 deriving Inhabited
 
 defmethod Post.traverse1 (post : Post) : Blog.TraverseM Post :=
-  withReader (fun ctxt => {ctxt with path := ctxt.path ++ [ctxt.config.postName post.date post.content.content.titleString]}) <| do
+  withReader (fun ctxt => {ctxt with path := ctxt.path ++ [ctxt.config.postName post.date post.content.titleString]}) <| do
     let content' ← Blog.traverse post.content
     pure {post with content := content'}
 
@@ -20,7 +20,7 @@ def Dir.traverse1 (dir : Dir α) (sub : α → Blog.TraverseM α) : Blog.Travers
   | .blog posts => .blog <$> posts.mapM Post.traverse1
 
 inductive Page where
-  | page (name : String) (id : Lean.Name) (text : Doc Blog) (contents : Dir Page)
+  | page (name : String) (id : Lean.Name) (text : Part Blog) (contents : Dir Page)
   | static (name : String) (files : System.FilePath)
 
 instance : Inhabited Page where
@@ -41,7 +41,7 @@ partial def Page.traverse1 (nav : Page) : Blog.TraverseM Page := do
   | .static .. => pure nav
 
 structure Site where
-  frontPage : Doc Blog
+  frontPage : Part Blog
   contents : Dir Page
 
 def Site.traverse1 (site : Site) : Blog.TraverseM Site := do
@@ -69,7 +69,7 @@ class MonadPath (m : Type → Type u) where
 export MonadPath (currentPath)
 
 def postName [Monad m] [MonadConfig m] (post : Post) : m String := do
-  pure <| (← currentConfig).postName post.date post.content.content.titleString
+  pure <| (← currentConfig).postName post.date post.content.titleString
 
 def relative [Monad m] [MonadConfig m] [MonadPath m] (target : List String) : m (List String) := do
   return relativize (← currentPath) target

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

@@ -93,15 +93,15 @@ partial instance : GenreHtml Blog IO where
         pure {{<strong class="internal-error">s!"Can't find target {x}"</strong>}}
       | some tgt =>
         let addr := s!"{String.join ((← relative tgt.path).intersperse "/")}#{tgt.htmlId}"
-        go <| .link contents (.url addr)
+        go <| .link contents addr
     | .pageref x, contents => do
       match (← state).pageIds.find? x with
       | none =>
         HtmlT.logError "Can't find target {x}"
         pure {{<strong class="internal-error">s!"Can't find target {x}"</strong>}}
       | some path =>
         let addr := String.join ((← relative path).intersperse "/")
-        go <| .link contents (.url addr)
+        go <| .link contents addr
     | .htmlSpan classes, contents => do
       pure {{ <span class={{classes}}> {{← contents.mapM go}} </span> }}
     | .blob html, _ => pure html

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

@@ -31,12 +31,12 @@ def dirLinks : Dir Page → TemplateM (Array Html)
   | .pages subs =>
     subs.filterMapM fun
       | .page name _id txt .. =>
-        pure <| some {{<li><a href={{"/" ++ name}}>{{txt.content.titleString}}</a></li>}}
+        pure <| some {{<li><a href={{"/" ++ name}}>{{txt.titleString}}</a></li>}}
       | .static .. => pure none
   | .blog subs =>
     subs.mapM fun s => do
-      let url ← mkLink [(← currentConfig).postName s.date s.content.content.titleString]
-      return {{<li><a href={{url}}>{{s.content.content.titleString}}</a></li>}}
+      let url ← mkLink [(← currentConfig).postName s.date s.content.titleString]
+      return {{<li><a href={{url}}>{{s.content.titleString}}</a></li>}}
 where
   mkLink dest := do
     let dest' ← relative dest
@@ -91,7 +91,7 @@ def archiveEntry : Template := do
     | Date.mk y m d => {{<span class="date"> s!"{y}-{m}-{d}" </span>}}
     }}
     " — "
-    <span class="name">{{post.content.content.titleString}}</span>
+    <span class="name">{{post.content.titleString}}</span>
     </a>
   </li>
 }}]

src/leandoc/LeanDoc/Doc.lean

@@ -42,20 +42,15 @@ instance : Repr Genre.none.PartMetadata where
   reprPrec e _ := nomatch e
 
 
-inductive LinkDest where
-  | url (address : String)
-  | ref (name : String)
-deriving Repr
-
 inductive Inline (genre : Genre) : Type where
   | text (string : String)
   | emph (content : Array (Inline genre))
   | bold (content : Array (Inline genre))
   | code (string : String)
   | linebreak (string : String)
-  | link (content : Array (Inline genre)) (dest : LinkDest)
-  | footnote (name : String)
-  | image (alt : String) (dest : LinkDest)
+  | link (content : Array (Inline genre)) (url : String)
+  | footnote (name : String) (content : Array (Inline genre))
+  | image (alt : String) (url : String)
   | concat (content : Array (Inline genre))
   | other (container : genre.Inline) (content : Array (Inline genre))
 
@@ -71,10 +66,6 @@ private def reprPair (x : α → Nat → Format) (y : β → Nat → Format) (v
 private def reprCtor (c : Name) (args : List Format) : Format :=
   .nest 2 <| .group (.joinSep (.text s!"{c}" :: args) .line)
 
-private def reprHash [BEq α] [Hashable α] (k : α → Nat → Format) (v : β → Nat → Format) (h : Lean.HashMap α β) : Format :=
-  reprCtor ``Lean.HashMap.ofList [reprList (fun x _ => reprPair k v x) h.toList]
-
-
 partial def Inline.reprPrec [Repr g.Inline] (inline : Inline g) (prec : Nat) : Std.Format :=
     open Repr Std.Format in
     let rec go i p :=
@@ -89,7 +80,7 @@ partial def Inline.reprPrec [Repr g.Inline] (inline : Inline g) (prec : Nat) : S
             reprArray go content,
             reprArg dest
           ]
-        | .footnote name => reprCtor ``Inline.footnote [reprArg name]
+        | .footnote name content => reprCtor ``Inline.footnote [reprArg name, reprArray go content]
         | .image content dest => reprCtor ``Inline.image [
             reprArg content,
             reprArg dest
@@ -187,20 +178,6 @@ partial def Part.reprPrec [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] (
 
 instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] : Repr (Part g) := ⟨Part.reprPrec⟩
 
-structure Doc (genre : Genre) where
-  content : Part genre
-  linkRefs : Lean.HashMap String String
-  footnotes : Lean.HashMap String (Array (Inline genre))
-deriving Inhabited
-
-instance [Repr k] [Repr v] [BEq k] [Hashable k] : Repr (Lean.HashMap k v) where
-  reprPrec h _n := reprCtor ``Lean.HashMap.ofList [reprArg h.toList]
-
-def Doc.reprPrec [Repr (Inline g)] [Repr (Part g)] (doc : Doc g) (prec : Nat) : Std.Format :=
-  reprCtor ``Doc.mk [reprArg doc.content, reprArg doc.linkRefs, reprArg doc.footnotes]
-
-instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] [Repr (Part g)] : Repr (Doc g)  := ⟨Doc.reprPrec⟩
-
 class Traverse (g : Genre) (m : outParam (Type → Type)) where
   part [MonadReader g.TraverseContext m] [MonadState g.TraverseState m] : Part g → m Unit
   block [MonadReader g.TraverseContext m] [MonadState g.TraverseState m] : Block g → m Unit
@@ -213,8 +190,8 @@ class Traverse (g : Genre) (m : outParam (Type → Type)) where
 
 partial def Genre.traverse (g : Genre)
     [Traverse g m] [Monad m] [MonadReader g.TraverseContext m] [MonadState g.TraverseState m]
-    (top : Doc g) : m (Doc g) :=
-  doc top
+    (top : Part g) : m (Part g) :=
+  part top
 
 where
   inline (i : Doc.Inline g) : m (Doc.Inline g) := do
@@ -223,7 +200,7 @@ where
     | .emph content => .emph <$> content.mapM inline
     | .bold content => .bold <$> content.mapM inline
     | .link content ref => (.link · ref) <$> content.mapM inline
-    | .footnote name => pure <| .footnote name
+    | .footnote name content => .footnote name <$> content.mapM inline
     | .image alt ref => pure <| .image alt ref
     | .concat content => .concat <$> content.mapM inline
     | .other container content => do
@@ -257,6 +234,3 @@ where
         p := p'
     let .mk title titleString meta content subParts := p
     pure <| .mk (← title.mapM inline) titleString meta (← content.mapM block) (← subParts.mapM part)
-
-  doc (d : Doc g) : m (Doc g) := do
-    pure <| .mk (← part d.content) d.linkRefs (← d.footnotes.foldM (fun fs k v => do pure <| fs.insert k (← v.mapM inline)) .empty)

src/leandoc/LeanDoc/Doc/Concrete.lean

@@ -9,6 +9,7 @@ import Lean
 import LeanDoc.Doc
 import LeanDoc.Doc.Elab
 import LeanDoc.Doc.Elab.Monad
+import LeanDoc.Doc.Lsp
 import LeanDoc.Parser
 import LeanDoc.SyntaxUtils
 
@@ -64,7 +65,7 @@ info: #[Inline.text "Hello, ", Inline.emph #[Inline.bold #[Inline.text "emph"]]]
 #check inlines!"Hello, _*emph*_"
 
 def document : Parser where
-  fn := rawFn <| LeanDoc.Parser.document (blockContext := {maxDirective := some 6})
+  fn := rawFn <| atomicFn <| LeanDoc.Parser.document (blockContext := {maxDirective := some 6})
 
 @[combinator_parenthesizer document] def document.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
 @[combinator_formatter document] def document.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
@@ -74,6 +75,14 @@ partial def findGenre [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv
   | `(($e)) => findGenre e
   | _ => pure ()
 
+def saveRefs [Monad m] [MonadInfoTree m] (st : DocElabM.State) (st' : PartElabM.State) : m Unit := do
+  for r in internalRefs st'.linkDefs st.linkRefs do
+    for stx in r.syntax do
+      pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
+  for r in internalRefs st'.footnoteDefs st.footnoteRefs do
+    for stx in r.syntax do
+      pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
+
 elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:document ":::::::" : command => open Lean Elab Command PartElabM DocElabM in do
   findGenre genre
   let endTok :=
@@ -96,15 +105,9 @@ elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:docu
     pure ()
   let finished := st'.partContext.toPartFrame.close endPos
   pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
-  for r in internalRefs st'.linkDefs st.linkRefs do
-    for stx in r.syntax do
-      pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
-  for r in internalRefs st'.footnoteDefs st.footnoteRefs do
-    for stx in r.syntax do
-      pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
-  let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v))
-  let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v))
-  elabCommand (← `(def $n : Doc $genre := {content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs)}))
+  saveRefs st st'
+
+  elabCommand (← `(def $n : Part $genre := $(← finished.toSyntax st'.linkDefs st'.footnoteDefs)))
 
 
 elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : term => open Lean Elab Term PartElabM DocElabM in do
@@ -122,16 +125,8 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : term
     pure ()
   let finished := st'.partContext.toPartFrame.close endPos
   pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
-  for r in internalRefs st'.linkDefs st.linkRefs do
-    for stx in r.syntax do
-      pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
-  for r in internalRefs st'.footnoteDefs st.footnoteRefs do
-    for stx in r.syntax do
-      pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
-
-  let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v))
-  let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v))
-  elabTerm (← `(({content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs) : Doc $genre}))) none
+  saveRefs st st'
+  elabTerm (← `( ($(← finished.toSyntax st'.linkDefs st'.footnoteDefs) : Part $genre))) none
 
 
 macro "%doc" moduleName:ident : term =>
@@ -161,14 +156,6 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : comm
     pure ()
   let finished := st'.partContext.toPartFrame.close endPos
   pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC}
+  saveRefs st st'
   let docName ← mkIdentFrom title <$> currentDocName
-  let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v))
-  let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v))
-  for r in internalRefs st'.linkDefs st.linkRefs do
-    for stx in r.syntax do
-      pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
-  for r in internalRefs st'.footnoteDefs st.footnoteRefs do
-    for stx in r.syntax do
-      pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r}
-
-  elabCommand (← `(def $docName : Doc $genre := {content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs)}))
+  elabCommand (← `(def $docName : Part $genre := $(← finished.toSyntax st'.linkDefs st'.footnoteDefs)))