# HG changeset patch
# User wenzelm
# Date 1676142330 -3600
# Node ID 2e5a3955bc69776ae9b638b6d8644b7453c26eea
# Parent  629dce95bb5cbaec14f5d2c294fee6dc7b1e329a
clarified signature and terminology;

diff -r 629dce95bb5c -r 2e5a3955bc69 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Feb 11 16:38:29 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 20:05:30 2023 +0100
@@ -61,12 +61,12 @@
 
       val timings =
         for (session <- graph.keys)
-          yield Build_Process.Session_Timing.load(session, store, progress = progress)
+          yield Build_Process.Session_Context.load(session, store, progress = progress)
       val command_timings =
-        timings.map(timing => timing.session -> timing.command_timings).toMap.withDefaultValue(Nil)
+        timings.map(timing => timing.session -> timing.old_command_timings).toMap.withDefaultValue(Nil)
       val session_timing =
         make_session_timing(sessions_structure,
-          timings.map(timing => timing.session -> timing.elapsed.seconds).toMap)
+          timings.map(timing => timing.session -> timing.old_time.seconds).toMap)
 
       object Ordering extends scala.math.Ordering[String] {
         def compare(name1: String, name2: String): Int =
diff -r 629dce95bb5c -r 2e5a3955bc69 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Feb 11 16:38:29 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 20:05:30 2023 +0100
@@ -9,16 +9,16 @@
 
 
 object Build_Process {
-  /* timings from session database */
+  /* static information */
 
-  object Session_Timing {
-    def empty(session: String): Session_Timing = new Session_Timing(session, Time.zero, Nil)
+  object Session_Context {
+    def empty(session: String): Session_Context = new Session_Context(session, Time.zero, Nil)
 
     def load(
       session: String,
       store: Sessions.Store,
       progress: Progress = new Progress
-    ): Session_Timing = {
+    ): Session_Context = {
       store.try_open_database(session) match {
         case None => empty(session)
         case Some(db) =>
@@ -34,7 +34,7 @@
                 case Markup.Elapsed(s) => Time.seconds(s)
                 case _ => Time.zero
               }
-            new Session_Timing(session, elapsed, command_timings)
+            new Session_Context(session, elapsed, command_timings)
           }
           catch {
             case ERROR(msg) => ignore_error(msg)
@@ -46,14 +46,14 @@
     }
   }
 
-  final class Session_Timing(
+  final class Session_Context(
     val session: String,
-    val elapsed: Time,
-    val command_timings: List[Properties.T]
+    val old_time: Time,
+    val old_command_timings: List[Properties.T]
   ) {
-    def is_empty: Boolean = elapsed.is_zero && command_timings.isEmpty
+    def is_empty: Boolean = old_time.is_zero && old_command_timings.isEmpty
 
     override def toString: String =
-      session + (if (elapsed.seconds > 0.0) " (" + elapsed.message_hms + " elapsed time)" else "")
+      session + (if (old_time.seconds > 0.0) " (" + old_time.message_hms + " elapsed time)" else "")
   }
 }