# HG changeset patch
# User wenzelm
# Date 1753801317 -7200
# Node ID fa8067dc67876a8ed1d0c4983b2fef1e2f532300
# Parent  eea4394dca0912d3c6eb934904c07eaee5492159
more markup for batch build: command ranges with trailing whitespace;

diff -r eea4394dca09 -r fa8067dc6787 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;
diff -r eea4394dca09 -r fa8067dc6787 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Jul 29 16:43:49 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Jul 29 17:01:57 2025 +0200
@@ -816,6 +816,7 @@
 
     /* command spans --- according to PIDE markup */
 
+    // Text.Info: core range
     def command_spans(range: Text.Range = Text.Range.full): List[Text.Info[Markup.Command_Span.Args]] =
       select(range, Markup.Elements(Markup.COMMAND_SPAN), _ =>
         {
@@ -823,6 +824,13 @@
             Some(Text.Info(range, args))
           case _ => None
         }).map(_.info)
+
+    // Text.Range: full source with trailing whitespace etc.
+    def command_range(caret_range: Text.Range): Option[Text.Range] =
+      select(caret_range, Markup.Elements(Markup.COMMAND_RANGE), _ =>
+        {
+          case Text.Info(range, _) => Some(range)
+        }).headOption.map(_.info)
   }
 
 
diff -r eea4394dca09 -r fa8067dc6787 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Tue Jul 29 16:43:49 2025 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Jul 29 17:01:57 2025 +0200
@@ -183,6 +183,7 @@
   val inputN: string val input: bool -> Properties.T -> T
   val command_keywordN: string val command_keyword: T
   val command_spanN: string val command_span: {name: string, kind: string, is_begin: bool} -> T
+  val command_rangeN: string val command_range: T
   val commandN: string val command_properties: T -> T
   val keywordN: string val keyword_properties: T -> T
   val stringN: string val string: T
@@ -664,6 +665,8 @@
 fun command_span {name, kind, is_begin} : T =
   (command_spanN, name_proper name @ kind_proper kind @ Properties.make_bool is_beginN is_begin);
 
+val (command_rangeN, command_range) = markup_elem "command_range";
+
 val commandN = "command"; val command_properties = properties [(kindN, commandN)];
 val keywordN = "keyword"; val keyword_properties = properties [(kindN, keywordN)];
 
diff -r eea4394dca09 -r fa8067dc6787 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Tue Jul 29 16:43:49 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Tue Jul 29 17:01:57 2025 +0200
@@ -464,6 +464,8 @@
       else None
   }
 
+  val COMMAND_RANGE = "command_range"
+
   val COMMAND = "command"
   val KEYWORD = "keyword"
   val KEYWORD1 = "keyword1"
diff -r eea4394dca09 -r fa8067dc6787 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 29 16:43:49 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 29 17:01:57 2025 +0200
@@ -300,6 +300,8 @@
 
     val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
     val elements = Thy_Element.parse_elements keywords spans;
+    val command_ranges =
+      Command_Span.command_ranges spans |> map (fn (pos, _) => (pos, Markup.command_range));
 
     val text_id = Position.copy_id text_pos Position.none;
 
@@ -307,6 +309,8 @@
 
     fun excursion () =
       let
+        val _ = Position.setmp_thread_data text_id (fn () => Position.reports command_ranges) ();
+
         fun element_result span_elem (st, _) =
           let
             fun prepare span =