diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/PIDE/command_span.scala	Wed Sep 24 17:41:36 2025 +0200
@@ -62,20 +62,26 @@
         case command: Command_Span => proper_string(command.name) getOrElse "<command>"
         case Ignored_Span => "<ignored>"
         case Malformed_Span => "<malformed>"
-        case Theory_Span => "<theory>"
+        case Theory_Span(_) => "<theory>"
       }
   }
   case class Command_Span(override val keyword_kind: Option[String], name: String, pos: Position.T)
     extends Kind
   case object Ignored_Span extends Kind
   case object Malformed_Span extends Kind
-  case object Theory_Span extends Kind
+  case class Theory_Span(commands: Int) extends Kind
 
 
   /* span */
 
   sealed case class Span(kind: Kind, content: List[Token]) {
-    def is_theory: Boolean = kind == Theory_Span
+    def is_theory: Boolean = kind.isInstanceOf[Theory_Span]
+
+    def theory_commands: Int =
+      kind match {
+        case Theory_Span(commands) => commands
+        case _ => 0
+      }
 
     def name: String =
       kind match { case k: Command_Span => k.name case _ => "" }
@@ -149,8 +155,12 @@
 
   val empty: Span = Span(Ignored_Span, Nil)
 
-  def unparsed(source: String, theory: Boolean = false): Span = {
-    val kind = if (theory) Theory_Span else Malformed_Span
+  def unparsed(source: String, theory_commands: Option[Int] = None): Span = {
+    val kind =
+      theory_commands match {
+        case Some(commands) => Theory_Span(commands)
+        case None => Malformed_Span
+      }
     Span(kind, List(Token(Token.Kind.UNPARSED, source)))
   }
 }