refactor: use Verso's runParserCategory function for string parsing

This is a step towards removing `parserInputString`. Upstream
`runParserCategory` always starts at `pos := 0`

Another option would be to update the upstream function to take this
into account, but the idea is that the function will evolve to take a
string literal so it should be able to compute the position by itself.

I made the types different (the Verso one is monadic) as to help avoid
confusion, and increase programming ergonomics.

Note that we don't change the parts `in VersoManual.Docstring` as
these are code strings that come from the `MD4Lean` and they don't
have an attached location.

Author: ejgallego

src/verso-blog/VersoBlog.lean

@@ -627,7 +627,7 @@ def leanInline : RoleExpanderOf LeanInlineConfig
         Elab.Term.withLevelNames us
       else id
 
-    match Parser.runParserCategory env `term altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `term altStr) with
     | .error e => throwErrorAt str e
     | .ok stx => withOptions (fun _ => opts) <| runWithOpenDecls scopes <| runWithVariables scopes fun _ => do
       let (newMsgs, type, tree) ← do
@@ -637,7 +637,7 @@ def leanInline : RoleExpanderOf LeanInlineConfig
           let (tree', t) ← do
 
             let expectedType ← config.type.mapM fun (s : StrLit) => do
-              match Parser.runParserCategory env `term s.getString (← getFileName) with
+              match (← SyntaxUtils.runParserCategory `term s.getString) with
               | .error e => throwErrorAt str e
               | .ok stx => withEnableInfoTree false do
                 let t ← leveller <| Elab.Term.elabType stx

src/verso-manual/VersoManual/InlineLean.lean

@@ -28,7 +28,7 @@ open Verso ArgParse Doc Elab Genre.Manual Html Code Highlighted.WebAssets Expect
 open Lean Elab
 open SubVerso.Highlighting
 
