diff -r 10d6a6d43599 -r f033ff36d9c8 src/Pure/PIDE/command_span.ML
--- a/src/Pure/PIDE/command_span.ML	Thu Oct 16 11:45:29 2025 +0200
+++ b/src/Pure/PIDE/command_span.ML	Thu Oct 16 12:25:58 2025 +0200
@@ -10,6 +10,7 @@
   datatype kind = Command_Span of string * Position.T | Ignored_Span | Malformed_Span
   datatype span = Span of kind * Token.T list
   val kind: span -> kind
+  val is_ignored: span -> bool
   val content: span -> Token.T list
   val range: span -> Position.range
   val symbol_length: span -> int option
@@ -35,6 +36,7 @@
 datatype span = Span of kind * Token.T list;
 
 fun kind (Span (k, _)) = k;
+fun is_ignored span = kind span = Ignored_Span;
 fun content (Span (_, toks)) = toks;
 val range = Token.range_of o content;
 val symbol_length = Position.distance_of o range;