feat: document inclusion

doc/UsersGuide/Basic.lean

@@ -1,6 +1,9 @@
 import LeanDoc.Genre.Manual
+import UsersGuide.Markup
 
-open LeanDoc.Genre
+open LeanDoc.Genre Manual
+
+set_option pp.rawOnError true
 
 #doc (Manual) "Documentation in Lean" =>
 
@@ -9,3 +12,21 @@ Documentation can take many forms:
  * References
  * Tutorials
  * Etc
+
+{include UsersGuide.Markup}
+
+# Genres
+
+:::paragraph
+Documentation comes in many forms, and no one system is suitable for representing all of them.
+The needs of software documentation writers are not the same as the needs of textbook authors, researchers writing papers, bloggers, or poets.
+Thus, Lean's documentation system supports multiple _genres_, each of which consists of:
+
+ * A global view of a document's structure, whether it be a document with subsections, a collection of interrelated documents such as a web site, or a single file of text
+ * A representation of cross-cutting state such as cross-references to figures, index entries, and named theorems
+ * Additions to the structure of the document - for instance, the blog genre supports the inclusion of raw HTML, and the manual genre supports grouping multiple top-level blocks into a single logical paragraph
+ * Procedures for resolving cross references and rendering the document to one or more output formats
+
+All genres use the same markup syntax, and they can share extensions to the markup language that don't rely on incompatible document structure additions.
+Mixing incompatible features results in an ordinary Lean type error.
+:::

doc/UsersGuide/Markup.lean

@@ -0,0 +1,62 @@
+import LeanDoc.Genre.Manual
+
+open LeanDoc.Genre
+
+#doc (Manual) "Lean Markup" =>
+
+Lean's documentation markup language is a close relative of Markdown, but it's not identical to it.
+
+# Design Principles
+
+ 1. Syntax errors - fail fast rather than producing unexpected output or having complicated rules
+ 2. Reduce lookahead - parsing should succeed or fail as locally as possible
+ 3. Extensibility - there should be dedicated features for compositionally adding new kinds of content, rather than relying on a collection of ad-hoc textual subformats
+ 4. Assume Unicode - Lean users are used to entering Unicode directly and have good tools for it, so there's no need to support alternative textual syntaxes for characters not on keyboards such as em dashes or typographical quotes
+ 5. Markdown compatibility - benefit from existing muscle memory and familiarity when it doesn't lead to violations of the other principles
+ 6. Pandoc and Djot compatibility - when Markdown doesn't have a syntax for a feature, attempt to be compatible with Pandoc Markdown or Djot
+
+# Syntax
+
+Like Markdown, Lean's markup has three primary syntactic categories:
+
+: Inline elements
+
+ The ordinary content of written text, such as text itself, bold or emphasized text, and hyperlinks.
+
+: Block elements
+
+ The main organization of written text, including paragraphs, lists, and quotations. Some blocks may be nested: for example, lists may contain other lists.
+
+: Document structure
+
+ Headers, footnote definitions, and named links give greater structure to a document. They may not be nested inside of blocks.
+
+## Description
+
+### Inline Syntax
+
+### Block Syntax
+
+### Document Structure
+
+## Differences from Markdown
+
+This is a quick "cheat sheet" for those who are used to Markdown, documenting the differences.
+
+### Syntax Errors
+
+While Markdown includes a set of precedence rules to govern the meaning of mismatched delimiters (such as in `what _is *bold_ or emph*?`), these are syntax errors in Lean's markup.
+Similarly, Markdown specifies that unmatched delimiters (such as `*` or `_`) should be included as characters, while Lean's markup requires explicit escaping of delimiters.
+
+This is based on the principle that, for long-form technical writing, it's better to catch typos while writing than while reviewing the text later.
+
+### Reduced Lookahead
+
+In Markdown, whether `[this][here]` is a link depends on whether `here` is defined as a link reference target somewhere in the document.
+In Lean's markup, it is always a link, and it is an error if `here` is not defined as a link target.
+
+### Header Nesting
+
+In Lean's markup, every document already has a title, so there's no need to use the highest level header (`#`) to specify one.
+Additionally, all documents are required to use `#` for their top-level header, `##` for the next level, and so forth, because a single file may represent a section, a chapter, or even a whole book.
+Authors should not need to maintain a global mapping from header levels to document structures, so Lean's markup automatically assigns these based on the structure of the document.

lake-manifest.json

@@ -0,0 +1,14 @@
+{"version": 7,
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover/std4",
+   "type": "git",
+   "subDir": null,
+   "rev": "1f24793af1db9cfb02ba71c6de5f205481de4a55",
+   "name": "std",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "leandoc",
+ "lakeDir": ".lake"}

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