-open Verso.SyntaxUtils (parserInputString runParserCategory' SyntaxError)
+open Verso.SyntaxUtils (parserInputString SyntaxError)
 
 open Lean.Doc.Syntax
 open Lean.Elab.Tactic.GuardMsgs
@@ -356,7 +356,7 @@ def leanTerm : CodeBlockExpanderOf LeanInlineConfig
         Elab.Term.withLevelNames us
       else id
 
-    match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `term altStr) with
     | .error e => throwErrorAt str e
     | .ok stx =>
       let (newMsgs, tree) ← do
@@ -366,7 +366,7 @@ def leanTerm : CodeBlockExpanderOf LeanInlineConfig
 
           let tree' ← runWithOpenDecls <| runWithVariables fun _vars => do
             let expectedType ← config.type.mapM fun (s : StrLit) => do
-              match Parser.runParserCategory (← getEnv) `term s.getString (← getFileName) with
+              match (← SyntaxUtils.runParserCategory `term s.getString) with
               | .error e => throwErrorAt stx e
               | .ok stx => withEnableInfoTree false do
                 let t ← leveller <| Elab.Term.elabType stx
@@ -433,7 +433,7 @@ def leanInline : RoleExpanderOf LeanInlineConfig
         Elab.Term.withLevelNames us
       else id
 
-    match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `term altStr) with
     | .error e => throwErrorAt term e
     | .ok stx =>
 
@@ -444,7 +444,7 @@ def leanInline : RoleExpanderOf LeanInlineConfig
           let (tree', t) ← runWithOpenDecls <| runWithVariables fun _ => do
 
             let expectedType ← config.type.mapM fun (s : StrLit) => do
-              match Parser.runParserCategory (← getEnv) `term s.getString (← getFileName) with
+              match (← SyntaxUtils.runParserCategory `term s.getString) with
               | .error e => throwErrorAt term e
               | .ok stx => withEnableInfoTree false do
                 let t ← leveller <| Elab.Term.elabType stx
@@ -516,7 +516,7 @@ def inst : RoleExpanderOf LeanBlockConfig
       | throwErrorAt arg "Expected code literal with the example name"
     let altStr ← parserInputString term
 
-    match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `term altStr) with
     | .error e => throwErrorAt term e
     | .ok stx =>
       let (newMsgs, tree) ← do

src/verso-manual/VersoManual/InlineLean/Signature.lean

@@ -15,7 +15,7 @@ open SubVerso.Highlighting
 open Verso Genre Manual ArgParse Doc Elab
 open Verso Output Html
 open Verso Code Highlighted WebAssets
-open Verso.SyntaxUtils
+open Verso.SyntaxUtils (parserInputString)
 open Lean Elab
 
 namespace Verso.Genre.Manual.InlineLean
@@ -63,7 +63,7 @@ def signature : CodeBlockExpanderOf SignatureConfig
     let col? := (← getRef).getPos? |>.map (← getFileMap).utf8PosToLspPos |>.map (·.character)
 
 
-    match Parser.runParserCategory (← getEnv) `signature_spec altStr (← getFileName) with
+    match (← SyntaxUtils.runParserCategory `signature_spec altStr) with
     | .error e => throwError e
     | .ok stx =>
       let `(signature_spec|$[$kw]? $name:declId $sig:declSig) := stx

src/verso-manual/VersoManual/InlineLean/SyntaxError.lean

@@ -16,7 +16,7 @@ open SubVerso.Highlighting
 open Verso Genre Manual ArgParse Doc Elab
 open Verso Output Html
 open Verso Code Highlighted WebAssets
-open Verso.SyntaxUtils
+open Verso.SyntaxUtils (SyntaxError)
 open Lean Elab
 
 namespace Verso.Genre.Manual.InlineLean
@@ -140,7 +140,8 @@ def syntaxError : CodeBlockExpanderOf SyntaxErrorConfig
       (detail? := some "Syntax error")
 
     let s := str.getString
-    match runParserCategory' (← getEnv) (← getOptions) config.category s with
+    let errorFn := SyntaxUtils.runParserCategory.toSyntaxErrors
+    match (← SyntaxUtils.runParserCategoryGen (errorFn := errorFn) config.category s) with
     | .ok stx =>
       throwErrorAt str m!"Expected a syntax error for category {config.category}, but got {indentD stx}"
     | .error es =>

src/verso/Verso/SyntaxUtils.lean

@@ -169,7 +169,6 @@ deriving ToJson, FromJson, BEq, Repr, Quote
 
 
 -- Based on mkErrorMessage used in Lean upstream - keep them in synch for best UX
-open Lean.Parser in
 private partial def mkSyntaxError (c : InputContext) (pos : String.Pos.Raw) (stk : SyntaxStack) (e : Parser.Error) : SyntaxError := Id.run do
   let mut pos := pos
   let mut endPos? := none
@@ -219,49 +218,44 @@ public defmethod ParserFn.parseString [Monad m] [MonadError m] [MonadEnv m] (p :
   else
     pure stk[0]
 
+-- Default from upstream
+public def runParserCategory.toErrorMsg (ictx : InputContext) (s : ParserState) :=
+  s.toErrorMsg ictx
 
-open Lean.Parser in
-/--
-Runs a parser category, returning any errors encountered as a list of position-string pairs.
+-- Unused
+public def runParserCategory.toErrorMsgList (ictx : InputContext) (s : ParserState) : List (Position × String) := Id.run do
+  let mut errs := []
+  for (pos, _stk, err) in s.allErrors do
+    let pos := ictx.fileMap.toPosition pos
+    errs := (pos, toString err) :: errs
+  errs.reverse
+
+-- Used in Manual's syntaxError block
+public def runParserCategory.toSyntaxErrors (ictx : InputContext) (s : ParserState) : Array SyntaxError :=
+    s.allErrors.map fun (pos, stk, e) => (mkSyntaxError ictx pos stk e)
+
+/-- Runs a parser category, returning any errors encountered. It takes
+and optional `fileName` as callers in VersoManual/Docstring like to
+override it.
 -/
-public def runParserCategory
-    (env : Environment) (opts : Lean.Options) (catName : Name)
-    (input : String) (fileName : String := "<example>") :
-    Except (List (Position × String)) Syntax :=
+public def runParserCategoryGen [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m]
+  (errorFn : InputContext → ParserState → ε)
+  (catName : Name) (input : String) (fileName : Option String := none) : m (Except ε Syntax) := do
+  let fileName ← fileName.getDM getFileName
+  let env ← getEnv
+  let options ← getOptions
   let p := andthenFn whitespace (categoryParserFnImpl catName)
   let ictx := mkInputContext input fileName
-  let s := p.run ictx { env, options := opts } (getTokenTable env) (mkParserState input)
-  if !s.allErrors.isEmpty then
-    Except.error (toErrorMsg ictx s)
+  let s := p.run ictx { env, options } (getTokenTable env) (mkParserState input)
+  pure $ if !s.allErrors.isEmpty then
+    Except.error (errorFn ictx s)
   else if ictx.atEnd s.pos then
     Except.ok s.stxStack.back
   else
-    Except.error (toErrorMsg ictx (s.mkError "end of input"))
-where
-  toErrorMsg (ctx : InputContext) (s : ParserState) : List (Position × String) := Id.run do
-    let mut errs := []
-    for (pos, _stk, err) in s.allErrors do
-      let pos := ctx.fileMap.toPosition pos
-      errs := (pos, toString err) :: errs
-    errs.reverse
-
-open Lean.Parser in
-/--
-Runs a parser category, returning any errors encountered as `SyntaxError`s, with the source spans
-computed the way Lean does.
--/
-public def runParserCategory' (env : Environment) (opts : Lean.Options) (catName : Name) (input : String) (fileName : String := "<example>") : Except (Array SyntaxError) Syntax :=
-    let p := andthenFn whitespace (categoryParserFnImpl catName)
-    let ictx := mkInputContext input fileName
-    let s := p.run ictx { env, options := opts } (getTokenTable env) (mkParserState input)
-    if !s.allErrors.isEmpty then
-      Except.error <| toSyntaxErrors ictx s
-    else if ictx.atEnd s.pos then
-      Except.ok s.stxStack.back
-    else
-      Except.error (toSyntaxErrors ictx (s.mkError "end of input"))
-where
-  toSyntaxErrors (ictx : InputContext) (s : ParserState) : Array SyntaxError :=
-    s.allErrors.map fun (pos, stk, e) => (mkSyntaxError ictx pos stk e)
+    Except.error (errorFn ictx (s.mkError "end of input"))
+
+public def runParserCategory [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m]
+  (catName : Name) (input : String) (fileName : Option String := none) : m (Except String Syntax) :=
+  runParserCategoryGen runParserCategory.toErrorMsg catName input fileName
 
 end Verso.SyntaxUtils