--- a/NEWS Wed Sep 17 12:19:12 2025 +0100
+++ b/NEWS Wed Sep 17 20:57:11 2025 +0200
@@ -408,6 +408,11 @@
information later on, using Thy_Info.get_theory_segments or
Thy_Info.get_theory_elements in Isabelle/ML.
+* System option "command_timing_threshold" has been renamed to
+"build_timing_threshold": it refers to batch-builds. Likewise,
+"jedit_timing_threshold" and "vscode_timing_threshold" have been unified
+as "editor_timing_threshold": it refers to PIDE editor interaction.
+
* The Z Garbage Collector (ZGC) of Java 21 is now used by default (see
also https://wiki.openjdk.org/display/zgc). This should work uniformly
on all platforms, but requires a reasonably new version of Windows
--- a/etc/options Wed Sep 17 12:19:12 2025 +0100
+++ b/etc/options Wed Sep 17 20:57:11 2025 +0200
@@ -107,8 +107,8 @@
option parallel_subproofs_threshold : real = 0.01 for build
-- "lower bound of timing estimate for forked nested proofs (seconds)"
-option command_timing_threshold : real = 0.1 for build
- -- "default threshold for persistent command timing (seconds)"
+option build_timing_threshold : real = 0.1 for build
+ -- "threshold for persistent storage of command timings (seconds)"
public option timeout_scale : real = 1.0 for build
-- "scale factor for timeout in Isabelle/ML and session build"
@@ -344,6 +344,9 @@
option editor_syslog_limit : int = 100
-- "maximum amount of buffered syslog messages"
+public option editor_timing_threshold : real = 0.1
+ -- "threshold for interactive display of command timings (seconds)"
+
section "Headless Session"
--- a/src/Pure/Build/build_job.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Pure/Build/build_job.scala Wed Sep 17 20:57:11 2025 +0200
@@ -280,8 +280,7 @@
for {
elapsed <- Markup.Elapsed.unapply(props)
elapsed_time = Time.seconds(elapsed)
- if elapsed_time.is_relevant &&
- elapsed_time >= options.seconds("command_timing_threshold")
+ if elapsed_time.is_notable(options.seconds("build_timing_threshold"))
} command_timings += props.filter(Markup.command_timing_property)
}
--- a/src/Pure/General/time.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Pure/General/time.scala Wed Sep 17 20:57:11 2025 +0200
@@ -61,6 +61,7 @@
def is_zero: Boolean = ms == 0
def is_relevant: Boolean = ms >= 1
+ def is_notable(threshold: Time): Boolean = is_relevant && this >= threshold
override def toString: String = Time.print_seconds(seconds)
--- a/src/Pure/General/timing.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Pure/General/timing.scala Wed Sep 17 20:57:11 2025 +0200
@@ -36,11 +36,15 @@
def factor_format(f: Double): String =
String.format(Locale.ROOT, ", factor %.2f", java.lang.Double.valueOf(f))
+
+ def merge(args: IterableOnce[Timing]): Timing =
+ args.iterator.foldLeft(zero)(_ + _)
}
sealed case class Timing(elapsed: Time, cpu: Time, gc: Time) {
def is_zero: Boolean = elapsed.is_zero && cpu.is_zero && gc.is_zero
def is_relevant: Boolean = elapsed.is_relevant || cpu.is_relevant || gc.is_relevant
+ def is_notable(threshold: Time): Boolean = is_relevant && elapsed.is_notable(threshold)
def resources: Time = cpu + gc
--- a/src/Pure/PIDE/command.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Pure/PIDE/command.scala Wed Sep 17 20:57:11 2025 +0200
@@ -49,6 +49,9 @@
args.iterator.foldLeft(empty)(_ + _)
def merge(args: IterableOnce[Results]): Results =
args.iterator.foldLeft(empty)(_ ++ _)
+
+ def warned(entry: Entry): Boolean = Protocol.is_warning_or_legacy(entry._2)
+ def failed(entry: Entry): Boolean = Protocol.is_error(entry._2)
}
final class Results private(private val rep: SortedMap[Long, XML.Elem]) {
@@ -57,8 +60,8 @@
def get(serial: Long): Option[XML.Elem] = rep.get(serial)
def iterator: Iterator[Results.Entry] = rep.iterator
- lazy val warned: Boolean = rep.exists(p => Protocol.is_warning(p._2) || Protocol.is_legacy(p._2))
- lazy val failed: Boolean = rep.exists(p => Protocol.is_error(p._2))
+ def warned: Boolean = rep.exists(Results.warned)
+ def failed: Boolean = rep.exists(Results.failed)
def + (entry: Results.Entry): Results =
if (defined(entry._1)) this
@@ -202,42 +205,71 @@
Markup_Tree.merge(states.map(_.markup(index)), range, elements)
def merge(command: Command, states: List[State]): State =
- State(command, states.flatMap(_.status), merge_results(states),
- merge_exports(states), merge_markups(states))
+ 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
+ ): 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)
+ }
}
- sealed case class State(
- command: Command,
- status: List[Markup] = Nil,
- results: Results = Results.empty,
- exports: Exports = Exports.empty,
- markups: Markups = Markups.empty
+ final class State private(
+ val command: Command,
+ val status: List[Markup],
+ val results: Results,
+ val exports: Exports,
+ val markups: Markups,
+ val document_status: Document_Status.Command_Status
) {
- lazy val document_status: Document_Status.Command_Status =
- Document_Status.Command_Status.make(
- status, warned = results.warned, failed = results.failed)
+ override def toString: String = "Command.State(" + command + ")"
+ override def hashCode(): Int = ???
+ override def equals(obj: Any): Boolean = ???
def initialized: Boolean = document_status.initialized
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 markup(index: Markup_Index): Markup_Tree = markups(index)
def redirect(other_command: Command): Option[State] = {
val markups1 = markups.redirect(other_command.id)
if (markups1.is_empty) None
- else Some(new State(other_command, markups = markups1))
+ else Some(State(other_command, markups = markups1))
+ }
+
+ 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)
}
- private def add_status(st: Markup): State =
- copy(status = st :: status)
-
- private def add_result(entry: Results.Entry): State =
- copy(results = results + entry)
+ private def add_result(entry: Results.Entry): State = {
+ val document_status1 =
+ document_status.update(
+ warned = Results.warned(entry),
+ failed = Results.failed(entry))
+ new State(command, status, results + entry, exports, markups, document_status1)
+ }
def add_export(entry: Exports.Entry): Option[State] =
- if (command.node_name.theory == entry._2.theory_name) Some(copy(exports = exports + entry))
+ if (command.node_name.theory == entry._2.theory_name) {
+ Some(new State(command, status, results, exports + entry, markups, document_status))
+ }
else None
private def add_markup(
@@ -249,7 +281,8 @@
if (status || Document_Status.Command_Status.liberal_elements(m.info.name))
markups.add(Markup_Index(true, chunk_name), m)
else markups
- copy(markups = markups1.add(Markup_Index(false, chunk_name), m))
+ val markups2 = markups1.add(Markup_Index(false, chunk_name), m)
+ new State(command, this.status, results, exports, markups2, document_status)
}
def accumulate(
@@ -464,8 +497,6 @@
lazy val is_unparsed: Boolean = span.content.exists(_.is_unparsed)
lazy val is_unfinished: Boolean = span.content.exists(_.is_unfinished)
- def potentially_initialized: Boolean = span.name == Thy_Header.THEORY
-
/* blobs */
--- a/src/Pure/PIDE/document.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Pure/PIDE/document.scala Wed Sep 17 20:57:11 2025 +0200
@@ -385,13 +385,13 @@
final class Nodes private(graph: Graph[Node.Name, Node]) {
def apply(name: Node.Name): Node = Nodes.init(graph, name).get_node(name)
- def is_suppressed(name: Node.Name): Boolean = {
+ def suppressed(name: Node.Name): Boolean = {
val graph1 = Nodes.init(graph, name)
graph1.is_maximal(name) && graph1.get_node(name).is_empty
}
def purge_suppressed: Option[Nodes] =
- graph.keys_iterator.filter(is_suppressed).toList match {
+ names_iterator.filter(suppressed).toList match {
case Nil => None
case del => Some(new Nodes(del.foldLeft(graph)(_.del_node(_))))
}
@@ -411,8 +411,10 @@
def iterator: Iterator[(Node.Name, Node)] =
graph.iterator.map({ case (name, (node, _)) => (name, node) })
+ def names_iterator: Iterator[Node.Name] = graph.keys_iterator
+
def theory_name(theory: String): Option[Node.Name] =
- graph.keys_iterator.find(name => name.theory == theory)
+ names_iterator.find(name => name.theory == theory)
def commands_loading(file_name: Node.Name): List[Command] =
(for {
@@ -598,12 +600,9 @@
for ((i, name) <- (0, node_name) :: node.load_commands.flatMap(_.blobs_files))
yield (i, File.symbolic_path(name.path))
- def node_consolidated(name: Node.Name): Boolean =
- state.node_consolidated(version, name)
-
def theory_consolidated(theory: String): Boolean =
version.nodes.theory_name(theory) match {
- case Some(name) => node_consolidated(name)
+ case Some(name) => state.node_consolidated(version, name)
case None => false
}
@@ -1267,6 +1266,13 @@
self.map(_._2) ::: others.flatMap(_.redirect(command))
}
+ def command_status(version: Version, command: Command): Document_Status.Command_Status =
+ 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))
@@ -1308,13 +1314,6 @@
else Nil
}
- def node_initialized(version: Version, name: Node.Name): Boolean =
- name.is_theory &&
- (version.nodes(name).commands.iterator.find(_.potentially_initialized) match {
- case None => false
- case Some(command) => command_states(version, command).headOption.exists(_.initialized)
- })
-
def node_maybe_consolidated(version: Version, name: Node.Name): Boolean =
name.is_theory &&
version.nodes(name).commands.reverse.iterator.forall(command_maybe_consolidated(version, _))
--- a/src/Pure/PIDE/document_status.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Pure/PIDE/document_status.scala Wed Sep 17 20:57:11 2025 +0200
@@ -21,6 +21,14 @@
def merge(t1: Value, t2: Value): Value = if (t1 >= t2) t1 else t2
}
+ trait Theory_Status {
+ def theory_status: Theory_Status.Value
+ def initialized: Boolean = Theory_Status.initialized(theory_status)
+ def finalized: Boolean = Theory_Status.finalized(theory_status)
+ def consolidating: Boolean = Theory_Status.consolidating(theory_status)
+ def consolidated: Boolean = Theory_Status.consolidated(theory_status)
+ }
+
/* command status */
@@ -33,7 +41,7 @@
proper_elements + Markup.WARNING + Markup.LEGACY + Markup.ERROR
def make(
- markups: Iterable[Markup],
+ markups: List[Markup] = Nil,
warned: Boolean = false,
failed: Boolean = false
): Command_Status = {
@@ -45,6 +53,7 @@
var canceled = false
var forks = 0
var runs = 0
+ var timing = Timing.zero
for (markup <- markups) {
markup.name match {
case Markup.INITIALIZED =>
@@ -65,6 +74,10 @@
case Markup.CANCELED => canceled = true
case _ =>
}
+ markup match {
+ case Markup.Timing(t) => timing += t
+ case _ =>
+ }
}
new Command_Status(
theory_status = theory_status,
@@ -74,25 +87,27 @@
failed = failed1,
canceled = canceled,
forks = forks,
- runs = runs)
+ runs = runs,
+ timing = timing)
}
- val empty: Command_Status = make(Nil)
+ val empty: Command_Status = make()
def merge(args: IterableOnce[Command_Status]): Command_Status =
args.iterator.foldLeft(empty)(_ + _)
}
final class Command_Status private(
- private val theory_status: Theory_Status.Value,
+ val theory_status: Theory_Status.Value,
private val touched: Boolean,
private val accepted: Boolean,
private val warned: Boolean,
private val failed: Boolean,
private val canceled: Boolean,
val forks: Int,
- val runs: Int
- ) {
+ val runs: Int,
+ val timing: Timing
+ ) extends Theory_Status {
override def toString: String =
if (is_empty) "Command_Status.empty"
else if (failed) "Command_Status(failed)"
@@ -102,7 +117,7 @@
def is_empty: Boolean =
!Theory_Status.initialized(theory_status) &&
!touched && !accepted && !warned && !failed && !canceled &&
- forks == 0 && runs == 0
+ forks == 0 && runs == 0 && timing.is_zero
def + (that: Command_Status): Command_Status =
if (is_empty) that
@@ -116,13 +131,35 @@
failed = failed || that.failed,
canceled = canceled || that.canceled,
forks = forks + that.forks,
- runs = runs + that.runs)
+ runs = runs + that.runs,
+ timing = timing + that.timing)
}
- def initialized: Boolean = Theory_Status.initialized(theory_status)
- def finalized: Boolean = Theory_Status.finalized(theory_status)
- def consolidating: Boolean = Theory_Status.consolidating(theory_status)
- def consolidated: Boolean = Theory_Status.consolidated(theory_status)
+ def update(
+ markups: List[Markup] = Nil,
+ warned: Boolean = false,
+ failed: Boolean = false
+ ): Command_Status = {
+ if (markups.isEmpty) {
+ val warned1 = this.warned || warned
+ val failed1 = this.failed || failed
+ if (this.warned == warned1 && this.failed == failed1) this
+ else {
+ new Command_Status(
+ theory_status = theory_status,
+ touched = touched,
+ accepted = accepted,
+ warned = warned1,
+ failed = failed1,
+ canceled = canceled,
+ forks = forks,
+ runs = runs,
+ timing = timing)
+ }
+ }
+ else this + Command_Status.make(markups = markups, warned = warned, failed = failed)
+ }
+
def maybe_consolidated: Boolean = touched && forks == 0 && runs == 0
def is_unprocessed: Boolean = accepted && !failed && (!touched || (forks != 0 && runs == 0))
@@ -138,27 +175,14 @@
/* node status */
object Node_Status {
- val empty: Node_Status =
- Node_Status(
- is_suppressed = false,
- unprocessed = 0,
- running = 0,
- warned = 0,
- failed = 0,
- finished = 0,
- canceled = false,
- terminated = false,
- initialized = false,
- finalized = false,
- consolidated = false)
+ val empty: Node_Status = Node_Status()
def make(
state: Document.State,
version: Document.Version,
- name: Document.Node.Name
+ name: Document.Node.Name,
+ threshold: Time = Time.max
): Node_Status = {
- val node = version.nodes(name)
-
var unprocessed = 0
var running = 0
var warned = 0
@@ -166,10 +190,13 @@
var finished = 0
var canceled = false
var terminated = true
- var finalized = false
- for (command <- node.commands.iterator) {
- val states = state.command_states(version, command)
- val status = Command_Status.merge(states.iterator.map(_.document_status))
+ var total_time = Time.zero
+ var max_time = Time.zero
+ var command_timings = Map.empty[Command, Time]
+ var theory_status = Document_Status.Theory_Status.NONE
+
+ for (command <- version.nodes(name).commands.iterator) {
+ val status = state.command_status(version, command)
if (status.is_running) running += 1
else if (status.is_failed) failed += 1
@@ -179,13 +206,17 @@
if (status.is_canceled) canceled = true
if (!status.is_terminated) terminated = false
- if (status.finalized) finalized = true
+
+ val t = state.command_timing(version, command).elapsed
+ total_time += t
+ if (t > max_time) max_time = t
+ if (t.is_notable(threshold)) command_timings += (command -> t)
+
+ theory_status = Theory_Status.merge(theory_status, status.theory_status)
}
- val initialized = state.node_initialized(version, name)
- val consolidated = state.node_consolidated(version, name)
Node_Status(
- is_suppressed = version.nodes.is_suppressed(name),
+ suppressed = version.nodes.suppressed(name),
unprocessed = unprocessed,
running = running,
warned = warned,
@@ -193,31 +224,35 @@
finished = finished,
canceled = canceled,
terminated = terminated,
- initialized = initialized,
- finalized = finalized,
- consolidated = consolidated)
+ total_time = total_time,
+ max_time = max_time,
+ threshold = threshold,
+ command_timings = command_timings,
+ theory_status = theory_status)
}
}
sealed case class Node_Status(
- is_suppressed: Boolean,
- unprocessed: Int,
- running: Int,
- warned: Int,
- failed: Int,
- finished: Int,
- canceled: Boolean,
- terminated: Boolean,
- initialized: Boolean,
- finalized: Boolean,
- consolidated: Boolean
- ) {
+ suppressed: Boolean = false,
+ unprocessed: Int = 0,
+ running: Int = 0,
+ warned: Int = 0,
+ failed: Int = 0,
+ finished: Int = 0,
+ canceled: Boolean = false,
+ terminated: Boolean = false,
+ total_time: Time = Time.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,
+ ) extends Theory_Status {
def is_empty: Boolean = this == Node_Status.empty
def ok: Boolean = failed == 0
def total: Int = unprocessed + running + warned + failed + finished
- def quasi_consolidated: Boolean = !is_suppressed && !finalized && terminated
+ def quasi_consolidated: Boolean = !suppressed && !finalized && terminated
def percentage: Int =
if (consolidated) 100
@@ -232,49 +267,9 @@
}
- /* overall timing */
-
- object Overall_Timing {
- val empty: Overall_Timing = Overall_Timing()
-
- def make(
- state: Document.State,
- version: Document.Version,
- commands: Iterable[Command],
- threshold: Double = 0.0
- ): Overall_Timing = {
- var total = 0.0
- var command_timings = Map.empty[Command, Double]
- for {
- command <- commands.iterator
- st <- state.command_states(version, command)
- } {
- val command_timing =
- st.status.foldLeft(0.0) {
- case (timing, Markup.Timing(t)) => timing + t.elapsed.seconds
- case (timing, _) => timing
- }
- total += command_timing
- if (command_timing > 0.0 && command_timing >= threshold) {
- command_timings += (command -> command_timing)
- }
- }
- Overall_Timing(total = total, command_timings = command_timings)
- }
- }
-
- sealed case class Overall_Timing(
- total: Double = 0.0,
- command_timings: Map[Command, Double] = Map.empty
- ) {
- def command_timing(command: Command): Double =
- command_timings.getOrElse(command, 0.0)
- }
-
-
/* nodes status */
- enum Overall_Node_Status { case ok, failed, pending }
+ enum Overall_Status { case ok, failed, pending }
object Nodes_Status {
val empty: Nodes_Status = new Nodes_Status(Map.empty, Document.Nodes.empty)
@@ -285,33 +280,36 @@
nodes: Document.Nodes
) {
def is_empty: Boolean = rep.isEmpty
- def apply(name: Document.Node.Name): Node_Status = rep(name)
+ 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 -> get(name).getOrElse(Node_Status.empty)
+ yield name -> apply(name)
}
def quasi_consolidated(name: Document.Node.Name): Boolean =
- rep.get(name) match {
+ get(name) match {
case Some(st) => st.quasi_consolidated
case None => false
}
- def overall_node_status(name: Document.Node.Name): Overall_Node_Status =
- rep.get(name) match {
+ def overall_status(name: Document.Node.Name): Overall_Status =
+ get(name) match {
case Some(st) if st.consolidated =>
- if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
- case _ => Overall_Node_Status.pending
+ if (st.ok) Overall_Status.ok else Overall_Status.failed
+ case _ => Overall_Status.pending
}
def update(
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) = {
@@ -320,8 +318,8 @@
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)
- if !rep.isDefinedAt(name) || rep(name) != st
+ 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
@@ -342,10 +340,10 @@
var pending = 0
var canceled = 0
for (name <- rep.keysIterator) {
- overall_node_status(name) match {
- case Overall_Node_Status.ok => ok += 1
- case Overall_Node_Status.failed => failed += 1
- case Overall_Node_Status.pending => pending += 1
+ overall_status(name) match {
+ case Overall_Status.ok => ok += 1
+ case Overall_Status.failed => failed += 1
+ case Overall_Status.pending => pending += 1
}
if (apply(name).canceled) canceled += 1
}
--- a/src/Pure/PIDE/protocol.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Pure/PIDE/protocol.scala Wed Sep 17 20:57:11 2025 +0200
@@ -168,6 +168,9 @@
case _ => false
}
+ def is_warning_or_legacy(msg: XML.Tree): Boolean =
+ is_warning(msg) || is_legacy(msg)
+
def is_inlined(msg: XML.Tree): Boolean =
!(is_result(msg) || is_tracing(msg))
@@ -176,7 +179,7 @@
def message_heading(elem: XML.Elem, pos: Position.T): String = {
val h =
- if (is_warning(elem) || is_legacy(elem)) "Warning"
+ if (is_warning_or_legacy(elem)) "Warning"
else if (is_error(elem)) "Error"
else if (is_information(elem)) "Information"
else if (is_tracing(elem)) "Tracing"
@@ -200,7 +203,7 @@
metric = metric, pure = true)
val text2 =
- if (is_warning(elem) || is_legacy(elem)) Output.warning_prefix(body)
+ if (is_warning_or_legacy(elem)) Output.warning_prefix(body)
else if (is_error(elem)) Output.error_message_prefix(body)
else body
--- a/src/Pure/PIDE/rendering.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Pure/PIDE/rendering.scala Wed Sep 17 20:57:11 2025 +0200
@@ -268,7 +268,7 @@
Markup.COMMAND_SPAN)
val tooltip_elements: Markup.Elements =
- Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION, Markup.TIMING,
+ Markup.Elements(Markup.LANGUAGE, Markup.NOTATION, Markup.EXPRESSION,
Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.CLASS_PARAMETER, Markup.ML_TYPING,
Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC, Markup.URL, Markup.COMMAND_SPAN,
Markup.MARKDOWN_PARAGRAPH, Markup.MARKDOWN_ITEM, Markup.Markdown_List.name) ++
@@ -510,7 +510,7 @@
color <-
result match {
case (markups, opt_color) if markups.nonEmpty =>
- val status = Document_Status.Command_Status.make(markups)
+ val status = Document_Status.Command_Status.make(markups = markups)
if (status.is_unprocessed) Some(Rendering.Color.unprocessed1)
else if (status.is_running) Some(Rendering.Color.running1)
else if (status.is_canceled) Some(Rendering.Color.canceled)
@@ -617,15 +617,13 @@
/* tooltips */
- def timing_threshold: Double = 0.0
+ def timing_threshold: Time = options.seconds("editor_timing_threshold")
private sealed case class Tooltip_Info(
range: Text.Range,
- timing: Timing = Timing.zero,
messages: List[(Long, XML.Elem)] = Nil,
rev_infos: List[(Boolean, Int, XML.Elem)] = Nil
) {
- def add_timing(t: Timing): Tooltip_Info = copy(timing = timing + t)
def add_message(r0: Text.Range, serial: Long, msg: XML.Elem): Tooltip_Info = {
val r = snapshot.convert(r0)
if (range == r) copy(messages = (serial -> msg) :: messages)
@@ -643,19 +641,8 @@
def add_info_text(r0: Text.Range, text: String, ord: Int = 0): Tooltip_Info =
add_info(r0, Pretty.string(text), ord = ord)
- def timing_info(elem: XML.Elem): Option[XML.Elem] =
- if (elem.markup.name == Markup.TIMING) {
- if (timing.elapsed.seconds >= timing_threshold) {
- Some(Pretty.string(timing.message))
- }
- else None
- }
- else Some(elem)
def infos(important: Boolean = true): List[XML.Elem] =
- for {
- (is_important, _, elem) <- rev_infos.reverse.sortBy(_._2) if is_important == important
- elem1 <- timing_info(elem)
- } yield elem1
+ for ((imp, _, elem) <- rev_infos.reverse.sortBy(_._2) if imp == important) yield elem
}
def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
@@ -666,8 +653,6 @@
val results =
snapshot.cumulate[Tooltip_Info](range, Tooltip_Info(range), elements, command_states =>
{
- case (info, Text.Info(_, XML.Elem(Markup.Timing(t), _))) => Some(info.add_timing(t))
-
case (info, Text.Info(r0, msg @ XML.Elem(Markup.Bad(i), body)))
if body.nonEmpty => Some(info.add_message(r0, i, msg))
@@ -680,7 +665,16 @@
if kind != "" && kind != Markup.ML_DEF =>
val txt = Rendering.gui_name(name, kind = kind)
val info1 = info.add_info_text(r0, txt, ord = 2)
- Some(if (kind == Markup.COMMAND) info1.add_info(r0, XML.elem(Markup.TIMING)) else info1)
+ 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))
+ }
+ else info1
+ }
+ else info1
+ Some(info2)
case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
val file = perhaps_append_file(snapshot.node_name, name)
@@ -778,7 +772,7 @@
}, status = true)
if (results.isEmpty) None
else {
- val status = Document_Status.Command_Status.make(results.flatMap(_.info))
+ val status = Document_Status.Command_Status.make(markups = results.flatMap(_.info))
if (status.is_running) Some(Rendering.Color.running)
else if (status.is_failed) Some(Rendering.Color.error)
--- a/src/Tools/VSCode/etc/options Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Tools/VSCode/etc/options Wed Sep 17 20:57:11 2025 +0200
@@ -15,9 +15,6 @@
option vscode_message_margin : int = 80 for vscode
-- "margin for pretty-printing of diagnostic messages"
-option vscode_timing_threshold : real = 0.1 for vscode
- -- "default threshold for timing display (seconds)"
-
option vscode_pide_extensions : bool = false for vscode
-- "use PIDE extensions for Language Server Protocol"
--- a/src/Tools/VSCode/src/vscode_rendering.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala Wed Sep 17 20:57:11 2025 +0200
@@ -251,11 +251,6 @@
}
- /* tooltips */
-
- override def timing_threshold: Double = options.real("vscode_timing_threshold")
-
-
/* hyperlinks */
def hyperlink_source_file(
--- a/src/Tools/jEdit/etc/options Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Tools/jEdit/etc/options Wed Sep 17 20:57:11 2025 +0200
@@ -33,9 +33,6 @@
public option jedit_symbols_search_limit : int = 50
-- "maximum number of symbols in search result"
-public option jedit_timing_threshold : real = 0.1
- -- "default threshold for timing display (seconds)"
-
public option jedit_text_overview : bool = true
-- "paint text overview column"
--- a/src/Tools/jEdit/src/jedit_rendering.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala Wed Sep 17 20:57:11 2025 +0200
@@ -310,7 +310,6 @@
/* tooltips */
def tooltip_margin: Int = options.int("jedit_tooltip_margin")
- override def timing_threshold: Double = options.real("jedit_timing_threshold")
def tooltip(range: Text.Range, control: Boolean): Option[Text.Info[List[XML.Elem]]] =
tooltips(if (control) Rendering.tooltip_elements else Rendering.tooltip_message_elements,
--- a/src/Tools/jEdit/src/theories_status.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala Wed Sep 17 20:57:11 2025 +0200
@@ -28,10 +28,9 @@
private def is_loaded_theory(name: Document.Node.Name): Boolean =
PIDE.resources.loaded_theory(name)
- private def overall_node_status(name: Document.Node.Name): Document_Status.Overall_Node_Status = {
- if (is_loaded_theory(name)) Document_Status.Overall_Node_Status.ok
- else nodes_status.overall_node_status(name)
- }
+ private def overall_status(name: Document.Node.Name): Document_Status.Overall_Status =
+ if (is_loaded_theory(name)) Document_Status.Overall_Status.ok
+ else nodes_status.overall_status(name)
private def init_state(): Unit = GUI_Thread.require {
if (document) {
@@ -128,16 +127,16 @@
}
def label_border(name: Document.Node.Name): Unit = {
- val st = overall_node_status(name)
+ val st = overall_status(name)
val color =
st match {
- case Document_Status.Overall_Node_Status.ok =>
+ case Document_Status.Overall_Status.ok =>
PIDE.options.color_value("ok_color")
- case Document_Status.Overall_Node_Status.failed =>
+ case Document_Status.Overall_Status.failed =>
PIDE.options.color_value("failed_color")
case _ => label.foreground
}
- val thickness1 = if (st == Document_Status.Overall_Node_Status.pending) 1 else 3
+ val thickness1 = if (st == Document_Status.Overall_Status.pending) 1 else 3
val thickness2 = 4 - thickness1
label.border =
@@ -211,10 +210,10 @@
}
else if (index >= 0 && node_renderer.in_label(index_location, point)) {
val name = listData(index)
- val st = overall_node_status(name)
+ val st = overall_status(name)
tooltip =
"theory " + quote(name.theory) +
- (if (st == Document_Status.Overall_Node_Status.ok) "" else " (" + st + ")")
+ (if (st == Document_Status.Overall_Status.ok) "" else " (" + st + ")")
}
else tooltip = null
}
@@ -249,7 +248,7 @@
else {
(for {
(name, node_status) <- nodes_status1.present().iterator
- if !node_status.is_empty && !node_status.is_suppressed && node_status.total > 0
+ if !node_status.is_empty && !node_status.suppressed && node_status.total > 0
} yield name).toList
}
}
--- a/src/Tools/jEdit/src/timing_dockable.scala Wed Sep 17 12:19:12 2025 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Wed Sep 17 20:57:11 2025 +0200
@@ -106,7 +106,7 @@
/* timing threshold */
- private var timing_threshold = PIDE.options.real("jedit_timing_threshold")
+ private var timing_threshold = PIDE.options.real("editor_timing_threshold")
private val threshold_tooltip = "Threshold for timing display (seconds)"
private val threshold_value = new TextField(Time.print_seconds(timing_threshold)) {
@@ -131,7 +131,7 @@
/* component state -- owned by GUI thread */
- private var nodes_timing = Map.empty[Document.Node.Name, Document_Status.Overall_Timing]
+ private var nodes_status = Document_Status.Nodes_Status.empty
private def make_entries(): List[Entry] = {
GUI_Thread.require {}
@@ -141,14 +141,14 @@
case None => Document.Node.Name.empty
case Some(doc_view) => doc_view.model.node_name
}
- val timing = nodes_timing.getOrElse(name, Document_Status.Overall_Timing.empty)
val theories =
- (for ((node_name, node_timing) <- nodes_timing.toList if node_timing.command_timings.nonEmpty)
- yield Theory_Entry(node_name, node_timing.total)).sorted(Entry.Ordering)
+ List.from(
+ for ((a, st) <- nodes_status.iterator if st.command_timings.nonEmpty)
+ yield Theory_Entry(a, st.total_time.seconds)).sorted(Entry.Ordering)
val commands =
- (for ((command, command_timing) <- timing.command_timings.toList)
- yield Command_Entry(command, command_timing)).sorted(Entry.Ordering)
+ (for ((command, command_timing) <- nodes_status(name).command_timings.toList)
+ yield Command_Entry(command, command_timing.seconds)).sorted(Entry.Ordering)
theories.flatMap(entry =>
if (entry.name == name) entry.make_current :: commands
@@ -160,21 +160,15 @@
val snapshot = PIDE.session.snapshot()
- val nodes_timing1 =
- (restriction match {
- case Some(names) => names.iterator.map(name => (name, snapshot.get_node(name)))
- case None => snapshot.version.nodes.iterator
- }).foldLeft(nodes_timing) {
- case (timing1, (name, node)) =>
- if (PIDE.resources.loaded_theory(name)) timing1
- else {
- val node_timing =
- Document_Status.Overall_Timing.make(
- snapshot.state, snapshot.version, node.commands, threshold = timing_threshold)
- timing1 + (name -> node_timing)
- }
- }
- nodes_timing = nodes_timing1
+ val domain =
+ restriction.getOrElse(
+ snapshot.version.nodes.names_iterator
+ .filterNot(PIDE.resources.loaded_theory).toSet)
+
+ nodes_status =
+ nodes_status.update(PIDE.resources, snapshot.state, snapshot.version,
+ threshold = Time.seconds(timing_threshold),
+ domain = Some(domain))._2
val entries = make_entries()
if (timing_view.listData.toList != entries) timing_view.listData = entries