# HG changeset patch
# User wenzelm
# Date 1758728496 -7200
# Node ID 37b61794a93aa5840b6e48a1dcc1a9b331a7d617
# Parent  1576fd83f1fe213249daab199d06f2cd3ab9062f
more informative Command_Span.Theory_Span;

diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/Build/build.scala
--- a/src/Pure/Build/build.scala	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/Build/build.scala	Wed Sep 24 17:41:36 2025 +0200
@@ -795,7 +795,7 @@
             yield i -> elem)
 
       val command =
-        Command.unparsed(thy_source, theory = true, id = id,
+        Command.unparsed(thy_source, theory_commands = Some(0), id = id,
           node_name = Document.Node.Name(thy_file, theory = theory_context.theory),
           blobs_info = Command.Blobs_Info.make(blobs),
           markups = markups, results = results)
diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Sep 24 17:41:36 2025 +0200
@@ -389,14 +389,14 @@
 
   def unparsed(
     source: String,
-    theory: Boolean = false,
+    theory_commands: Option[Int] = None,
     id: Document_ID.Command = Document_ID.none,
     node_name: Document.Node.Name = Document.Node.Name.empty,
     blobs_info: Blobs_Info = Blobs_Info.empty,
     results: Results = Results.empty,
     markups: Markups = Markups.empty
   ): Command = {
-    val span = Command_Span.unparsed(source, theory = theory)
+    val span = Command_Span.unparsed(source, theory_commands = theory_commands)
     new Command(id, node_name, blobs_info, span, source, results,
       Exports.empty, markups, Document_Status.Command_Status.empty)
   }
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)))
   }
 }
diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Sep 24 17:41:36 2025 +0200
@@ -1082,14 +1082,15 @@
     def begin_theory(
       node_name: Node.Name,
       id: Document_ID.Exec,
+      commands: Int,
       source: String,
       blobs_info: Command.Blobs_Info
     ): State = {
       if (theories.isDefinedAt(id)) fail
       else {
         val command =
-          Command.unparsed(source, theory = true, id = id, node_name = node_name,
-            blobs_info = blobs_info)
+          Command.unparsed(source, theory_commands = Some(commands), id = id,
+            node_name = node_name, blobs_info = blobs_info)
         copy(theories = theories + (id -> command.empty_state))
       }
     }
diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/PIDE/markup.ML	Wed Sep 24 17:41:36 2025 +0200
@@ -265,7 +265,7 @@
   val task_statistics: Properties.entry
   val command_timing: Properties.entry
   val session_timing: Properties.entry
-  val loading_theory: string -> Properties.T
+  val loading_theory: {name: string, commands: int} -> Properties.T
   val build_session_finished: Properties.T
   val print_operations: Properties.T
   val exportN: string
@@ -834,7 +834,8 @@
 
 val session_timing = function "session_timing";
 
-fun loading_theory name = [function "loading_theory", (nameN, name)];
+fun loading_theory {name, commands} =
+  [function "loading_theory", (nameN, name), ("commands", Value.print_int commands)];
 
 val build_session_finished = [function "build_session_finished"];
 
diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/PIDE/markup.scala	Wed Sep 24 17:41:36 2025 +0200
@@ -721,6 +721,7 @@
   }
   object Task_Statistics extends Properties_Function("task_statistics")
 
+  val Commands = new Properties.Int("commands")
   object Loading_Theory extends Properties_Function("loading_theory")
   object Build_Session_Finished extends Function("build_session_finished")
 
diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Sep 24 17:41:36 2025 +0200
@@ -23,12 +23,13 @@
   /* batch build */
 
   object Loading_Theory {
-    def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] =
+    def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec, Int)] =
       for {
         theory <- Markup.Name.unapply(props)
+        commands <- Markup.Commands.unapply(props)
         file <- Position.File.unapply(props) if Path.is_wellformed(file)
         id <- Position.Id.unapply(props)
-      } yield (Document.Node.Name(file, theory = theory), id)
+      } yield (Document.Node.Name(file, theory = theory), id, commands)
   }
 
 
diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Sep 24 17:41:36 2025 +0200
@@ -547,9 +547,11 @@
                 val entry = Export.Entry.make(Sessions.DRAFT, args, msg.chunk, cache)
                 change_command(_.add_export(id, (args.serial, entry)))
 
-              case Protocol.Loading_Theory(node_name, id) =>
+              case Protocol.Loading_Theory(node_name, id, commands) =>
                 val blobs_info = build_blobs_info(node_name)
-                try { global_state.change(_.begin_theory(node_name, id, msg.text, blobs_info)) }
+                try {
+                  global_state.change(_.begin_theory(node_name, id, commands, msg.text, blobs_info))
+                }
                 catch { case _: Document.State.Fail => bad_output() }
 
               case List(Markup.Commands_Accepted.THIS) =>
diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Sep 24 17:41:36 2025 +0200
@@ -290,7 +290,7 @@
 
 (* eval theory *)
 
-fun eval_thy options master_dir header text_pos text parents =
+fun eval_thy loading_theory options master_dir header text_pos text parents =
   let
     val (name, _) = #name header;
     val keywords =
@@ -298,6 +298,8 @@
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
 
     val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
+    val () = loading_theory (length spans);
+
     val elements = Thy_Element.parse_elements keywords spans;
     val command_ranges =
       Command_Span.command_ranges spans |> map (fn (pos, _) => (pos, Markup.command_range));
@@ -365,7 +367,9 @@
 
     val _ = remove_thy name;
     val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) [XML.blob [text]];
+    fun loading_theory commands =
+      Output.try_protocol_message
+        (Markup.loading_theory {name = name, commands = commands} @ text_props) [XML.blob [text]];
 
     val _ =
       Position.setmp_thread_data (Position.id_only id) (fn () =>
@@ -374,7 +378,7 @@
 
     val header = Thy_Header.make (name, put_id header_pos) imports keywords;
     val (theory, present) =
-      eval_thy options dir header text_pos text
+      eval_thy loading_theory options dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
     fun commit segments =
diff -r 1576fd83f1fe -r 37b61794a93a src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Sep 24 16:53:36 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Sep 24 17:41:36 2025 +0200
@@ -188,8 +188,8 @@
                   XML.Elem(Markup.Bad(Document_ID.make()),
                     XML.string("Changed sources for loaded theory " + quote(theory) +
                       ":\n" + cat_lines(changed.map(a => "  " + quote(a)))))
-                Command.unparsed(node.source, theory = true, id = command.id, node_name = node_name,
-                  blobs_info = command.blobs_info,
+                Command.unparsed(node.source, theory_commands = Some(0), id = command.id,
+                  node_name = node_name, blobs_info = command.blobs_info,
                   markups = Command.Markups.empty.add(Text.Info(node_range, msg)))
               }