From 51bfc32a6f1109b40f3520147a96dd41995ea15c Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 6 Dec 2024 15:27:29 +0100
Subject: [PATCH] fix: file end position for doc term

---
 src/verso/Verso/Doc/Concrete.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/verso/Verso/Doc/Concrete.lean b/src/verso/Verso/Doc/Concrete.lean
index 78f6926..e7542e0 100644
--- 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