@@ -336,7 +336,8 @@ partial def highlight' (ids : HashMap Lsp.RefIdent Lsp.RefIdent) (stx : Syntax)
       if let .sort ← identKind ids ⟨stx⟩ then
         emitToken i ⟨.sort, x⟩
         return
-      emitToken i <| (⟨ ·,  x⟩) <|
+      else
+        emitToken i <| (⟨ ·,  x⟩) <|
         match x.get? 0 with
         | some '#' => .keyword lookingAt docs
         | some c =>

src/leandoc/LeanDoc/Doc/Elab.lean

@@ -192,6 +192,8 @@ def partCommand (cmd : Syntax) : PartElabM Unit :=
     fallback
 where
   fallback : PartElabM Unit := do
+    if (← getThe PartElabM.State).partContext.priorParts.size > 0 then
+      throwErrorAt cmd "Unexpected block"
     let blk ← liftDocElabM <| elabBlock cmd
     addBlock blk
 
@@ -244,6 +246,21 @@ partial def _root_.LeanDoc.Syntax.header.command : PartCommand
   | _ => throwUnsupportedSyntax
 
 
+@[part_command LeanDoc.Syntax.block_role]
+def includeSection : PartCommand
+  | `(block|block_role{include $_args* }[ $content ]) => throwErrorAt content "Unexpected block argument"
+  | `(block|block_role{include}) => throwError "Expected exactly one argument"
+  | `(block|block_role{include $arg1 $arg2 $args*}) => throwErrorAt arg2 "Expected exactly one argument"
+  | stx@`(block|block_role{include $args* }) => do
+    match (← parseArgs args) with
+    | #[.anon (.name x)] =>
+      let name ← resolved x
+      addPart <| .included name
+    | _ => throwErrorAt stx "Expected exactly one positional argument that is a name"
+  | stx => dbg_trace "Not {stx}"; Lean.Elab.throwUnsupportedSyntax
+where
+ resolved id := mkIdentFrom id <$> resolveGlobalConstNoOverload (mkIdentFrom id (docName id.getId))
+
 @[block_expander LeanDoc.Syntax.para]
 partial def _root_.LeanDoc.Syntax.para.expand : BlockExpander
   | `<low|(LeanDoc.Syntax.para ~(.node _ `null args) )> => do

src/leandoc/LeanDoc/Doc/Elab/Monad.lean

