src/Pure/Isar/token.ML

--- a/src/Pure/Isar/token.ML	Mon Oct 23 12:11:39 2023 +0200
+++ b/src/Pure/Isar/token.ML	Mon Oct 23 12:52:56 2023 +0200
@@ -36,6 +36,7 @@
   val pos_of: T -> Position.T
   val adjust_offsets: (int -> int option) -> T -> T
   val input_position: src -> string option
+  val context_input_position: Context.generic * src -> string option
   val eof: T
   val is_eof: T -> bool
   val not_eof: T -> bool
@@ -219,6 +220,9 @@
 fun input_position [] = NONE
   | input_position (tok :: _) = SOME (Position.here (pos_of tok));
 
+fun context_input_position (_: Context.generic, []) = NONE
+  | context_input_position (_, tok :: _) = SOME (Position.here (pos_of tok));
+
 
 (* stopper *)