src/Pure/PIDE/command_span.ML

--- a/src/Pure/PIDE/command_span.ML	Tue Jul 29 16:43:49 2025 +0200
+++ b/src/Pure/PIDE/command_span.ML	Tue Jul 29 17:01:57 2025 +0200
@@ -11,12 +11,14 @@
   datatype span = Span of kind * Token.T list
   val kind: span -> kind
   val content: span -> Token.T list
+  val range: span -> Position.range
   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
+  val command_ranges: span list -> Position.range list
 end;
 
 structure Command_Span: COMMAND_SPAN =
@@ -34,7 +36,8 @@
 
 fun kind (Span (k, _)) = k;
 fun content (Span (_, toks)) = toks;
-val symbol_length = Position.distance_of o Token.range_of o content;
+val range = Token.range_of o content;
+val symbol_length = Position.distance_of o range;
 
 
 (* stopper *)
@@ -57,4 +60,24 @@
 fun adjust_offsets adjust (Span (k, toks)) =
   Span (adjust_offsets_kind adjust k, map (Token.adjust_offsets adjust) toks);
 
+
+(* command ranges, including trailing non-commands (whitespace etc.) *)
+
+fun command_ranges spans =
+  let
+    fun ranges NONE [] result = rev result
+      | ranges (SOME pos) [] result =
+          let val end_pos = #2 (range (List.last spans))
+          in rev (Position.range (pos, end_pos) :: result) end
+      | ranges start_pos (span :: rest) result =
+          (case (start_pos, kind span) of
+            (NONE, Command_Span _) => ranges (SOME (#1 (range span))) rest result
+          | (SOME pos, Command_Span _) =>
+              let
+                val pos' = #1 (range span);
+                val result' = Position.range (pos, pos') :: result;
+              in ranges (SOME pos') rest result' end
+          | _ => ranges start_pos rest result);
+  in ranges NONE spans [] end;
+
 end;