fix: file end position for doc term

leanprover · Dec 6, 2024 · 51bfc32 · 51bfc32
1 parent 2b7f731
commit 51bfc32
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
@@ -127,9 +127,9 @@ 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:completeDocument eof:eoi : term => open Lean Elab Term PartElabM DocElabM in do
+elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:completeDocument eoi : term => open Lean Elab Term PartElabM DocElabM in do
   findGenreTm genre
-  let endPos := eof.raw.getTailPos?.get!
+  let endPos := (← getFileMap).source.endPos
   let .node _ _ blocks := text.raw
     | dbg_trace "nope {ppSyntax text.raw}" throwUnsupportedSyntax
   let ⟨`<low| [~_ ~(titleName@(.node _ _ titleParts))]>⟩ := title