From a745a0ba33e2929bb4cd7dbc8e413309f956d03d Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 15 Dec 2023 10:14:03 +0100 Subject: [PATCH] feat: document inclusion --- doc/UsersGuide/Basic.lean | 23 +++- doc/UsersGuide/Markup.lean | 62 +++++++++++ lake-manifest.json | 14 +++ .../LeanDoc/Genre/Blog/HighlightCode.lean | 3 +- src/leandoc/LeanDoc/Doc/Elab.lean | 17 +++ src/leandoc/LeanDoc/Doc/Elab/Monad.lean | 7 ++ src/leandoc/LeanDoc/Doc/Lsp.lean | 16 ++- src/leandoc/LeanDoc/Doc/TeX.lean | 4 +- src/leandoc/LeanDoc/Output/TeX.lean | 4 +- src/leandoc/LeanDoc/Parser.lean | 101 ++++++++++++------ src/leandoc/LeanDoc/Syntax.lean | 2 +- src/manual/LeanDoc/Genre/Manual.lean | 27 ++++- 12 files changed, 232 insertions(+), 48 deletions(-) create mode 100644 doc/UsersGuide/Markup.lean create mode 100644 lake-manifest.json diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index 2539c7f..d700ac0 100644 --- a/doc/UsersGuide/Basic.lean +++ b/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. +::: diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean new file mode 100644 index 0000000..97388b4 --- /dev/null +++ b/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. diff --git a/lake-manifest.json b/lake-manifest.json new file mode 100644 index 0000000..42594c8 --- /dev/null +++ b/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"} diff --git a/src/leanblog/LeanDoc/Genre/Blog/HighlightCode.lean b/src/leanblog/LeanDoc/Genre/Blog/HighlightCode.lean index 0c4e561..cd7ce04 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/HighlightCode.lean +++ b/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 => diff --git a/src/leandoc/LeanDoc/Doc/Elab.lean b/src/leandoc/LeanDoc/Doc/Elab.lean index 52df76a..097987b 100644 --- a/src/leandoc/LeanDoc/Doc/Elab.lean +++ b/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 | ` => do diff --git a/src/leandoc/LeanDoc/Doc/Elab/Monad.lean b/src/leandoc/LeanDoc/Doc/Elab/Monad.lean index 4d3443e..3d710c4 100644 --- a/src/leandoc/LeanDoc/Doc/Elab/Monad.lean +++ b/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 diff --git a/src/leandoc/LeanDoc/Doc/Lsp.lean b/src/leandoc/LeanDoc/Doc/Lsp.lean index d4d8a73..1caeb65 100644 --- a/src/leandoc/LeanDoc/Doc/Lsp.lean +++ b/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 diff --git a/src/leandoc/LeanDoc/Doc/TeX.lean b/src/leandoc/LeanDoc/Doc/TeX.lean index f628ab7..f36058f 100644 --- a/src/leandoc/LeanDoc/Doc/TeX.lean +++ b/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 } } diff --git a/src/leandoc/LeanDoc/Output/TeX.lean b/src/leandoc/LeanDoc/Output/TeX.lean index f4a6fdf..4796b0c 100644 --- a/src/leandoc/LeanDoc/Output/TeX.lean +++ b/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! diff --git a/src/leandoc/LeanDoc/Parser.lean b/src/leandoc/LeanDoc/Parser.lean index 812611e..286d91d 100644 --- a/src/leandoc/LeanDoc/Parser.lean +++ b/src/leandoc/LeanDoc/Parser.lean @@ -922,8 +922,6 @@ Remaining: "_ aa_" #guard_msgs in #eval emph {} |>.test! "_ aa_" - - /-- info: Success! Final stack: (LeanDoc.Syntax.code @@ -1037,6 +1035,7 @@ Remaining: "\no `" #guard_msgs in #eval (inline {}).test! "` fo\no `" + /-- info: Success! Final stack: (LeanDoc.Syntax.bold @@ -1418,7 +1417,8 @@ mutual colonFn >> withCurrentColumn fun c => textLine >> ignoreFn (manyFn blankLine) >> fakeAtom "=>" >> - blocks1 { ctxt with minIndent := c} + blocks1 { ctxt with minIndent := c} >> + ignoreFn (manyFn blankLine) where colonFn := atomicFn <| takeWhileFn (· == ' ') >> @@ -1539,6 +1539,8 @@ mutual notFollowedByFn (skipChFn ':') "extra :" >> takeWhileFn (· == ' ') >> (satisfyFn (· == '\n') "newline" <|> eoiFn) + -- This low-level definition is to get exactly the right amount of lookahead + -- together with column tracking partial def block_role (ctxt : BlockCtxt) : ParserFn := fun c s => let iniPos := s.pos let iniSz := s.stxStack.size @@ -1552,7 +1554,7 @@ mutual let s := (intro >> eatSpaces >> ignoreFn (satisfyFn (· == '\n') "newline" <|> eoiFn)) c s if s.hasError then restorePosOnErr s else - let s := block {ctxt with minIndent := col} c s + let s := (nodeFn nullKind <| atomicFn (ignoreFn (eatSpaces >> satisfyFn (· == '\n') "newline")) <|> block {ctxt with minIndent := col}) c s s.mkNode ``block_role iniSz where eatSpaces := takeWhileFn (· == ' ') @@ -1828,6 +1830,31 @@ Remaining: "" #guard_msgs in #eval blocks {} |>.test! ": an excellent idea\n\n Let's say more!\n\n: more\n\n" +/-- +info: Success! Final stack: + [(LeanDoc.Syntax.dl + [(LeanDoc.Syntax.desc + ":" + [(LeanDoc.Syntax.text + (str "\" an excellent idea\""))] + "=>" + [(LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str "\"Let's say more!\""))])]) + (LeanDoc.Syntax.desc + ":" + [(LeanDoc.Syntax.text (str "\" more\""))] + "=>" + [(LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str "\"even more!\""))])])])] +All input consumed. +-/ +-- Test having lots of blank lines between items +#guard_msgs in + #eval blocks {} |>.test! ": an excellent idea\n\n Let's say more!\n\n\n\n\n: more\n\n even more!" + + /-- info: Success! Final stack: [(LeanDoc.Syntax.dl @@ -2205,9 +2232,10 @@ info: Success! Final stack: `test [] "}" - (LeanDoc.Syntax.para - [(LeanDoc.Syntax.text - (str "\"Here's a modified paragraph.\""))])) + [(LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str + "\"Here's a modified paragraph.\""))])]) All input consumed. -/ #guard_msgs in @@ -2219,9 +2247,10 @@ info: Success! Final stack: `test [] "}" - (LeanDoc.Syntax.para - [(LeanDoc.Syntax.text - (str "\"Here's a modified paragraph.\""))])) + [(LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str + "\"Here's a modified paragraph.\""))])]) All input consumed. -/ #guard_msgs in @@ -2233,9 +2262,10 @@ info: Success! Final stack: `test [] "}" - (LeanDoc.Syntax.para - [(LeanDoc.Syntax.text - (str "\"Here's a modified paragraph.\""))])) + [(LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str + "\"Here's a modified paragraph.\""))])]) All input consumed. -/ #guard_msgs in @@ -2248,7 +2278,7 @@ Final stack: `test [] "}" - (LeanDoc.Syntax.para )) + [(LeanDoc.Syntax.para )]) Remaining: "Here's a modified paragraph." -/ #guard_msgs in @@ -2260,15 +2290,15 @@ info: Success! Final stack: `test [] "}" - (LeanDoc.Syntax.blockquote - ">" - [(LeanDoc.Syntax.para - [(LeanDoc.Syntax.text - (str - "\"Here's a modified blockquote\""))]) - (LeanDoc.Syntax.para - [(LeanDoc.Syntax.text - (str "\"with multiple paras\""))])])) + [(LeanDoc.Syntax.blockquote + ">" + [(LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str + "\"Here's a modified blockquote\""))]) + (LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str "\"with multiple paras\""))])])]) Remaining: "that ends" -/ @@ -2290,9 +2320,10 @@ info: Success! Final stack: `test [] "}" - (LeanDoc.Syntax.para - [(LeanDoc.Syntax.text - (str "\"Here's a modified paragraph.\""))])) + [(LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str + "\"Here's a modified paragraph.\""))])]) All input consumed. -/ #guard_msgs in @@ -2313,27 +2344,27 @@ info: Success! Final stack: `test [(LeanDoc.Syntax.anon `arg)] "}" - (LeanDoc.Syntax.para - [(LeanDoc.Syntax.text - (str "\"Here's a modified paragraph.\""))])) + [(LeanDoc.Syntax.para + [(LeanDoc.Syntax.text + (str + "\"Here's a modified paragraph.\""))])]) All input consumed. -/ #guard_msgs in #eval block {} |>.test! "{\n test\n arg}\nHere's a modified paragraph." /-- -info: Failure: '{'; expected ![, *, +, -, [ or [^ -Final stack: +info: Success! Final stack: (LeanDoc.Syntax.block_role "{" `test [(LeanDoc.Syntax.anon `arg)] "}" - (LeanDoc.Syntax.para - [(LeanDoc.Syntax.footnote )])) -Remaining: "\n\nHere's a modified paragraph." + []) +Remaining: +"\nHere's a non-modified paragraph." -/ #guard_msgs in -#eval block {} |>.test! "{\n test\n arg}\n\n\nHere's a modified paragraph." +#eval block {} |>.test! "{\n test\n arg}\n\n\nHere's a non-modified paragraph." /-- diff --git a/src/leandoc/LeanDoc/Syntax.lean b/src/leandoc/LeanDoc/Syntax.lean index 6f287d9..3777a82 100644 --- a/src/leandoc/LeanDoc/Syntax.lean +++ b/src/leandoc/LeanDoc/Syntax.lean @@ -67,4 +67,4 @@ syntax (name:=directive) "directive{" ident argument* "}" "[" block* "]": block /-- A header -/ syntax (name:=header) inline* : block -syntax (name:=block_role) "role{" ident argument* "}" "[" block "]" : block +syntax (name:=block_role) "block_role{" ident argument* "}" ("[" block "]")? : block diff --git a/src/manual/LeanDoc/Genre/Manual.lean b/src/manual/LeanDoc/Genre/Manual.lean index 7a2bfe8..327c188 100644 --- a/src/manual/LeanDoc/Genre/Manual.lean +++ b/src/manual/LeanDoc/Genre/Manual.lean @@ -2,11 +2,13 @@ import LeanDoc.Doc import LeanDoc.Doc.Concrete import LeanDoc.Doc.TeX import LeanDoc.Output.TeX +import LeanDoc.Doc.Lsp +import LeanDoc.Doc.Elab import LeanDoc.Genre.Manual.TeX -open LeanDoc.Doc +open LeanDoc.Doc Elab open LeanDoc.Genre.Manual.TeX @@ -15,19 +17,36 @@ namespace LeanDoc.Genre structure Manual.PartMetadata where authors : List String := [] +inductive Manual.Block where + | paragraph + def Manual : Genre where PartMetadata := Manual.PartMetadata - Block := Empty + Block := Manual.Block Inline := Empty TraverseContext := Unit TraverseState := Unit +namespace Manual + +open LeanDoc.Output.TeX in instance : TeX.GenreTeX Manual IO where part go _meta txt := go txt - block _go b _txt := nomatch b + block go + | .paragraph, content => do + pure <| .seq <| ← content.mapM fun b => do + pure <| .seq #[← go b, .raw "\n"] inline _go i _txt := nomatch i -namespace Manual + +@[directive_expander paragraph] +def paragraph : DirectiveExpander + | #[], stxs => do + let args ← stxs.mapM elabBlock + let val ← ``(Block.other Manual.Block.paragraph #[ $[ $args ],* ]) + pure #[val] + | _, _ => Lean.Elab.throwUnsupportedSyntax + structure Config where destination : System.FilePath := "_out"