fix for VersoManual.imports

Author: ejgallego

src/verso-manual/VersoManual/Imports.lean

@@ -32,7 +32,8 @@ Parses, but does not validate, a module header.
 def imports : CodeBlockExpanderOf ImportsParams
   | { «show» } , str => do
     let p := Parser.whitespace >> Parser.Module.header.fn
-    let headerStx ← parseStrLitWith p str
+    -- Provenance of `str` here is from Verso parser
+    let headerStx ← p.parseString str (versoStyle := true)
     let hl ← highlight headerStx #[] {}
     if «show» then
       ``(Block.other (Block.lean $(quote hl) {}) #[Block.code $(quote str.getString)])

src/verso/Verso/Parser.lean

@@ -985,6 +985,8 @@ namespace Verso.Doc.Concrete
 open Verso.Parser
 open Lean Elab Term
 
+-- Important! Both functions below expect strings in "Lean style",
+-- that is to say, with positions including quotes around the string.
 public def stringToInlines [Monad m] [MonadError m] [MonadLog m] [MonadOptions m] [MonadEnv m] [MonadQuotation m] (s : StrLit) : m (Array Syntax) :=
   withRef s do
     return (← textLine.parseString s).getArgs

src/verso/Verso/SyntaxUtils.lean

@@ -320,4 +320,11 @@ public def runParserCategory [Monad m] [MonadEnv m] [MonadLog m] [MonadOptions m
   (catName : Name) (input : StrLit) (versoStyle : Bool := true) (fileName : Option String := none) : m (Except String Syntax) :=
   runParserCategoryGen runParserCategory.toErrorMsg catName input versoStyle fileName
 
+/- This function can be used to check whether string are in Verso
+  style or in Lean style -/
+public def checkString (str : StrLit) : String :=
+  let s := str.getString
+  let sz := (str.raw.getTailPos?.getD 0 |>.byteIdx) - str.raw.getPos!.byteIdx
+  s!"real size: {s.length}, syntax size: {sz}"
+
 end Verso.SyntaxUtils