@@ -89,6 +89,7 @@ def internalRefs (defs : HashMap String (DocDef α)) (refs : HashMap String DocU
 
 inductive TOC where
   | mk (title : String) (titleSyntax : Syntax) (endPos : String.Pos) (children : Array TOC)
+  | included (name : Ident)
 deriving Repr, TypeName, Inhabited
 
 structure TocFrame where
@@ -129,6 +130,7 @@ def TocFrame.wrapAll (stack : Array TocFrame) (item : TOC) (endPos : String.Pos)
 
 inductive FinishedPart where
   | mk (titleSyntax : Syntax) (expandedTitle : Array (TSyntax `term)) (titlePreview : String) (blocks : Array (TSyntax `term)) (subParts : Array FinishedPart) (endPos : String.Pos)
+  | included (name : Ident)
 deriving Repr, BEq
 
 private def linkRefName (ref : TSyntax `str) : TSyntax `ident :=
@@ -149,6 +151,7 @@ partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m]
     let subStx ← subParts.mapM (toSyntax {} {})
     let body ← ``(Part.mk #[$[$titleInlines],*] $(quote titleString) none #[$[$blocks],*] #[$[$subStx],*])
     bindFootnotes footnoteDefs (← bindLinks linkDefs body)
+  | .included name => pure name
 where
   bindLinks (linkDefs : HashMap String (DocDef String)) (body : TSyntax `term) : m (TSyntax `term) := do
     let defs ← linkDefs.toArray.mapM fun (_, defn) =>
@@ -163,6 +166,7 @@ where
 partial def FinishedPart.toTOC : FinishedPart → TOC
   | .mk titleStx _titleInlines titleString _blocks subParts endPos =>
     .mk titleString titleStx endPos (subParts.map toTOC)
+  | .included name => .included name
 
 structure PartFrame where
   titleSyntax : Syntax
@@ -276,6 +280,9 @@ def PartElabM.setTitle (titlePreview : String) (titleInlines : Array (TSyntax `t
 def PartElabM.addBlock (block : TSyntax `term) : PartElabM Unit := modifyThe State fun st =>
   {st with partContext.blocks := st.partContext.blocks.push block}
 
+def PartElabM.addPart (finished : FinishedPart) : PartElabM Unit := modifyThe State fun st =>
+  {st with partContext.priorParts := st.partContext.priorParts.push finished}
+
 def PartElabM.addLinkDef (refName : TSyntax `str) (url : String) : PartElabM Unit := do
   let strName := refName.getString
   match (← getThe State).linkDefs.find? strName with

src/leandoc/LeanDoc/Doc/Lsp.lean

@@ -237,8 +237,8 @@ partial def handleSyms (_params : DocumentSymbolParams) (prev : RequestTask Docu
   --pure syms
   where
     combineAnswers (x y : Option DocumentSymbolResult) : DocumentSymbolResult := ⟨graftSymbols (x.getD ⟨{}⟩).syms (y.getD ⟨{}⟩).syms⟩
-    tocSym (text : FileMap) : TOC → Option DocumentSymbol
-      | .mk title titleStx endPos children => Id.run do
+    tocSym (text : FileMap) : TOC → Id (Option DocumentSymbol)
+      | .mk title titleStx endPos children => do
         let some selRange@⟨start, _⟩ := titleStx.lspRange text
           | return none
         let mut kids := #[]
@@ -251,6 +251,16 @@ partial def handleSyms (_params : DocumentSymbolParams) (prev : RequestTask Docu
           selectionRange := selRange,
           children? := kids
         }
+      | .included name => do
+        -- TODO Evaluate the name to find the actual included title
+        let some rng := name.raw.lspRange text
+          | return none
+        return some <| DocumentSymbol.mk {
+          name := toString name,
+          kind := SymbolKind.property,
+          range := rng
+          selectionRange := rng
+        }
     getSections text ss : Array DocumentSymbol := Id.run do
       let mut syms := #[]
       for snap in ss do
@@ -260,7 +270,7 @@ partial def handleSyms (_params : DocumentSymbolParams) (prev : RequestTask Docu
             data.get? TOC
           | _ => none
         for i in info do
-          if let some x := tocSym text i then syms := syms.push x
+          if let some x ← tocSym text i then syms := syms.push x
       pure syms
 
 -- Shamelessly cribbed from https://github.com/tydeu/lean4-alloy/blob/57792f4e8a9674f8b4b8b17742607a1db142d60e/Alloy/C/Server/SemanticTokens.lean

src/leandoc/LeanDoc/Doc/TeX.lean

@@ -67,7 +67,7 @@ partial defmethod Inline.toTeX [Monad m] [GenreTeX g m] : Inline g → TeXT g m
 
 partial defmethod Block.toTeX [Monad m] [GenreTeX g m] : Block g → TeXT g m TeX
   | .para xs => do
-    pure <| (← xs.mapM Inline.toTeX) ++ TeX.raw "\n\n"
+    pure <| (← xs.mapM Inline.toTeX)
   | .blockquote bs => do
     pure \TeX{\begin{quotation} \Lean{← bs.mapM Block.toTeX} \end{quotation}}
   | .ul items => do
@@ -88,7 +88,7 @@ partial defmethod Part.toTeX [Monad m] [GenreTeX g m] (p : Part g) : TeXT g m Te
     pure \TeX{
       \Lean{← header (← p.title.mapM Inline.toTeX)}
       "\n\n"
-      \Lean{← p.content.mapM Block.toTeX}
+      \Lean{← p.content.mapM (fun b => do pure <| TeX.seq #[← Block.toTeX b, .paragraphBreak])}
       "\n\n"
       \Lean{← inHeader <| p.subParts.mapM Part.toTeX }
     }

src/leandoc/LeanDoc/Output/TeX.lean

@@ -10,6 +10,7 @@ inductive TeX where
   | raw (string : String)
   | command (name : String) (optArgs : Array TeX) (args : Array TeX)
   | environment (name : String)  (optArgs : Array TeX) (args : Array TeX) (content : Array TeX)
+  | paragraphBreak
   | seq (contents : Array TeX)
 deriving Repr, Inhabited
 
@@ -34,7 +35,8 @@ partial def asString (doc : TeX) : String :=
   | .environment name opt req content =>
     "\\begin{" ++ name ++ "}" ++ opt.foldl (· ++ "[" ++ ·.asString ++ "]") "" ++ req.foldl (· ++ "{" ++ ·.asString ++ "}") "" ++ "\n" ++
     String.join (content.map (·.asString) |>.toList) ++ "\n" ++
-    "\\end{" ++ name ++ "}\n"
+    "\\end{" ++ name ++ "}"
+  | .paragraphBreak => "\n\n"
   | .seq texs => String.join (texs.map (·.asString) |>.toList)
 where
   escape s := s.replace "\\" "\\\\" |>.replace "{" "\\{" |>.replace "}" "\\}" --TODO make correct!