src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Sun Oct 22 19:40:28 2023 +0200
+++ b/src/Pure/Isar/token.ML	Mon Oct 23 12:08:38 2023 +0200
@@ -35,6 +35,7 @@
     Output of XML.body option
   val pos_of: T -> Position.T
   val adjust_offsets: (int -> int option) -> T -> T
+  val input_position: src -> string option
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -215,6 +216,9 @@
 fun adjust_offsets adjust (Token ((x, range), y, z)) =
   Token ((x, apply2 (Position.adjust_offsets adjust) range), y, z);
 
+fun input_position [] = NONE
+  | input_position (tok :: _) = SOME (Position.here (pos_of tok));
+
 
 (* stopper *)