src/Pure/PIDE/command_span.ML

--- a/src/Pure/PIDE/command_span.ML	Sun Jun 01 15:35:28 2025 +0200
+++ b/src/Pure/PIDE/command_span.ML	Sun Jun 01 16:43:09 2025 +0200
@@ -12,6 +12,9 @@
   val kind: span -> kind
   val content: span -> Token.T list
   val symbol_length: span -> int option
+  val eof: span
+  val is_eof: span -> bool
+  val stopper: span Scan.stopper
   val adjust_offsets_kind: (int -> int option) -> kind -> kind
   val adjust_offsets: (int -> int option) -> span -> span
 end;
@@ -34,6 +37,16 @@
 val symbol_length = Position.distance_of o Token.range_of o content;
 
 
+(* stopper *)
+
+val eof = Span (Command_Span ("", Position.none), []);
+
+fun is_eof (Span (Command_Span ("", _), _)) = true
+  | is_eof _ = false;
+
+val stopper = Scan.stopper (K eof) is_eof;
+
+
 (* presentation positions *)
 
 fun adjust_offsets_kind adjust k =