--- a/src/Pure/Build/build_job.scala Tue Nov 04 17:20:20 2025 +0100
+++ b/src/Pure/Build/build_job.scala Tue Nov 04 20:11:15 2025 +0100
@@ -167,7 +167,8 @@
case None => status
case Some(snapshot) =>
Exn.Interrupt.expose()
- status.update_node(snapshot.state, snapshot.version, snapshot.node_name,
+ status.update_node(Date.now(),
+ snapshot.state, snapshot.version, snapshot.node_name,
threshold = editor_timing_threshold)
}
})
--- a/src/Pure/PIDE/command.scala Tue Nov 04 17:20:20 2025 +0100
+++ b/src/Pure/PIDE/command.scala Tue Nov 04 20:11:15 2025 +0100
@@ -217,7 +217,7 @@
markups: Markups = Markups.empty,
): State = {
new State(command, results, exports, markups,
- Document_Status.Command_Status.make(Time.now(),
+ Document_Status.Command_Status.make(Date.now(),
warned = results.warned,
failed = results.failed))
}
@@ -252,11 +252,11 @@
new Command(id, command.node_name, command.blobs_info, command.span, command.source,
results, exports, markups, document_status)
- private def add_status(now: Time, st: Markup): State =
+ private def add_status(now: Date, st: Markup): State =
new State(command, results, exports, markups,
document_status.update(now, markups = List(st)))
- private def add_result(now: Time, entry: Results.Entry): State =
+ private def add_result(now: Date, entry: Results.Entry): State =
new State(command, results + entry, exports, markups,
document_status.update(now,
warned = Results.warned(entry),
@@ -282,7 +282,7 @@
}
def accumulate(
- now: Time,
+ now: Date,
self_id: Document_ID.Generic => Boolean,
other_id: (Document.Node.Name, Document_ID.Generic) =>
Option[(Symbol.Text_Chunk.Id, Symbol.Text_Chunk)],
@@ -623,7 +623,7 @@
lazy val init_state: Command.State =
new Command.State(this, init_results, init_exports, init_markups,
- init_document_status.update(Time.now(),
+ init_document_status.update(Date.now(),
warned = init_results.warned,
failed = init_results.failed))
--- a/src/Pure/PIDE/document.scala Tue Nov 04 17:20:20 2025 +0100
+++ b/src/Pure/PIDE/document.scala Tue Nov 04 20:11:15 2025 +0100
@@ -1036,7 +1036,7 @@
message: XML.Elem,
cache: XML.Cache
) : (Command.State, State) = {
- val now = Time.now()
+ val now = Date.now()
def update(st: Command.State): (Command.State, State) = {
val st1 = st.accumulate(now, self_id(st), other_id, message, cache)
(st1, copy(commands_redirection = redirection(st1)))
--- a/src/Pure/PIDE/document_status.scala Tue Nov 04 17:20:20 2025 +0100
+++ b/src/Pure/PIDE/document_status.scala Tue Nov 04 20:11:15 2025 +0100
@@ -36,6 +36,7 @@
/* command timings: for pro-forma command with actual commands at offset */
object Command_Timings {
+ type Entry0 = (Symbol.Offset, Date)
type Entry = (Symbol.Offset, Time)
val empty: Command_Timings =
new Command_Timings(SortedMap.empty, SortedMap.empty, Time.zero)
@@ -44,14 +45,14 @@
}
final class Command_Timings private(
- private val running: SortedMap[Symbol.Offset, Time], // start time (in Scala)
+ private val running: SortedMap[Symbol.Offset, Date], // start time (in Scala)
private val finished: SortedMap[Symbol.Offset, Time], // elapsed time (in ML)
private val sum_finished: Time
) {
def is_empty: Boolean = running.isEmpty && finished.isEmpty
def has_running: Boolean = running.nonEmpty
- def add_running(entry: Command_Timings.Entry): Command_Timings =
+ def add_running(entry: Command_Timings.Entry0): Command_Timings =
new Command_Timings(running + entry, finished, sum_finished)
def count_finished: Int = finished.size
@@ -64,7 +65,7 @@
new Command_Timings(running1, finished1, sum_finished1)
}
- def sum(now: Time): Time =
+ def sum(now: Date): Time =
running.valuesIterator.foldLeft(sum_finished)({ case (t, t0) => t + (now - t0) })
def ++ (other: Command_Timings): Command_Timings =
@@ -107,7 +108,7 @@
timings = Command_Timings.empty)
def make(
- now: Time,
+ now: Date,
markups: List[Markup] = Nil,
warned: Boolean = false,
failed: Boolean = false
@@ -158,7 +159,7 @@
}
def update(
- now: Time,
+ now: Date,
markups: List[Markup] = Nil,
warned: Boolean = false,
failed: Boolean = false
@@ -241,13 +242,12 @@
val empty: Node_Status = Node_Status()
def make(
+ now: Date,
state: Document.State,
version: Document.Version,
name: Document.Node.Name,
threshold: Time = Time.max
): Node_Status = {
- val now = Time.now()
-
val node = version.nodes(name)
var theory_status = Document_Status.Theory_Status.NONE
@@ -382,16 +382,19 @@
}
def update_node(
+ now: Date,
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)
+ val node_status =
+ Document_Status.Node_Status.make(now, state, version, name, threshold = threshold)
new Nodes_Status(rep + (name -> node_status))
}
def update_nodes(
+ now: Date,
resources: Resources,
state: Document.State,
version: Document.Version,
@@ -404,7 +407,7 @@
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) })
+ else a.update_node(now, state, version, name, threshold = threshold) })
if (trim) new Nodes_Status(that.rep -- that.rep.keysIterator.filterNot(domain1))
else that
}
--- a/src/Pure/PIDE/headless.scala Tue Nov 04 17:20:20 2025 +0100
+++ b/src/Pure/PIDE/headless.scala Tue Nov 04 20:11:15 2025 +0100
@@ -129,7 +129,7 @@
load_state: Load_State,
watchdog_timeout: Time,
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit],
- last_update: Time = Time.now(),
+ last_update: Date = Date.now(),
nodes_status: Document_Status.Nodes_Status = Document_Status.Nodes_Status.empty,
already_committed: Map[Document.Node.Name, Document_Status.Node_Status] = Map.empty,
changed_nodes: Set[Document.Node.Name] = Set.empty,
@@ -140,9 +140,10 @@
domain: Option[Set[Document.Node.Name]] = None,
trim: Boolean = false
): (Boolean, Use_Theories_State) = {
+ val now = Date.now()
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.update_nodes(now, resources, state, version, domain = domain, trim = trim)
+ val st1 = copy(last_update = now, nodes_status = nodes_status1)
(nodes_status1 != nodes_status, st1)
}
@@ -160,7 +161,7 @@
else copy(changed_nodes = Set.empty, changed_assignment = false)
def watchdog: Boolean =
- watchdog_timeout > Time.zero && Time.now() - last_update > watchdog_timeout
+ watchdog_timeout > Time.zero && Date.now() - last_update > watchdog_timeout
def finished_result: Boolean = result.isDefined
@@ -230,7 +231,7 @@
if (!committed.isDefinedAt(name) && parents_committed &&
state.node_consolidated(version, name)) {
val snapshot = stable_snapshot(state, version, name)
- val status = Document_Status.Node_Status.make(state, version, name)
+ val status = Document_Status.Node_Status.make(Date.now(), state, version, name)
commit_fn(snapshot, status)
committed + (name -> status)
}
@@ -251,6 +252,7 @@
if (!finished_result && load_theories.isEmpty &&
(stopped || dep_graph.keys_iterator.forall(consolidated(state, version, _)))
) {
+ val now = Date.now()
@tailrec def make_nodes(
input: List[Document.Node.Name],
output: List[(Document.Node.Name, Document_Status.Node_Status)]
@@ -259,7 +261,7 @@
case name :: rest =>
if (resources.loaded_theory(name)) make_nodes(rest, output)
else {
- val status = Document_Status.Node_Status.make(state, version, name)
+ val status = Document_Status.Node_Status.make(now, state, version, name)
val ok = if (commit.isDefined) committed(name) else status.consolidated
if (stopped || ok) make_nodes(rest, (name -> status) :: output) else None
}
--- a/src/Pure/PIDE/rendering.scala Tue Nov 04 17:20:20 2025 +0100
+++ b/src/Pure/PIDE/rendering.scala Tue Nov 04 20:11:15 2025 +0100
@@ -469,7 +469,7 @@
range: Text.Range,
focus: Rendering.Focus
) : List[Text.Info[Rendering.Color.Value]] = {
- val now = Time.now()
+ val now = Date.now()
for {
Text.Info(r, result) <-
snapshot.cumulate[(List[Markup], Option[Rendering.Color.Value])](
@@ -764,7 +764,7 @@
/* command status overview */
def overview_color(range: Text.Range): Option[Rendering.Color.Value] = {
- val now = Time.now()
+ val now = Date.now()
if (snapshot.is_outdated) None
else {
val results =
--- a/src/Tools/jEdit/src/theories_status.scala Tue Nov 04 17:20:20 2025 +0100
+++ b/src/Tools/jEdit/src/theories_status.scala Tue Nov 04 20:11:15 2025 +0100
@@ -235,8 +235,10 @@
val snapshot = PIDE.session.snapshot()
+ val now = Date.now()
+
val nodes_status1 =
- nodes_status.update_nodes(
+ nodes_status.update_nodes(now,
PIDE.resources, snapshot.state, snapshot.version, domain = domain, trim = trim)
if (force || nodes_status1 != nodes_status) {
--- a/src/Tools/jEdit/src/timing_dockable.scala Tue Nov 04 17:20:20 2025 +0100
+++ b/src/Tools/jEdit/src/timing_dockable.scala Tue Nov 04 20:11:15 2025 +0100
@@ -142,7 +142,7 @@
case Some(doc_view) => doc_view.model.node_name
}
- val now = Time.now()
+ val now = Date.now()
val theories =
List.from(
@@ -168,7 +168,7 @@
.filterNot(PIDE.resources.loaded_theory).toSet)
nodes_status =
- nodes_status.update_nodes(PIDE.resources, snapshot.state, snapshot.version,
+ nodes_status.update_nodes(Date.now(), PIDE.resources, snapshot.state, snapshot.version,
threshold = Time.seconds(timing_threshold),
domain = Some(domain))