From 7b69f84bc78771919d83430e11940f342c5d8d77 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 10 Jan 2024 21:30:24 +0100 Subject: [PATCH] doc: add automatic syntax examples to manual --- doc/UsersGuide/Basic.lean | 2 +- doc/UsersGuide/Markup.lean | 78 ++++++- src/verso/Verso/Doc/Elab.lean | 6 +- src/verso/Verso/Doc/Elab/Monad.lean | 2 + src/verso/Verso/Parser.lean | 328 ++++++++++++++++++++-------- src/verso/Verso/Syntax.lean | 4 +- src/verso/Verso/SyntaxUtils.lean | 14 ++ 7 files changed, 335 insertions(+), 99 deletions(-) diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index dac774e..255f613 100644 --- a/doc/UsersGuide/Basic.lean +++ b/doc/UsersGuide/Basic.lean @@ -5,7 +5,7 @@ open Verso.Genre Manual set_option pp.rawOnError true -#doc (Manual) "Writing Documentation in Lean" => +#doc (Manual) "Writing Documentation in Lean with Verso" => %%% authors := ["David Thrane Christiansen"] diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean index 12bfc84..d9e9c08 100644 --- a/doc/UsersGuide/Markup.lean +++ b/doc/UsersGuide/Markup.lean @@ -1,6 +1,52 @@ +import Verso.Syntax import Verso.Genre.Manual +import Lean + +open Verso Genre + +open Lean in +open Verso.Syntax in +partial def preview [Monad m] [MonadError m] (stx : Syntax) : m String := + match stx with + | `(inline| $s:str) => pure s.getString + | `(inline| line! $s:str) => pure s.getString + | `(inline| _{ $s:inline* }) => do + let contents ← s.toList.mapM (preview ∘ TSyntax.raw) + pure <| "" ++ String.join contents ++ "" + | `(inline| *{ $s:inline* }) => do + let contents ← s.toList.mapM (preview ∘ TSyntax.raw) + pure <| "" ++ String.join contents ++ "" + | `(inline| link[ $txt:inline* ]( $url:str )) => do + let contents ← txt.toList.mapM (preview ∘ TSyntax.raw) + pure s!"{String.join contents}" + | `(inline| link[ $txt:inline* ][ $tgt:str ]) => do + let contents ← txt.toList.mapM (preview ∘ TSyntax.raw) + pure s!"{String.join contents}" + | `(inline| code{ $code:str }) => + pure s!"{code.getString}" + | `(block| para{ $i:inline* }) => do + let contents ← i.toList.mapM (preview ∘ TSyntax.raw) + pure <| String.join contents + | `(block| [ $ref:str ]: $url:str) => + pure s!"where «{ref.getString}» := {url.getString}" + | other => do + if other.getKind = nullKind then + pure <| String.join <| (← other.args.toList.mapM preview).intersperse "\n\n" + else + throwErrorAt stx "Didn't understand {Verso.SyntaxUtils.ppSyntax stx} for preview" + +open Lean Verso Doc Elab Parser in +@[code_block_expander markupPreview] +def markupPreview : CodeBlockExpander + | #[], contents => do + let stx ← blocks {} |>.parseString contents.getString + let p ← preview stx + pure #[ + ← ``(Block.code none #[] 0 $(quote contents.getString)), + ← ``(Block.code none #[] 0 $(quote <| toString <| p)) + ] + | _, contents => throwErrorAt contents "Unexpected arguments" -open Verso.Genre #doc (Manual) "Lean Markup" => @@ -33,10 +79,36 @@ Like Markdown, Lean's markup has three primary syntactic categories: ## Description -TODO build an extension to test the parsing here - ### Inline Syntax +Emphasis is written with underscores: +```markupPreview +Here's some _emphasized_ text +``` +Emphasis can be nested by using more underscores for the outer emphasis: +```markupPreview +Here's some __emphasized text with _extra_ emphasis__ inside +``` + +Strong emphasis (bold) is written with asterisks: +```markupPreview +Here's some *bold* text +``` + +Hyperlinks consist of the link text in square brackets followed by the target in parentheses: +```markupPreview +The [Lean website](https://lean-lang.org) +``` + +```markupPreview +The [Lean website][lean] + +[lean]: https://lean-lang.org +``` + +```markupPreview +The definition of `main` +``` TeX math can be included using a single or double dollar sign followed by code. Two dollar signs results in display-mode math, so `` $`\sum_{i=0}^{10} i` `` results in $`\sum_{i=0}^{10} i` while `` $$`\sum_{i=0}^{10} i` `` results in: $$`\sum_{i=0}^{10} i` diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean index 82ef4a0..2dbf248 100644 --- a/src/verso/Verso/Doc/Elab.lean +++ b/src/verso/Verso/Doc/Elab.lean @@ -54,8 +54,8 @@ partial def _root_.Verso.Syntax.text.expand : InlineExpander := fun x => @[inline_expander Verso.Syntax.linebreak] def _root_.linebreak.expand : InlineExpander - | ` => - ``(Inline.linebreak $(quote s)) + | `(inline|line! $s:str) => + ``(Inline.linebreak $(quote s.getString)) | _ => throwUnsupportedSyntax @[inline_expander Verso.Syntax.emph] @@ -289,7 +289,7 @@ where @[block_expander Verso.Syntax.para] partial def _root_.Verso.Syntax.para.expand : BlockExpander - | ` => do + | `(block| para{ $args:inline* }) => do ``(Block.para #[$[$(← args.mapM elabInline)],*]) | _ => throwUnsupportedSyntax diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean index e8db6d0..8bf0a92 100644 --- a/src/verso/Verso/Doc/Elab/Monad.lean +++ b/src/verso/Verso/Doc/Elab/Monad.lean @@ -266,6 +266,8 @@ instance : MonadStateOf DocElabM.State DocElabM := inferInstanceAs <| MonadState instance : MonadFinally DocElabM := inferInstanceAs <| MonadFinally (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) +instance : MonadEnv DocElabM := inferInstanceAs <| MonadEnv (ReaderT PartElabM.State (StateT DocElabM.State TermElabM)) + instance : MonadRecDepth DocElabM where withRecDepth n act := fun st st' => MonadRecDepth.withRecDepth n (act st st') getRecDepth := fun _ st' => do return (← MonadRecDepth.getRecDepth, st') diff --git a/src/verso/Verso/Parser.lean b/src/verso/Verso/Parser.lean index 8f87a6e..ce0ee9a 100644 --- a/src/verso/Verso/Parser.lean +++ b/src/verso/Verso/Parser.lean @@ -786,7 +786,11 @@ A linebreak that isn't a block break (that is, there's non-space content on the -/ def linebreak (ctxt : InlineCtxt) := if ctxt.allowNewlines then - nodeFn ``linebreak <| asStringFn <| atomicFn (chFn '\n' >> lookaheadFn (manyFn (chFn ' ') >> notFollowedByFn (chFn '\n' <|> blockOpener) "newline")) + nodeFn ``linebreak <| + andthenFn (fakeAtom "line!") <| + nodeFn strLitKind <| + asStringFn (quoted := true) <| + atomicFn (chFn '\n' >> lookaheadFn (manyFn (chFn ' ') >> notFollowedByFn (chFn '\n' <|> blockOpener) "newline")) else errorFn "Newlines not allowed here" @@ -1084,7 +1088,9 @@ info: Success! Final stack: (Verso.Syntax.bold "**" [(Verso.Syntax.text (str "\"aa\"")) - (Verso.Syntax.linebreak "\n") + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\"")) (Verso.Syntax.text (str "\"bb\""))] "**") All input consumed. @@ -1586,7 +1592,11 @@ mutual withCurrentColumn (fun c => many1Fn (descItem {ctxt with minIndent := c})) partial def para (ctxt : BlockCtxt) : ParserFn := - nodeFn ``para <| atomicFn (takeWhileFn (· == ' ') >> notFollowedByFn blockOpener "block opener" >> guardMinColumn ctxt.minIndent) >> textLine + nodeFn ``para <| + atomicFn (takeWhileFn (· == ' ') >> notFollowedByFn blockOpener "block opener" >> guardMinColumn ctxt.minIndent) >> + fakeAtom "para{" >> + textLine >> + fakeAtom "}" partial def header (ctxt : BlockCtxt) : ParserFn := nodeFn ``header <| @@ -1599,7 +1609,7 @@ mutual partial def codeBlock (ctxt : BlockCtxt) : ParserFn := nodeFn ``codeblock <| -- Opener - leaves indent info and open token on the stack - atomicFn (takeWhileFn (· == ' ') >> guardMinColumn ctxt.minIndent >> pushColumn >> asStringFn (atLeastFn 3 (skipChFn '`'))) >> + atomicFn (takeWhileFn (· == ' ') >> guardMinColumn ctxt.minIndent >> pushColumn >> asStringFn (atLeastFn 3 (skipChFn '`'))) >> withIndentColumn fun c => withCurrentColumn fun c' => let fenceWidth := c' - c @@ -1726,11 +1736,15 @@ end /-- info: Success! Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str - "\"This is just some textual content. How is it?\""))]) + "\"This is just some textual content. How is it?\""))] + "}") (Verso.Syntax.para - [(Verso.Syntax.text (str "\"More?\""))])] + "para{" + [(Verso.Syntax.text (str "\"More?\""))] + "}")] All input consumed. -/ #guard_msgs in @@ -1739,11 +1753,15 @@ All input consumed. /-- info: Success! Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"Newlines are preserved\"")) - (Verso.Syntax.linebreak "\n") + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\"")) (Verso.Syntax.text - (str "\"in paragraphs.\""))])] + (str "\"in paragraphs.\""))] + "}")] All input consumed. -/ #guard_msgs in @@ -1752,18 +1770,24 @@ All input consumed. /-- info: Success! Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str - "\"I can describe lists like this one:\""))]) + "\"I can describe lists like this one:\""))] + "}") (Verso.Syntax.ul [(Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"a\""))])]) + "para{" + [(Verso.Syntax.text (str "\"a\""))] + "}")]) (Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"b\""))])])])] + "para{" + [(Verso.Syntax.text (str "\"b\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -1773,6 +1797,7 @@ All input consumed. /-- info: Success! Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.image "![" "Lean logo" @@ -1780,11 +1805,14 @@ info: Success! Final stack: (Verso.Syntax.url "(" (str "\"/static/lean_logo.svg\"") - ")"))]) + ")"))] + "}") (Verso.Syntax.para + "para{" [(Verso.Syntax.text (str - "\"This is an example website/blog, for testing purposes.\""))])] + "\"This is an example website/blog, for testing purposes.\""))] + "}")] All input consumed. -/ #guard_msgs in @@ -1797,7 +1825,9 @@ info: Success! Final stack: (Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))])]) + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}")]) Remaining: "* bar\n" -/ @@ -1810,12 +1840,18 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))])]) + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}")]) (Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"bar\"")) - (Verso.Syntax.linebreak "\n")])])])] + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -1827,10 +1863,13 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"foo\"")) - (Verso.Syntax.linebreak "\n") - (Verso.Syntax.text - (str "\" thing\""))])])])] + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Verso.Syntax.text (str "\" thing\""))] + "}")])])] Remaining: "* bar\n" -/ @@ -1843,12 +1882,18 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "0") "+") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))])]) + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}")]) (Verso.Syntax.li (bullet (column "0") "+") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"bar\"")) - (Verso.Syntax.linebreak "\n")])])])] + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -1861,12 +1906,18 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))])]) + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}")]) (Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"bar\"")) - (Verso.Syntax.linebreak "\n")])])])] + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -1878,21 +1929,32 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"foo\"")) - (Verso.Syntax.linebreak "\n") - (Verso.Syntax.text (str "\" stuff\""))]) + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\"")) + (Verso.Syntax.text (str "\" stuff\""))] + "}") (Verso.Syntax.blockquote ">" [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"more \""))])]) + "para{" + [(Verso.Syntax.text (str "\"more \""))] + "}")]) (Verso.Syntax.para - [(Verso.Syntax.text (str "\"abc\""))])]) + "para{" + [(Verso.Syntax.text (str "\"abc\""))] + "}")]) (Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"bar\"")) - (Verso.Syntax.linebreak "\n")])])])] + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -1904,18 +1966,23 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))]) + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}") (Verso.Syntax.ul [(Verso.Syntax.li (bullet (column "2") "*") [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"bar\""))])])])]) + "para{" + [(Verso.Syntax.text (str "\"bar\""))] + "}")])])]) (Verso.Syntax.li (bullet (column "0") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"more outer\""))])])])] + (str "\"more outer\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -1929,7 +1996,9 @@ Final stack: ":" [(Verso.Syntax.text (str "\" an excellent idea\"")) - (Verso.Syntax.linebreak "\n") + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\"")) (Verso.Syntax.text (str "\"Let's say more!\""))] "=>" @@ -1949,8 +2018,10 @@ info: Success! Final stack: (str "\" an excellent idea\""))] "=>" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"Let's say more!\""))])])])] + (str "\"Let's say more!\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -1966,8 +2037,10 @@ Final stack: (str "\" an excellent idea\""))] "=>" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"Let's say more!\""))])]) + (str "\"Let's say more!\""))] + "}")]) (Verso.Syntax.desc ":" [(Verso.Syntax.text (str "\" more\""))] @@ -1990,18 +2063,21 @@ info: Success! Final stack: (str "\" an excellent idea\""))] "=>" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"Let's say more!\""))])]) + (str "\"Let's say more!\""))] + "}")]) (Verso.Syntax.desc ":" [(Verso.Syntax.text (str "\" more\""))] "=>" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"even more!\""))])])])] + (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!" @@ -2015,15 +2091,18 @@ info: Success! Final stack: (str "\" an excellent idea\""))] "=>" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"Let's say more!\""))])]) + (str "\"Let's say more!\""))] + "}")]) (Verso.Syntax.desc ":" [(Verso.Syntax.text (str "\" more\""))] "=>" [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"stuff\""))])])])] + "para{" + [(Verso.Syntax.text (str "\"stuff\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -2036,12 +2115,15 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "0") "1.") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"Hello\""))])]) + "para{" + [(Verso.Syntax.text (str "\"Hello\""))] + "}")]) (Verso.Syntax.li (bullet (column "0") "2.") [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"World\""))])])])] + "para{" + [(Verso.Syntax.text (str "\"World\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -2054,8 +2136,9 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "1") "1.") [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"Hello\""))])])])] + "para{" + [(Verso.Syntax.text (str "\"Hello\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -2068,15 +2151,17 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "0") "1.") [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"Hello\""))])])]) + "para{" + [(Verso.Syntax.text (str "\"Hello\""))] + "}")])]) (Verso.Syntax.ol (num "2") [(Verso.Syntax.li (bullet (column "1") "2.") [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"World\""))])])])] + "para{" + [(Verso.Syntax.text (str "\"World\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -2089,12 +2174,15 @@ info: Success! Final stack: [(Verso.Syntax.li (bullet (column "1") "1.") [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"Hello\""))])]) + "para{" + [(Verso.Syntax.text (str "\"Hello\""))] + "}")]) (Verso.Syntax.li (bullet (column "1") "2.") [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"World\""))])])])] + "para{" + [(Verso.Syntax.text (str "\"World\""))] + "}")])])] All input consumed. -/ #guard_msgs in @@ -2105,8 +2193,12 @@ info: Success! Final stack: [(Verso.Syntax.blockquote ">" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"hey\"")) - (Verso.Syntax.linebreak "\n")])])] + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\""))] + "}")])] All input consumed. -/ #guard_msgs in @@ -2115,7 +2207,9 @@ All input consumed. /-- info: Success! Final stack: [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"n*k \""))])] + "para{" + [(Verso.Syntax.text (str "\"n*k \""))] + "}")] All input consumed. -/ #guard_msgs in @@ -2126,6 +2220,7 @@ All input consumed. info: Failure: 1 underscores Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.bold "*" [(Verso.Syntax.text (str "\"This is \"")) @@ -2163,10 +2258,14 @@ info: Success! Final stack: [(Verso.Syntax.blockquote ">" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"Quotation\"")) - (Verso.Syntax.linebreak "\n") + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\"")) (Verso.Syntax.text - (str "\"and contained\""))])])] + (str "\"and contained\""))] + "}")])] All input consumed. -/ #guard_msgs in @@ -2177,10 +2276,14 @@ info: Success! Final stack: [(Verso.Syntax.blockquote ">" [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"Quotation\""))]) + "para{" + [(Verso.Syntax.text (str "\"Quotation\""))] + "}") (Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"and contained\""))])])] + (str "\"and contained\""))] + "}")])] All input consumed. -/ #guard_msgs in @@ -2191,11 +2294,14 @@ info: Success! Final stack: [(Verso.Syntax.blockquote ">" [(Verso.Syntax.para - [(Verso.Syntax.text - (str "\"Quotation\""))])]) + "para{" + [(Verso.Syntax.text (str "\"Quotation\""))] + "}")]) (Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"and not contained\""))])] + (str "\"and not contained\""))] + "}")] All input consumed. -/ #guard_msgs in @@ -2381,9 +2487,10 @@ info: Success! Final stack: [] "}" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str - "\"Here's a modified paragraph.\""))])]) + (str "\"Here's a modified paragraph.\""))] + "}")]) All input consumed. -/ #guard_msgs in @@ -2396,9 +2503,10 @@ info: Success! Final stack: [] "}" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str - "\"Here's a modified paragraph.\""))])]) + (str "\"Here's a modified paragraph.\""))] + "}")]) All input consumed. -/ #guard_msgs in @@ -2411,9 +2519,10 @@ info: Success! Final stack: [] "}" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str - "\"Here's a modified paragraph.\""))])]) + (str "\"Here's a modified paragraph.\""))] + "}")]) All input consumed. -/ #guard_msgs in @@ -2443,12 +2552,16 @@ info: Success! Final stack: [(Verso.Syntax.blockquote ">" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str - "\"Here's a modified blockquote\""))]) + "\"Here's a modified blockquote\""))] + "}") (Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"with multiple paras\""))])])]) + (str "\"with multiple paras\""))] + "}")])]) Remaining: "that ends" -/ @@ -2458,6 +2571,7 @@ Remaining: info: Failure: expected identifier Final stack: (Verso.Syntax.para + "para{" [(Verso.Syntax.role "{" )]) Remaining: "\ntest}\nHere's a modified paragraph." -/ @@ -2471,9 +2585,10 @@ info: Success! Final stack: [] "}" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str - "\"Here's a modified paragraph.\""))])]) + (str "\"Here's a modified paragraph.\""))] + "}")]) All input consumed. -/ #guard_msgs in @@ -2482,6 +2597,7 @@ All input consumed. info: Failure: expected identifier Final stack: (Verso.Syntax.para + "para{" [(Verso.Syntax.role "{" )]) Remaining: "\n test\narg}\nHere's a modified paragraph." -/ @@ -2495,9 +2611,10 @@ info: Success! Final stack: [(Verso.Syntax.anon `arg)] "}" [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str - "\"Here's a modified paragraph.\""))])]) + (str "\"Here's a modified paragraph.\""))] + "}")]) All input consumed. -/ #guard_msgs in @@ -2528,8 +2645,10 @@ info: Success! Final stack: (Term.optEllipsis []) "%%%") (Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"Text/paragraph!\""))])] + (str "\"Text/paragraph!\""))] + "}")] All input consumed. -/ #guard_msgs in @@ -2544,7 +2663,9 @@ info: Success! Final stack: "\n" "\n" [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))])] + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}")] "::::") All input consumed. -/ @@ -2563,7 +2684,9 @@ info: Success! Final stack: "\n" "\n" [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))])] + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}")] ":::") All input consumed. -/ @@ -2580,13 +2703,17 @@ info: Success! Final stack: "\n" "\n" [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))]) + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}") (Verso.Syntax.ul [(Verso.Syntax.li (bullet (column "2") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"List item \""))])])])] + (str "\"List item \""))] + "}")])])] ":::") All input consumed. -/ @@ -2602,13 +2729,17 @@ info: Success! Final stack: "\n" "\n" [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))]) + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}") (Verso.Syntax.ul [(Verso.Syntax.li (bullet (column "2") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"List item \""))])])])] + (str "\"List item \""))] + "}")])])] ":::") All input consumed. -/ @@ -2624,13 +2755,17 @@ info: Success! Final stack: "\n" "\n" [(Verso.Syntax.para - [(Verso.Syntax.text (str "\"foo\""))]) + "para{" + [(Verso.Syntax.text (str "\"foo\""))] + "}") (Verso.Syntax.ul [(Verso.Syntax.li (bullet (column "1") "*") [(Verso.Syntax.para + "para{" [(Verso.Syntax.text - (str "\"List item \""))])])])] + (str "\"List item \""))] + "}")])])] ":::") All input consumed. -/ @@ -2649,6 +2784,7 @@ Remaining: /-- info: Success! Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.link "[" [(Verso.Syntax.text (str "\"[link A]\""))] @@ -2665,7 +2801,8 @@ info: Success! Final stack: (Verso.Syntax.url "(" (str "\"https://more.example.com\"") - ")"))])] + ")"))] + "}")] All input consumed. -/ #guard_msgs in @@ -2675,6 +2812,7 @@ All input consumed. /-- info: Success! Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.link "[" [(Verso.Syntax.text (str "\"My link\""))] @@ -2682,7 +2820,8 @@ info: Success! Final stack: (Verso.Syntax.ref "[" (str "\"lean\"") - "]"))]) + "]"))] + "}") (Verso.Syntax.link_ref "[" (str "\"lean\"") @@ -2697,12 +2836,15 @@ All input consumed. info: Failure: expected ( or [ Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.link "[" [(Verso.Syntax.text (str "\"My link\""))] "]" (Verso.Syntax.ref "[" (str "\"lean\"") "]")) - (Verso.Syntax.linebreak "\n") + (Verso.Syntax.linebreak + "line!" + (str "\"\\n\"")) (Verso.Syntax.link "[" [(Verso.Syntax.text (str "\"lean\""))] @@ -2716,6 +2858,7 @@ Remaining: ": https://lean-lang.org" /-- info: Success! Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.link "[" [(Verso.Syntax.text (str "\"My link\""))] @@ -2723,14 +2866,17 @@ info: Success! Final stack: (Verso.Syntax.ref "[" (str "\"lean\"") - "]"))]) + "]"))] + "}") (Verso.Syntax.link_ref "[" (str "\"lean\"") "]:" (str "\"https://lean-lang.org\"")) (Verso.Syntax.para - [(Verso.Syntax.text (str "\"hello\""))])] + "para{" + [(Verso.Syntax.text (str "\"hello\""))] + "}")] All input consumed. -/ #guard_msgs in @@ -2739,11 +2885,13 @@ All input consumed. /-- info: Success! Final stack: [(Verso.Syntax.para + "para{" [(Verso.Syntax.text (str "\"Blah blah\"")) (Verso.Syntax.footnote "[^" (str "\"1\"") - "]")]) + "]")] + "}") (Verso.Syntax.footnote_ref "[^" (str "\"1\"") diff --git a/src/verso/Verso/Syntax.lean b/src/verso/Verso/Syntax.lean index 79363b8..5225349 100644 --- a/src/verso/Verso/Syntax.lean +++ b/src/verso/Verso/Syntax.lean @@ -34,7 +34,7 @@ syntax (name:=image) "image[" str* "]" link_target : inline /-- A footnote use -/ syntax (name:=footnote) "[^" str "]" : inline /-- Line break -/ -syntax (name:=linebreak) "line!" : inline +syntax (name:=linebreak) "line!" str : inline /-- Literal characters-/ syntax (name:=code) "code{" str "}" : inline syntax (name:=role) "role{" ident argument* "}" "[" inline "]" : inline @@ -57,7 +57,7 @@ syntax (name:=dl) "dl{" desc_item* "}" : block /-- Ordered list -/ syntax (name:=ol) "ol{" num list_item* "}" : block /-- Literal code -/ -syntax (name:=codeblock) str : block +syntax (name:=codeblock) "```" str "```" : block /-- Quotation -/ syntax (name:=blockquote) str : block /-- A link reference definition -/ diff --git a/src/verso/Verso/SyntaxUtils.lean b/src/verso/Verso/SyntaxUtils.lean index b4b6649..b75d351 100644 --- a/src/verso/Verso/SyntaxUtils.lean +++ b/src/verso/Verso/SyntaxUtils.lean @@ -51,6 +51,20 @@ defmethod ParserFn.test (p : ParserFn) (input : String) : IO String := do defmethod ParserFn.test! (p : ParserFn) (input : String) : IO Unit := p.test input >>= IO.println +defmethod ParserFn.parseString [Monad m] [MonadError m] [MonadEnv m] (p : ParserFn) (input : String) : m Syntax := do + let ictx := mkInputContext input "" + let env ← getEnv + let pmctx : ParserModuleContext := {env := env, options := {}} + let s' := p.run ictx pmctx (getTokenTable env) (mkParserState input) + let stk := s'.stxStack.extract 0 s'.stxStack.size + if let some err := s'.errorMsg then + throwError err.toString + if h : ¬stk.size = 1 then + throwError "Expected single item in parser stack, got {ppStack stk}" + else + have : stk.size = 1 := Classical.byContradiction h + have : 0 < stk.size := by simp_arith [*] + pure stk[0] scoped instance : Quote SourceInfo `term where quote