feat: error recovery in parser

Now that Lean supports parser error recovery, Verso can too. The main
benefit is that parse errors in Verso documents recover by eating the
whole file, preventing Lean's error recovery from creating chaos. But
smaller elements also allow recovery, which is convenient.

examples/website/DemoSite/Blog/FirstPost.lean

@@ -21,10 +21,7 @@ def jsonHl : Highlighter where
 #defineLexerBlock json ← jsonHl
 
 #doc (Post) "First Post" =>
-%%%
-authors := ["Fictional Author"]
-date := {year := 2008, month := 2, day := 15}
-%%%
+
 
 This post introduces the blog and says what it will do.
 
@@ -35,3 +32,8 @@ Here is some syntax-highlighted JSON:
  "and numbers": 1.5,
  "and more": [true, false, null, {}]}
 ```
+
+And a random code block:
+```
+hello
+```

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4",
    "type": "git",
    "subDir": null,
-   "rev": "b1ebd72c5d262ea10a33ea582525925df874ad1e",
+   "rev": "a178ab58c07c37d919079ac3a5e4514fd85b791b",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing-2024-02-22",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "verso",

lakefile.lean

@@ -1,7 +1,7 @@
 import Lake
 open Lake DSL
 
-require std from git "https://github.com/leanprover/std4" @ "main"
+require std from git "https://github.com/leanprover/std4" @ "nightly-testing-2024-02-22"
 
 package verso where
   -- add package configuration options here

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:nightly-2024-02-22

src/verso-blog/Verso/Genre/Blog/Template.lean

@@ -135,8 +135,9 @@ def _root_.Array.mapIndexed (arr : Array α) (f : Fin arr.size → α → β) :
     if h : i < arr.size then
       go (acc.push (f ⟨i, h⟩ arr[i])) (i + 1)
     else acc
+  termination_by arr.size - i
   go #[] 0
-termination_by go acc i => arr.size - i
+
 
 partial defmethod Highlighted.toHtml : Highlighted → Html
   | .token t => t.toHtml

src/verso/Verso/Doc/Concrete.lean

@@ -70,6 +70,17 @@ def document : Parser where
 @[combinator_parenthesizer document] def document.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
 @[combinator_formatter document] def document.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
 
+/-- Advance the parser to EOF on failure so Lean doesn't try to parse further commands -/
+def completeDocument : Parser where
+  fn := rawFn <| atomicFn <| recoverFn Verso.Parser.document untilEoi
+where
+  untilEoi : RecoveryContext → ParserFn := fun _ c s =>
+    s.setPos c.input.endPos
+
+@[combinator_parenthesizer completeDocument] def completeDocument.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
+@[combinator_formatter completeDocument] def completeDocument.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
+
+
 partial def findGenre [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv m] [MonadError m] : Syntax → m Unit
   | `($g:ident) => discard <| resolveGlobalConstNoOverloadWithInfo g -- Don't allow it to become an auto-argument
   | `(($e)) => findGenre e
@@ -110,7 +121,7 @@ elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:docu
   elabCommand (← `(def $n : Part $genre := $(← finished.toSyntax genre st'.linkDefs st'.footnoteDefs)))
 
 
-elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : term => open Lean Elab Term PartElabM DocElabM in do
+elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eof:eoi : term => open Lean Elab Term PartElabM DocElabM in do
   findGenre genre
   let endPos := eof.raw.getTailPos?.get!
   let .node _ _ blocks := text.raw
@@ -141,7 +152,7 @@ def currentDocName [Monad m] [MonadEnv m] : m Name := do
   pure <| docName <| (← Lean.MonadEnv.getEnv).mainModule
 
 
-elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : command => open Lean Elab Term Command PartElabM DocElabM in do
+elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eof:eoi : command => open Lean Elab Term Command PartElabM DocElabM in do
   findGenre genre
   if eof.raw.isMissing then
     throwError "Syntax error prevents processing document"

src/verso/Verso/Doc/Elab.lean

@@ -262,13 +262,13 @@ partial def _root_.Verso.Syntax.header.command : PartCommand
 
 @[part_command Verso.Syntax.metadata_block]
 def _root_.Verso.Syntax.metadata_block.command : PartCommand
-  | `(block| %%%%$tk $fieldOrAbbrev* $ellipsis:optEllipsis %%%) => do
+  | `(block| %%%%$tk $fieldOrAbbrev*  %%%) => do
     let ctxt := (← getThe PartElabM.State).partContext
     if ctxt.blocks.size > 0 || ctxt.priorParts.size > 0 then
       throwErrorAt tk "Metadata blocks must precede both content and subsections"
     if ctxt.metadata.isSome then
       throwErrorAt tk "Metadata already provided for this section"
-    let stx ← `(term| { $(⟨fieldOrAbbrev⟩)* $ellipsis })
+    let stx ← `(term| { $fieldOrAbbrev* })
     modifyThe PartElabM.State fun st => {st with partContext.metadata := some stx}
   | _ => throwUnsupportedSyntax
 

src/verso/Verso/Method.lean

@@ -11,7 +11,7 @@ namespace Verso.Method
 open Lean Parser Elab Command
 
 def method := leading_parser
-  declModifiers false >> "defmethod " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving >> terminationSuffix
+  declModifiers false >> "defmethod " >> declId >> ppIndent optDeclSig >> declVal >> optDefDeriving
 
 /-- Like 'def', except the namespace is resolved to an existing unique
 name, and the resulting name is defined in that namespace.

src/verso/Verso/Output/Html.lean

@@ -49,8 +49,7 @@ def revFrom (i : Nat) (input : Array α) (output : Array α := #[]) : Array α :
   if h : i < input.size then
     revFrom (i+1) input (output.push input[i])
   else output
-termination_by
-  revFrom i input _ => input.size - i
+termination_by input.size - i
 
 namespace Html