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 ← p.parseString 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

@@ -135,6 +135,10 @@ macro_rules
 end
 
 open Syntax in
+
+/-- get the inner start/end position of a string literal. If the
+ string is coming from Verso, this corresponds to the positions stored
+ in the syntax object, otherwise we must remove the quotes. -/
 def _root_.Lean.TSyntax.innerPos? (str : StrLit) (versoStyle : Bool) : Option (String.Pos.Raw × String.Pos.Raw) :=
   if versoStyle then
     match str.raw.getPos?, str.raw.getTailPos? with
@@ -265,5 +269,12 @@ 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