--- 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)
--- 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)
}
--- 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)))
}
}
--- 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))
}
}
--- 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"];
--- 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")
--- 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)
}
--- 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) =>
--- 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 =
--- 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)))
}