--- a/etc/options Wed Sep 24 17:50:30 2025 +0200
+++ b/etc/options Wed Sep 24 23:06:22 2025 +0200
@@ -212,14 +212,20 @@
option build_database_slice : real = 300 for build_sync
-- "slice size in MiB for ML heap stored within database"
+option build_progress : bool = false
+ -- "enabled detailed build progress"
+
+option build_progress_delay : real = 2
+ -- "delay for detailed build progress"
+
option build_delay : real = 0.2
- -- "delay build process main loop (local)"
+ -- "delay for build process main loop (local)"
option build_delay_master : real = 1.0
- -- "delay build process main loop (cluster master)"
+ -- "delay for build process main loop (cluster master)"
option build_delay_worker : real = 0.5
- -- "delay build process main loop (cluster worker)"
+ -- "delay for build process main loop (cluster worker)"
option build_cluster_expire : int = 50
-- "enforce database synchronization after given number of delay loops"
--- a/src/Pure/Build/build.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/Build/build.scala Wed Sep 24 23:06:22 2025 +0200
@@ -22,6 +22,16 @@
def engine_name(options: Options): String = options.string("build_engine")
+ /* detailed build progress */
+
+ class Build_Progress(options: Options, verbose: Boolean = false)
+ extends Console_Progress(verbose = verbose) {
+ override def nodes_status(nodes_status: Progress.Nodes_Status): Unit =
+ if (options.bool("build_progress")) {
+ output(nodes_status.message.copy(verbose = false))
+ }
+ }
+
/* context */
@@ -431,7 +441,7 @@
val sessions = getopts(args)
- val progress = new Console_Progress(verbose = verbose)
+ val progress = new Build_Progress(options, verbose = verbose)
val ml_settings = ML_Settings(options)
@@ -785,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/Build/build_job.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/Build/build_job.scala Wed Sep 24 23:06:22 2025 +0200
@@ -121,6 +121,10 @@
val options = Host.node_options(info.options, node_info)
val store = build_context.store
+ val build_progress_delay: Time = options.seconds("build_progress_delay")
+ val build_timing_threshold: Time = options.seconds("build_timing_threshold")
+ val editor_timing_threshold: Time = options.seconds("editor_timing_threshold")
+
using_optional(store.maybe_open_database_server(server = server)) { database_server =>
store.clean_output(database_server, session_name, session_init = true)
@@ -206,13 +210,48 @@
Export.consumer(store.open_database(session_name, output = true, server = server),
store.cache, progress = progress)
+ // mutable state: session.synchronized
val stdout = new StringBuilder(1000)
val stderr = new StringBuilder(1000)
val command_timings = new mutable.ListBuffer[Properties.T]
- val theory_timings = new mutable.ListBuffer[Properties.T]
val session_timings = new mutable.ListBuffer[Properties.T]
val runtime_statistics = new mutable.ListBuffer[Properties.T]
val task_statistics = new mutable.ListBuffer[Properties.T]
+ var nodes_changed = Set.empty[Document_ID.Generic]
+ var nodes_status = Document_Status.Nodes_Status.empty
+
+ val nodes_domain =
+ session_background.base.used_theories.map(_._1.symbolic_path)
+
+ def nodes_status_progress(): Unit = {
+ val state = session.get_state()
+ val result =
+ session.synchronized {
+ val nodes_status1 =
+ nodes_changed.foldLeft(nodes_status)({ case (status, state_id) =>
+ state.theory_snapshot(state_id, session.build_blobs) match {
+ case None => status
+ case Some(snapshot) =>
+ status.update_node(snapshot.state, snapshot.version, snapshot.node_name,
+ threshold = editor_timing_threshold)
+ }
+ })
+ val result =
+ if (nodes_changed.isEmpty) None
+ else {
+ Some(Progress.Nodes_Status(
+ nodes_domain, nodes_status1, session = session_name, old = Some(nodes_status)))
+ }
+
+ nodes_changed = Set.empty
+ nodes_status = nodes_status1
+
+ result
+ }
+ result.foreach(progress.nodes_status)
+ }
+
+ val nodes_delay = Delay.first(build_progress_delay) { nodes_status_progress() }
def fun(
name: String,
@@ -221,7 +260,7 @@
): (String, Session.Protocol_Function) = {
name -> ((msg: Prover.Protocol_Output) =>
unapply(msg.properties) match {
- case Some(props) => acc += props; true
+ case Some(props) => session.synchronized { acc += props }; true
case _ => false
})
}
@@ -270,18 +309,21 @@
Markup.Build_Session_Finished.name -> build_session_finished,
Markup.Loading_Theory.name -> loading_theory,
Markup.EXPORT -> export_,
- fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply))
})
session.command_timings += Session.Consumer("command_timings") {
- case Session.Command_Timing(props) =>
- for {
- elapsed <- Markup.Elapsed.unapply(props)
- elapsed_time = Time.seconds(elapsed)
- if elapsed_time.is_notable(options.seconds("build_timing_threshold"))
- } command_timings += props.filter(Markup.command_timing_property)
+ case Session.Command_Timing(state_id, props) =>
+ session.synchronized {
+ for {
+ elapsed <- Markup.Elapsed.unapply(props)
+ if Time.seconds(elapsed).is_notable(build_timing_threshold)
+ } command_timings += props.filter(Markup.command_timing_property)
+
+ nodes_changed += state_id
+ nodes_delay.invoke()
+ }
}
session.runtime_statistics += Session.Consumer("ML_statistics") {
@@ -330,10 +372,10 @@
if (msg.is_system) session.resources.log(Protocol.message_text(message))
if (msg.is_stdout) {
- stdout ++= Symbol.encode(XML.content(message))
+ session.synchronized { stdout ++= Symbol.encode(XML.content(message)) }
}
else if (msg.is_stderr) {
- stderr ++= Symbol.encode(XML.content(message))
+ session.synchronized { stderr ++= Symbol.encode(XML.content(message)) }
}
else if (msg.is_exit) {
val err =
@@ -392,6 +434,9 @@
session.stop()
+ nodes_delay.revoke()
+ nodes_status_progress()
+
val export_errors =
export_consumer.shutdown(close = true).map(Output.error_message_text)
@@ -424,24 +469,21 @@
/* process result */
val result1 = {
- val theory_timing =
- theory_timings.iterator.flatMap(
- {
- case props @ Markup.Name(name) => Some(name -> props)
- case _ => None
- }).toMap
- val used_theory_timings =
- for { (name, _) <- session_background.base.used_theories }
- yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))
+ val more_output =
+ session.synchronized {
+ val used_theory_timings =
+ nodes_domain.map(name =>
+ Markup.Name(name.theory) :::
+ Markup.Timing_Properties(nodes_status(name).total_timing))
- val more_output =
- Library.trim_line(stdout.toString) ::
- command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
- used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
- session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
- runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
- task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
- document_output
+ Library.trim_line(stdout.toString) ::
+ command_timings.toList.map(Protocol.Command_Timing_Marker.apply) :::
+ used_theory_timings.map(Protocol.Theory_Timing_Marker.apply) :::
+ session_timings.toList.map(Protocol.Session_Timing_Marker.apply) :::
+ runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) :::
+ task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
+ document_output
+ }
result0.output(more_output)
.error(Library.trim_line(stderr.toString))
--- a/src/Pure/Build/database_progress.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/Build/database_progress.scala Wed Sep 24 23:06:22 2025 +0200
@@ -311,7 +311,7 @@
override def output(message: Progress.Message): Unit = sync_context { _consumer.send(message) }
override def theory(theory: Progress.Theory): Unit = sync_context { _consumer.send(theory) }
- override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit =
+ override def nodes_status(nodes_status: Progress.Nodes_Status): Unit =
base_progress.nodes_status(nodes_status)
override def verbose: Boolean = base_progress.verbose
--- a/src/Pure/General/completion.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/General/completion.scala Wed Sep 24 23:06:22 2025 +0200
@@ -150,7 +150,7 @@
def apply(pos: Position.T, semantic: Semantic): XML.Elem = {
val elem =
semantic match {
- case No_Completion => XML.Elem(Markup(Markup.NO_COMPLETION, pos), Nil)
+ case No_Completion => XML.elem(Markup(Markup.NO_COMPLETION, pos))
case Names(total, names) =>
XML.Elem(Markup(Markup.COMPLETION, pos),
{
--- a/src/Pure/General/html.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/General/html.scala Wed Sep 24 23:06:22 2025 +0200
@@ -100,14 +100,14 @@
def link(path: Path, body: XML.Body): XML.Elem = link(path.implode, body)
def image(src: String, alt: String = ""): XML.Elem =
- XML.Elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList), Nil)
+ XML.elem(Markup("img", List("src" -> src) ::: proper_string(alt).map("alt" -> _).toList))
def source(body: XML.Body): XML.Elem = pre("source", body)
def source(src: String): XML.Elem = source(text(src))
def style(s: String): XML.Elem = XML.elem("style", text(s))
def style_file(href: String): XML.Elem =
- XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
+ XML.elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)))
def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
def script(s: String): XML.Elem = XML.elem("script", List(raw(text(s))))
--- a/src/Pure/General/timing.ML Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/General/timing.ML Wed Sep 24 23:06:22 2025 +0200
@@ -24,7 +24,6 @@
val is_relevant_time: Time.time -> bool
val is_relevant: timing -> bool
val message: timing -> string
- val protocol_message: string -> Position.T -> timing -> unit
val protocol: string -> Position.T -> ('a -> 'b) -> 'a -> 'b
end
@@ -106,16 +105,11 @@
fun timeap f x = timeit (fn () => f x);
fun timeap_msg msg f x = cond_timeit true msg (fn () => f x);
-fun protocol_message name pos t =
- if is_relevant t then
- let val props = Markup.command_timing :: (Markup.nameN, name) :: Position.properties_of pos
- in Output.try_protocol_message (props @ Markup.timing_properties t) [] end
- else ();
-
fun protocol name pos f x =
let
val (t, result) = timing (Exn.result f) x;
- val _ = protocol_message name pos t;
+ val props = Markup.command_timing :: (Markup.nameN, name) :: Position.properties_of pos;
+ val _ = Output.try_protocol_message (props @ Markup.timing_properties t) [];
in Exn.release result end;
end;
--- a/src/Pure/Isar/outer_syntax.ML Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed Sep 24 23:06:22 2025 +0200
@@ -229,9 +229,7 @@
let
val keywords = Thy_Header.get_keywords thy;
val tr0 =
- Toplevel.empty
- |> Toplevel.name name
- |> Toplevel.position pos
+ Toplevel.make name pos
|> Keyword.is_proof_open keywords name ? Toplevel.skip_proof_open
|> Keyword.is_proof_close keywords name ? Toplevel.skip_proof_close;
val command_markers =
@@ -291,7 +289,13 @@
let val name = Token.content_of tok in
(case lookup_commands thy name of
NONE => []
- | SOME cmd => [((Token.pos_of tok, command_markup {def = false} (name, cmd)), "")])
+ | SOME cmd =>
+ let
+ val pos = Token.pos_of tok;
+ val markup =
+ command_markup {def = false} (name, cmd)
+ |> Markup.command_offset (Position.offset_of pos);
+ in [((pos, markup), "")] end)
end
else [];
--- a/src/Pure/Isar/toplevel.ML Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Sep 24 23:06:22 2025 +0200
@@ -30,12 +30,12 @@
val pretty_abstract: state -> Pretty.T
type presentation = state -> Latex.text
type transition
+ val make: string -> Position.T -> transition
val empty: transition
val name_of: transition -> string
val pos_of: transition -> Position.T
val timing_of: transition -> Time.time
val type_error: transition -> string
- val name: string -> transition -> transition
val position: Position.T -> transition -> transition
val markers: Input.source list -> transition -> transition
val timing: Time.time -> transition -> transition
@@ -349,7 +349,8 @@
fun map_transition f (Transition {name, pos, markers, timing, trans}) =
make_transition (f (name, pos, markers, timing, trans));
-val empty = make_transition ("", Position.none, [], Time.zeroTime, []);
+fun make name pos = make_transition (name, pos, [], Time.zeroTime, []);
+val empty = make "" Position.none;
(* diagnostics *)
@@ -368,9 +369,6 @@
(* modify transitions *)
-fun name name = map_transition (fn (_, pos, markers, timing, trans) =>
- (name, pos, markers, timing, trans));
-
fun position pos = map_transition (fn (name, _, markers, timing, trans) =>
(name, pos, markers, timing, trans));
@@ -418,11 +416,8 @@
fun is_ignored tr = name_of tr = ignoredN;
fun is_malformed tr = name_of tr = malformedN;
-fun ignored pos =
- empty |> name ignoredN |> position pos |> keep (fn _ => ());
-
-fun malformed pos msg =
- empty |> name malformedN |> position pos |> keep (fn _ => error msg);
+fun ignored pos = make ignoredN pos |> keep (fn _ => ());
+fun malformed pos msg = make malformedN pos |> keep (fn _ => error msg);
(* theory transitions *)
--- a/src/Pure/PIDE/command.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/command.scala Wed Sep 24 23:06:22 2025 +0200
@@ -206,30 +206,23 @@
def merge(command: Command, states: List[State]): State =
State(command,
- status = states.flatMap(_.status),
results = merge_results(states),
exports = merge_exports(states),
markups = merge_markups(states))
def apply(
command: Command,
- status: List[Markup] = Nil,
results: Results = Results.empty,
exports: Exports = Exports.empty,
- markups: Markups = Markups.empty
+ markups: Markups = Markups.empty,
): State = {
- val document_status =
- Document_Status.Command_Status.make(
- markups = status,
- warned = results.warned,
- failed = results.failed)
- new State(command, status, results, exports, markups, document_status)
+ new State(command, results, exports, markups,
+ Document_Status.Command_Status.make(warned = results.warned, failed = results.failed))
}
}
- final class State private(
+ final class State private[Command](
val command: Command,
- val status: List[Markup],
val results: Results,
val exports: Exports,
val markups: Markups,
@@ -243,7 +236,7 @@
def consolidating: Boolean = document_status.consolidating
def consolidated: Boolean = document_status.consolidated
def maybe_consolidated: Boolean = document_status.maybe_consolidated
- def timing: Timing = document_status.timing
+ def timings: Document_Status.Command_Timings = document_status.timings
def markup(index: Markup_Index): Markup_Tree = markups(index)
@@ -253,9 +246,13 @@
else Some(State(other_command, markups = markups1))
}
+ def exit(id: Document_ID.Generic): Command =
+ new Command(id, command.node_name, command.blobs_info, command.span, command.source,
+ results, exports, markups, document_status)
+
private def add_status(st: Markup): State = {
val document_status1 = document_status.update(markups = List(st))
- new State(command, st :: status, results, exports, markups, document_status1)
+ new State(command, results, exports, markups, document_status1)
}
private def add_result(entry: Results.Entry): State = {
@@ -263,12 +260,12 @@
document_status.update(
warned = Results.warned(entry),
failed = Results.failed(entry))
- new State(command, status, results + entry, exports, markups, document_status1)
+ new State(command, results + entry, exports, markups, document_status1)
}
def add_export(entry: Exports.Entry): Option[State] =
if (command.node_name.theory == entry._2.theory_name) {
- Some(new State(command, status, results, exports + entry, markups, document_status))
+ Some(new State(command, results, exports + entry, markups, document_status))
}
else None
@@ -282,7 +279,7 @@
markups.add(Markup_Index(true, chunk_name), m)
else markups
val markups2 = markups1.add(Markup_Index(false, chunk_name), m)
- new State(command, this.status, results, exports, markups2, document_status)
+ new State(command, results, exports, markups2, document_status)
}
def accumulate(
@@ -292,6 +289,8 @@
message: XML.Elem,
cache: XML.Cache): State =
message match {
+ case XML.Elem(markup @ Markup(Markup.TIMING, _), _) => add_status(markup)
+
case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
if (command.span.is_theory) this
else {
@@ -381,7 +380,8 @@
span: Command_Span.Span
): Command = {
val (source, span1) = span.compact_source
- new Command(id, node_name, blobs_info, span1, source, Results.empty, Markups.empty)
+ new Command(id, node_name, blobs_info, span1, source,
+ Results.empty, Exports.empty, Markups.empty, Document_Status.Command_Status.empty)
}
val empty: Command =
@@ -389,15 +389,16 @@
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)
- new Command(id, node_name, blobs_info, span, source, results, markups)
+ 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)
}
@@ -483,7 +484,9 @@
val span: Command_Span.Span,
val source: String,
val init_results: Command.Results,
- val init_markups: Command.Markups
+ val init_exports: Command.Exports,
+ val init_markups: Command.Markups,
+ val init_document_status: Document_Status.Command_Status
) {
override def toString: String = id.toString + "/" + span.kind.toString
@@ -618,7 +621,8 @@
/* accumulated results */
lazy val init_state: Command.State =
- Command.State(this, results = init_results, markups = init_markups)
+ new Command.State(this, init_results, init_exports, init_markups,
+ init_document_status.update(warned = init_results.warned, failed = init_results.failed))
lazy val empty_state: Command.State = Command.State(this)
}
--- a/src/Pure/PIDE/command_span.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/command_span.scala Wed Sep 24 23:06:22 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 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/document.scala Wed Sep 24 23:06:22 2025 +0200
@@ -135,6 +135,8 @@
def path: Path = Path.explode(File.standard_path(node))
+ def symbolic_path: Name = Name(File.symbolic_path(path), theory)
+
def master_dir: String = Url.strip_base_name(node).getOrElse("")
def is_theory: Boolean = theory.nonEmpty
@@ -321,6 +323,10 @@
def load_commands_changed(doc_blobs: Blobs): Boolean =
load_commands.exists(_.blobs_changed(doc_blobs))
+ def get_theory: Option[Command] =
+ if (commands.size == 1 && commands.last.span.is_theory) Some(commands.last)
+ else None
+
def update_header(new_header: Node.Header): Node =
new Node(get_blob, new_header, syntax, text_perspective, perspective, _commands)
@@ -1080,14 +1086,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))
}
}
@@ -1096,16 +1103,15 @@
theories.get(id) match {
case None => fail
case Some(st) =>
- val command = st.command
- val node_name = command.node_name
- val doc_blobs = document_blobs(node_name)
- val command1 =
- Command.unparsed(command.source, theory = true, id = id, node_name = node_name,
- blobs_info = command.blobs_info, results = st.results, markups = st.markups)
+ val command1 = st.exit(id)
+ val doc_blobs = document_blobs(command1.node_name)
val state1 = copy(theories = theories - id)
(state1.snippet(List(command1), doc_blobs), state1)
}
+ def theory_snapshot(id: Document_ID.Exec, document_blobs: Node.Name => Blobs): Option[Snapshot] =
+ if (theories.isDefinedAt(id)) Some(end_theory(id, document_blobs)._1) else None
+
def assign(
id: Document_ID.Version,
edited: List[String],
@@ -1270,9 +1276,6 @@
Document_Status.Command_Status.merge(
command_states(version, command).iterator.map(_.document_status))
- def command_timing(version: Version, command: Command): Timing =
- Timing.merge(command_states(version, command).iterator.map(_.timing))
-
def command_results(version: Version, command: Command): Command.Results =
Command.State.merge_results(command_states(version, command))
--- a/src/Pure/PIDE/document_status.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/document_status.scala Wed Sep 24 23:06:22 2025 +0200
@@ -7,6 +7,9 @@
package isabelle
+import scala.collection.immutable.SortedMap
+
+
object Document_Status {
/* theory status: via 'theory' or 'end' commands */
@@ -30,6 +33,48 @@
}
+ /* command timings: for pro-forma command with actual commands at offset */
+
+ object Command_Timings {
+ type Entry = (Symbol.Offset, Timing)
+ val empty: Command_Timings =
+ new Command_Timings(SortedMap.empty, Timing.zero)
+ def make(args: IterableOnce[Entry]): Command_Timings =
+ args.iterator.foldLeft(empty)(_ + _)
+ def merge(args: IterableOnce[Command_Timings]): Command_Timings =
+ args.iterator.foldLeft(empty)(_ ++ _)
+ }
+
+ final class Command_Timings private(
+ private val rep: SortedMap[Symbol.Offset, Timing],
+ val sum: Timing
+ ) {
+ def is_empty: Boolean = rep.isEmpty
+ def count: Int = rep.size
+ def apply(offset: Symbol.Offset): Timing = rep.getOrElse(offset, Timing.zero)
+ def iterator: Iterator[(Symbol.Offset, Timing)] = rep.iterator
+
+ def + (entry: Command_Timings.Entry): Command_Timings = {
+ val (offset, timing) = entry
+ val rep1 = rep + (offset -> (apply(offset) + timing))
+ val sum1 = sum + timing
+ new Command_Timings(rep1, sum1)
+ }
+
+ def ++ (other: Command_Timings): Command_Timings =
+ if (rep.isEmpty) other
+ else other.rep.foldLeft(this)(_ + _)
+
+ override def hashCode: Int = rep.hashCode
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Command_Timings => rep == other.rep
+ case _ => false
+ }
+ override def toString: String = rep.mkString("Command_Timings(", ", ", ")")
+ }
+
+
/* command status */
object Command_Status {
@@ -53,7 +98,7 @@
var canceled = false
var forks = 0
var runs = 0
- var timing = Timing.zero
+ var timings = Command_Timings.empty
for (markup <- markups) {
markup.name match {
case Markup.INITIALIZED =>
@@ -72,10 +117,11 @@
case Markup.WARNING | Markup.LEGACY => warned1 = true
case Markup.FAILED | Markup.ERROR => failed1 = true
case Markup.CANCELED => canceled = true
- case _ =>
- }
- markup match {
- case Markup.Timing(t) => timing += t
+ case Markup.TIMING =>
+ val props = markup.properties
+ val offset = Position.Offset.get(props)
+ val timing = Markup.Timing_Properties.get(props)
+ timings += (offset -> timing)
case _ =>
}
}
@@ -88,7 +134,7 @@
canceled = canceled,
forks = forks,
runs = runs,
- timing = timing)
+ timings = timings)
}
val empty: Command_Status = make()
@@ -106,7 +152,7 @@
private val canceled: Boolean,
val forks: Int,
val runs: Int,
- val timing: Timing
+ val timings: Command_Timings
) extends Theory_Status {
override def toString: String =
if (is_empty) "Command_Status.empty"
@@ -117,7 +163,7 @@
def is_empty: Boolean =
!Theory_Status.initialized(theory_status) &&
!touched && !accepted && !warned && !failed && !canceled &&
- forks == 0 && runs == 0 && timing.is_zero
+ forks == 0 && runs == 0 && timings.is_empty
def + (that: Command_Status): Command_Status =
if (is_empty) that
@@ -132,7 +178,7 @@
canceled = canceled || that.canceled,
forks = forks + that.forks,
runs = runs + that.runs,
- timing = timing + that.timing)
+ timings = timings ++ that.timings)
}
def update(
@@ -154,7 +200,7 @@
canceled = canceled,
forks = forks,
runs = runs,
- timing = timing)
+ timings = timings)
}
}
else this + Command_Status.make(markups = markups, warned = warned, failed = failed)
@@ -183,6 +229,9 @@
name: Document.Node.Name,
threshold: Time = Time.max
): Node_Status = {
+ val node = version.nodes(name)
+
+ var theory_status = Document_Status.Theory_Status.NONE
var unprocessed = 0
var running = 0
var warned = 0
@@ -190,14 +239,15 @@
var finished = 0
var canceled = false
var terminated = true
- var total_time = Time.zero
+ var total_timing = Timing.zero
var max_time = Time.zero
- var command_timings = Map.empty[Command, Time]
- var theory_status = Document_Status.Theory_Status.NONE
+ var command_timings = Map.empty[Command, Command_Timings]
- for (command <- version.nodes(name).commands.iterator) {
+ for (command <- node.commands.iterator) {
val status = state.command_status(version, command)
+ theory_status = Theory_Status.merge(theory_status, status.theory_status)
+
if (status.is_running) running += 1
else if (status.is_failed) failed += 1
else if (status.is_warned) warned += 1
@@ -207,15 +257,32 @@
if (status.is_canceled) canceled = true
if (!status.is_terminated) terminated = false
- val t = state.command_timing(version, command).elapsed
- total_time += t
+ val t = status.timings.sum.elapsed
+ total_timing += status.timings.sum
if (t > max_time) max_time = t
- if (t.is_notable(threshold)) command_timings += (command -> t)
+ if (t.is_notable(threshold)) command_timings += (command -> status.timings)
+ }
+
+ def percent(a: Int, b: Int): Int =
+ if (b == 0) 0 else ((a.toDouble / b) * 100).toInt
- theory_status = Theory_Status.merge(theory_status, status.theory_status)
+ val percentage: Int = {
+ node.get_theory match {
+ case None =>
+ if (Theory_Status.consolidated(theory_status)) 100
+ else {
+ val total = unprocessed + running + warned + failed + finished
+ percent(total - unprocessed, total).min(99)
+ }
+ case Some(command) =>
+ val total = command.span.theory_commands
+ val processed = state.command_status(version, command).timings.count
+ percent(processed, total)
+ }
}
Node_Status(
+ theory_status = theory_status,
suppressed = version.nodes.suppressed(name),
unprocessed = unprocessed,
running = running,
@@ -224,15 +291,16 @@
finished = finished,
canceled = canceled,
terminated = terminated,
- total_time = total_time,
+ total_timing = total_timing,
max_time = max_time,
threshold = threshold,
command_timings = command_timings,
- theory_status = theory_status)
+ percentage)
}
}
sealed case class Node_Status(
+ theory_status: Theory_Status.Value = Theory_Status.NONE,
suppressed: Boolean = false,
unprocessed: Int = 0,
running: Int = 0,
@@ -241,11 +309,11 @@
finished: Int = 0,
canceled: Boolean = false,
terminated: Boolean = false,
- total_time: Time = Time.zero,
+ total_timing: Timing = Timing.zero,
max_time: Time = Time.zero,
threshold: Time = Time.zero,
- command_timings: Map[Command, Time] = Map.empty,
- theory_status: Theory_Status.Value = Theory_Status.NONE,
+ command_timings: Map[Command, Command_Timings] = Map.empty,
+ percentage: Int = 0
) extends Theory_Status {
def is_empty: Boolean = this == Node_Status.empty
@@ -254,11 +322,6 @@
def quasi_consolidated: Boolean = !suppressed && !finalized && terminated
- def percentage: Int =
- if (consolidated) 100
- else if (total == 0) 0
- else (((total - unprocessed).toDouble / total) * 100).toInt min 99
-
def json: JSON.Object.T =
JSON.Object("ok" -> ok, "total" -> total, "unprocessed" -> unprocessed,
"running" -> running, "warned" -> warned, "failed" -> failed, "finished" -> finished,
@@ -272,26 +335,15 @@
enum Overall_Status { case ok, failed, pending }
object Nodes_Status {
- val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
+ val empty: Nodes_Status = new Nodes_Status(Map.empty)
}
- final class Nodes_Status private(
- private val rep: Map[Document.Node.Name, Node_Status],
- nodes: Document.Nodes
- ) {
+ final class Nodes_Status private(private val rep: Map[Document.Node.Name, Node_Status]) {
def is_empty: Boolean = rep.isEmpty
def apply(name: Document.Node.Name): Node_Status = rep.getOrElse(name, Node_Status.empty)
def get(name: Document.Node.Name): Option[Node_Status] = rep.get(name)
-
def iterator: Iterator[(Document.Node.Name, Node_Status)] = rep.iterator
- def present(
- domain: Option[List[Document.Node.Name]] = None
- ): List[(Document.Node.Name, Node_Status)] = {
- for (name <- domain.getOrElse(nodes.topological_order))
- yield name -> apply(name)
- }
-
def quasi_consolidated(name: Document.Node.Name): Boolean =
get(name) match {
case Some(st) => st.quasi_consolidated
@@ -305,26 +357,32 @@
case _ => Overall_Status.pending
}
- def update(
+ def update_node(
+ state: Document.State,
+ version: Document.Version,
+ name: Document.Node.Name,
+ threshold: Time = Time.max
+ ): Nodes_Status = {
+ val node_status = Document_Status.Node_Status.make(state, version, name, threshold = threshold)
+ new Nodes_Status(rep + (name -> node_status))
+ }
+
+ def update_nodes(
resources: Resources,
state: Document.State,
version: Document.Version,
threshold: Time = Time.max,
domain: Option[Set[Document.Node.Name]] = None,
trim: Boolean = false
- ): (Boolean, Nodes_Status) = {
- val nodes1 = version.nodes
- val update_iterator =
- for {
- name <- domain.getOrElse(nodes1.domain).iterator
- if !Resources.hidden_node(name) && !resources.loaded_theory(name)
- st = Document_Status.Node_Status.make(state, version, name, threshold = threshold)
- if apply(name) != st
- } yield (name -> st)
- val rep1 = rep ++ update_iterator
- val rep2 = if (trim) rep1 -- rep1.keysIterator.filterNot(nodes1.domain) else rep1
-
- (rep != rep2, new Nodes_Status(rep2, nodes1))
+ ): Nodes_Status = {
+ val domain1 = version.nodes.domain
+ val that =
+ domain.getOrElse(domain1).iterator.foldLeft(this)(
+ { case (a, name) =>
+ if (Resources.hidden_node(name) || resources.loaded_theory(name)) a
+ else a.update_node(state, version, name, threshold = threshold) })
+ if (trim) new Nodes_Status(that.rep -- that.rep.keysIterator.filterNot(domain1))
+ else that
}
override def hashCode: Int = rep.hashCode
--- a/src/Pure/PIDE/headless.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/headless.scala Wed Sep 24 23:06:22 2025 +0200
@@ -140,10 +140,10 @@
domain: Option[Set[Document.Node.Name]] = None,
trim: Boolean = false
): (Boolean, Use_Theories_State) = {
- val (nodes_status_changed, nodes_status1) =
- nodes_status.update(resources, state, version, domain = domain, trim = trim)
+ val nodes_status1 =
+ nodes_status.update_nodes(resources, state, version, domain = domain, trim = trim)
val st1 = copy(last_update = Time.now(), nodes_status = nodes_status1)
- (nodes_status_changed, st1)
+ (nodes_status1 != nodes_status, st1)
}
def changed(
@@ -351,7 +351,9 @@
val consumer = {
val delay_nodes_status =
Delay.first(nodes_status_delay max Time.zero) {
- progress.nodes_status(use_theories_state.value.nodes_status)
+ val st = use_theories_state.value
+ progress.nodes_status(
+ Progress.Nodes_Status(st.dep_graph.topological_order, st.nodes_status))
}
val delay_commit_clean =
@@ -390,7 +392,8 @@
val theory_progress =
(for {
- (name, node_status) <- st1.nodes_status.present().iterator
+ name <- st1.dep_graph.topological_order.iterator
+ node_status = st1.nodes_status(name)
if !node_status.is_empty && changed_st.changed_nodes(name) &&
!st.already_committed.isDefinedAt(name)
p1 = node_status.percentage
--- a/src/Pure/PIDE/markup.ML Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/markup.ML Wed Sep 24 23:06:22 2025 +0200
@@ -206,9 +206,9 @@
val cpuN: string
val gcN: string
val timing_properties: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> Properties.T
+ val command_offsetN: string val command_offset: int option -> T -> T
val parse_command_timing_properties:
Properties.T -> ({file: string, offset: int, name: string} * Time.time) option
- val timingN: string val timing: {elapsed: Time.time, cpu: Time.time, gc: Time.time} -> T
val command_indentN: string val command_indent: int -> T
val goalN: string val goal: T
val subgoalN: string val subgoal: string -> T
@@ -264,9 +264,8 @@
val cancel_scala: string -> Properties.T
val task_statistics: Properties.entry
val command_timing: Properties.entry
- val theory_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
@@ -714,12 +713,14 @@
(cpuN, Time.print cpu),
(gcN, Time.print gc)];
-val timingN = "timing";
-fun timing t = (timingN, timing_properties t);
-
(* command timing *)
+val command_offsetN = "command_offset";
+fun command_offset offset =
+ let val i = the_default 0 offset
+ in if i = 0 then I else properties [(command_offsetN, Value.print_int i)] end;
+
fun parse_command_timing_properties props =
(case (Properties.get props fileN, Properties.get props offsetN, Properties.get props nameN) of
(SOME file, SOME offset, SOME name) =>
@@ -831,11 +832,10 @@
val command_timing = function "command_timing";
-val theory_timing = function "theory_timing";
-
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 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/markup.scala Wed Sep 24 23:06:22 2025 +0200
@@ -513,22 +513,16 @@
case _ => None
}
- def get(props: Properties.T): isabelle.Timing =
- unapply(props).getOrElse(isabelle.Timing.zero)
+ def get(props: Properties.T): isabelle.Timing = {
+ val elapsed = Time.seconds(Elapsed.get(props))
+ val cpu = Time.seconds(CPU.get(props))
+ val gc = Time.seconds(GC.get(props))
+ isabelle.Timing(elapsed, cpu, gc)
+ }
}
val TIMING = "timing"
- object Timing {
- def apply(timing: isabelle.Timing): Markup = Markup(TIMING, Timing_Properties(timing))
-
- def unapply(markup: Markup): Option[isabelle.Timing] =
- markup match {
- case Markup(TIMING, Timing_Properties(timing)) => Some(timing)
- case _ => None
- }
- }
-
/* process result */
@@ -542,8 +536,7 @@
def unapply(props: Properties.T): Option[Process_Result] =
props match {
case Return_Code(rc) =>
- val timing = Timing_Properties.unapply(props).getOrElse(isabelle.Timing.zero)
- Some(isabelle.Process_Result(rc, timing = timing))
+ Some(isabelle.Process_Result(rc, timing = Timing_Properties.get(props)))
case _ => None
}
}
@@ -718,16 +711,17 @@
}
}
+ val Command_Offset = new Properties.Int("command_offset")
val command_timing_properties: Set[String] = Set(FILE, OFFSET, NAME, Elapsed.name)
def command_timing_property(entry: Properties.Entry): Boolean = command_timing_properties(entry._1)
object Command_Timing extends Properties_Function("command_timing")
- object Theory_Timing extends Properties_Function("theory_timing")
object Session_Timing extends Properties_Function("session_timing") {
val Threads = new Properties.Int("threads")
}
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/markup_tree.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/markup_tree.scala Wed Sep 24 23:06:22 2025 +0200
@@ -76,7 +76,7 @@
case List(XML.Wrapped_Elem(markup1, body1, body2)) =>
strip_elems(XML.Elem(markup1, body1) :: elems, body2)
case List(XML.Elem(markup1, body1)) =>
- strip_elems(XML.Elem(markup1, Nil) :: elems, body1)
+ strip_elems(XML.elem(markup1) :: elems, body1)
case _ => (elems, body)
}
--- a/src/Pure/PIDE/protocol.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/protocol.scala Wed Sep 24 23:06:22 2025 +0200
@@ -23,12 +23,13 @@
/* batch build */
object Loading_Theory {
- def unapply(props: Properties.T): Option[(Document.Node.Name, Document_ID.Exec)] =
- (props, props, props) match {
- case (Markup.Name(theory), Position.File(file), Position.Id(id))
- if Path.is_wellformed(file) => Some((Document.Node.Name(file, theory = theory), id))
- case _ => None
- }
+ 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, commands)
}
@@ -78,28 +79,9 @@
/* command timing */
object Command_Timing {
- def unapply(props: Properties.T): Option[(Properties.T, Document_ID.Generic, isabelle.Timing)] =
+ def unapply(props: Properties.T): Option[(Document_ID.Generic, Properties.T)] =
props match {
- case Markup.Command_Timing(args) =>
- (args, args) match {
- case (Position.Id(id), Markup.Timing_Properties(timing)) => Some((args, id, timing))
- case _ => None
- }
- case _ => None
- }
- }
-
-
- /* theory timing */
-
- object Theory_Timing {
- def unapply(props: Properties.T): Option[(String, isabelle.Timing)] =
- props match {
- case Markup.Theory_Timing(args) =>
- (args, args) match {
- case (Markup.Name(name), Markup.Timing_Properties(timing)) => Some((name, timing))
- case _ => None
- }
+ case Markup.Command_Timing(args@Position.Id(id)) => Some((id, args))
case _ => None
}
}
--- a/src/Pure/PIDE/prover.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/prover.scala Wed Sep 24 23:06:22 2025 +0200
@@ -63,7 +63,7 @@
Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
class Protocol_Output(props: Properties.T, val chunks: List[Bytes])
- extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil)) {
+ extends Output(XML.elem(Markup(Markup.PROTOCOL, props))) {
def chunk: Bytes = the_chunk(chunks, toString)
lazy val text: String = chunk.text
}
--- a/src/Pure/PIDE/rendering.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/rendering.scala Wed Sep 24 23:06:22 2025 +0200
@@ -661,15 +661,16 @@
for ((i, msg) <- Command.State.get_result_proper(command_states, props))
yield info.add_message(r0, i, msg)
- case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
+ case (info, Text.Info(r0, XML.Elem(markup@Markup.Entity(kind, name), _)))
if kind != "" && kind != Markup.ML_DEF =>
val txt = Rendering.gui_name(name, kind = kind)
val info1 = info.add_info_text(r0, txt, ord = 2)
val info2 =
if (kind == Markup.COMMAND) {
- val timing = Timing.merge(command_states.iterator.map(_.timing))
- if (timing.is_notable(timing_threshold)) {
- info1.add_info(r0, Pretty.string(timing.message))
+ val timings = Document_Status.Command_Timings.merge(command_states.map(_.timings))
+ val t = timings(Markup.Command_Offset.get(markup.properties))
+ if (t.is_notable(timing_threshold)) {
+ info1.add_info(r0, Pretty.string(t.message))
}
else info1
}
--- a/src/Pure/PIDE/session.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/session.scala Wed Sep 24 23:06:22 2025 +0200
@@ -63,8 +63,7 @@
/* events */
//{{{
- case class Command_Timing(props: Properties.T)
- case class Theory_Timing(props: Properties.T)
+ case class Command_Timing(state_id: Document_ID.Generic, props: Properties.T)
case class Runtime_Statistics(props: Properties.T)
case class Task_Statistics(props: Properties.T)
case class Global_Options(options: Options)
@@ -239,7 +238,6 @@
val finished_theories = new Session.Outlet[Document.Snapshot](dispatcher)
val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher)
- val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher)
val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher)
val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher)
val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
@@ -535,13 +533,10 @@
val handled = protocol_handlers.invoke(msg)
if (!handled) {
msg.properties match {
- case Protocol.Command_Timing(props, state_id, timing) if prover.defined =>
- command_timings.post(Session.Command_Timing(props))
- val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
+ case Protocol.Command_Timing(state_id, props) if prover.defined =>
+ val message = XML.elem(Markup(Markup.TIMING, props))
change_command(_.accumulate(state_id, cache.elem(message), cache))
-
- case Markup.Theory_Timing(props) =>
- theory_timings.post(Session.Theory_Timing(props))
+ command_timings.post(Session.Command_Timing(state_id, props))
case Markup.Task_Statistics(props) =>
task_statistics.post(Session.Task_Statistics(props))
@@ -552,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/PIDE/xml.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/PIDE/xml.scala Wed Sep 24 23:06:22 2025 +0200
@@ -71,7 +71,7 @@
def elem(markup: Markup): XML.Elem = XML.Elem(markup, Nil)
def elem(name: String, body: Body): XML.Elem = XML.Elem(Markup(name, Nil), body)
- def elem(name: String): XML.Elem = XML.Elem(Markup(name, Nil), Nil)
+ def elem(name: String): XML.Elem = XML.elem(name, Nil)
val no_text: Text = Text("")
val newline: Text = Text("\n")
@@ -356,8 +356,7 @@
val tree: T[XML.Tree] = (t => List(t))
- val properties: T[Properties.T] =
- (props => List(XML.Elem(Markup(":", props), Nil)))
+ val properties: T[Properties.T] = (props => List(XML.elem(Markup(":", props))))
val string: T[String] = XML.string
--- a/src/Pure/System/progress.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/System/progress.scala Wed Sep 24 23:06:22 2025 +0200
@@ -36,15 +36,40 @@
sealed case class Theory(
theory: String,
session: String = "",
- percentage: Option[Int] = None
+ percentage: Option[Int] = None,
+ total_time: Time = Time.zero
) extends Output {
def message: Message =
- Message(Kind.writeln, print_session + print_theory + print_percentage, verbose = true)
+ Message(Kind.writeln, print_session + print_theory + print_percentage + print_total_time,
+ verbose = true)
def print_session: String = if_proper(session, session + ": ")
def print_theory: String = "theory " + theory
def print_percentage: String =
percentage match { case None => "" case Some(p) => " " + p + "%" }
+ def print_total_time: String =
+ if (total_time.is_relevant) " (" + total_time.message + " elapsed time)" else ""
+ }
+
+ sealed case class Nodes_Status(
+ domain: List[Document.Node.Name],
+ document_status: Document_Status.Nodes_Status,
+ session: String = "",
+ old: Option[Document_Status.Nodes_Status] = None
+ ) {
+ def message: Message =
+ Message(Kind.writeln, cat_lines(domain.map(name => theory(name).message.text)),
+ verbose = true)
+
+ def apply(name: Document.Node.Name): Document_Status.Node_Status =
+ document_status(name)
+
+ def theory(name: Document.Node.Name): Theory = {
+ val node_status = apply(name)
+ Theory(theory = name.theory, session = session,
+ percentage = Some(node_status.percentage),
+ total_time = node_status.total_timing.elapsed)
+ }
}
}
@@ -67,7 +92,7 @@
final def echo_if(cond: Boolean, msg: String): Unit = if (cond) echo(msg)
def theory(theory: Progress.Theory): Unit = output(theory.message)
- def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {}
+ def nodes_status(nodes_status: Progress.Nodes_Status): Unit = {}
final def capture[A](e: => A, msg: String, err: Throwable => String): Exn.Result[A] = {
echo(msg)
--- a/src/Pure/System/web_app.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/System/web_app.scala Wed Sep 24 23:06:22 2025 +0200
@@ -35,9 +35,9 @@
val td = new Operator("td")
def icon(href: String): XML.Elem =
- XML.Elem(Markup("link", List("rel" -> "icon", "type" -> "image/x-icon", "href" -> href)), Nil)
+ XML.elem(Markup("link", List("rel" -> "icon", "type" -> "image/x-icon", "href" -> href)))
- def legend(txt: String): XML.Elem = XML.Elem(Markup("legend", Nil), text(txt))
+ def legend(txt: String): XML.Elem = XML.elem("legend", text(txt))
def input(typ: String): XML.Elem = XML.Elem(Markup("input", List("type" -> typ)), Nil)
def hidden(k: Params.Key, v: String): XML.Elem =
id(k.print)(name(k.print)(value(v)(input("hidden"))))
--- a/src/Pure/Thy/thy_info.ML Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/Thy/thy_info.ML Wed Sep 24 23:06:22 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,24 +367,20 @@
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 () =>
(parents, map #2 imports) |> ListPair.app (fn (thy, pos) =>
Context_Position.reports_global thy [(put_id pos, Theory.get_markup thy)])) ();
- val timing_start = Timing.start ();
-
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);
- val timing_result = Timing.result timing_start;
- val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
- val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []
-
fun commit segments =
update_thy deps (theory,
if Options.bool options \<^system_option>\<open>record_theories\<close> then segments else []);
--- a/src/Pure/Thy/thy_syntax.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Sep 24 23:06:22 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)))
}
--- a/src/Pure/Tools/server.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Pure/Tools/server.scala Wed Sep 24 23:06:22 2025 +0200
@@ -274,10 +274,12 @@
context.writeln(theory.message.text, entries ::: more.toList:_*)
}
- override def nodes_status(nodes_status: Document_Status.Nodes_Status): Unit = {
+ override def nodes_status(nodes_status: Progress.Nodes_Status): Unit = {
val json =
- for ((name, node_status) <- nodes_status.present() if !node_status.is_empty)
- yield name.json + ("status" -> node_status.json)
+ List.from(for {
+ name <- nodes_status.domain.iterator
+ node_status = nodes_status(name) if !node_status.is_empty
+ } yield name.json + ("status" -> node_status.json))
context.notify(JSON.Object(Markup.KIND -> Markup.NODES_STATUS, Markup.NODES_STATUS -> json))
}
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala Wed Sep 24 23:06:22 2025 +0200
@@ -61,12 +61,10 @@
children.values.toList.collect {
case Left(data) => Some(format_hint(data))
case Right(tree) if tree.interesting => tree.format
- }.flatten.map(item =>
- XML.Elem(Markup(Markup.ITEM, Nil), List(item))
- )
+ }.flatten.map(item => XML.elem(Markup.ITEM, List(item)))
val all = XML.Text(data.text) :: data.content ::: bodies
- val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
+ val res = XML.elem(Markup.TEXT_FOLD, List(Pretty.block(Pretty.separate(all))))
if (bodies != Nil)
Some(res)
--- a/src/Tools/jEdit/src/theories_status.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Tools/jEdit/src/theories_status.scala Wed Sep 24 23:06:22 2025 +0200
@@ -235,23 +235,23 @@
val snapshot = PIDE.session.snapshot()
- val (nodes_status_changed, nodes_status1) =
- nodes_status.update(
+ val nodes_status1 =
+ nodes_status.update_nodes(
PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
- nodes_status = nodes_status1
- if (nodes_status_changed || force) {
+ if (force || nodes_status1 != nodes_status) {
gui.listData =
- if (document) {
- nodes_status1.present(domain = Some(PIDE.editor.document_theories())).map(_._1)
- }
+ if (document) PIDE.editor.document_theories()
else {
(for {
- (name, node_status) <- nodes_status1.present().iterator
+ name <- snapshot.version.nodes.topological_order.iterator
+ node_status = nodes_status1(name)
if !node_status.is_empty && !node_status.suppressed && node_status.total > 0
} yield name).toList
}
}
+
+ nodes_status = nodes_status1
}
--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Sep 24 17:50:30 2025 +0200
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Sep 24 23:06:22 2025 +0200
@@ -145,10 +145,10 @@
val theories =
List.from(
for ((a, st) <- nodes_status.iterator if st.command_timings.nonEmpty)
- yield Theory_Entry(a, st.total_time.seconds)).sorted(Entry.Ordering)
+ yield Theory_Entry(a, st.total_timing.elapsed.seconds)).sorted(Entry.Ordering)
val commands =
- (for ((command, command_timing) <- nodes_status(name).command_timings.toList)
- yield Command_Entry(command, command_timing.seconds)).sorted(Entry.Ordering)
+ (for ((command, timings) <- nodes_status(name).command_timings.toList)
+ yield Command_Entry(command, timings.sum.elapsed.seconds)).sorted(Entry.Ordering)
theories.flatMap(entry =>
if (entry.name == name) entry.make_current :: commands
@@ -166,9 +166,9 @@
.filterNot(PIDE.resources.loaded_theory).toSet)
nodes_status =
- nodes_status.update(PIDE.resources, snapshot.state, snapshot.version,
+ nodes_status.update_nodes(PIDE.resources, snapshot.state, snapshot.version,
threshold = Time.seconds(timing_threshold),
- domain = Some(domain))._2
+ domain = Some(domain))
val entries = make_entries()
if (timing_view.listData.toList != entries) timing_view.listData = entries