# HG changeset patch
# User wenzelm
# Date 1676112133 -3600
# Node ID 02308a0ddf30327faba346833c41870a711f9553
# Parent  f947e045fa61603ce9ef59476a17365d788fec5f
clarified modules;

diff -r f947e045fa61 -r 02308a0ddf30 etc/build.props
--- a/etc/build.props	Sat Feb 11 11:06:38 2023 +0100
+++ b/etc/build.props	Sat Feb 11 11:42:13 2023 +0100
@@ -186,6 +186,7 @@
   src/Pure/Tools/build.scala \
   src/Pure/Tools/build_docker.scala \
   src/Pure/Tools/build_job.scala \
+  src/Pure/Tools/build_process.scala \
   src/Pure/Tools/check_keywords.scala \
   src/Pure/Tools/debugger.scala \
   src/Pure/Tools/doc.scala \
diff -r f947e045fa61 -r 02308a0ddf30 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Feb 11 11:06:38 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 11:42:13 2023 +0100
@@ -31,37 +31,6 @@
   /* queue with scheduling information */
 
   private object Queue {
-    type Timings = (List[Properties.T], Double)
-
-    def load_timings(progress: Progress, store: Sessions.Store, session_name: String): Timings = {
-      val no_timings: Timings = (Nil, 0.0)
-
-      store.try_open_database(session_name) match {
-        case None => no_timings
-        case Some(db) =>
-          def ignore_error(msg: String) = {
-            progress.echo_warning("Ignoring bad database " + db +
-              " for session " + quote(session_name) + (if (msg == "") "" else ":\n" + msg))
-            no_timings
-          }
-          try {
-            val command_timings = store.read_command_timings(db, session_name)
-            val session_timing =
-              store.read_session_timing(db, session_name) match {
-                case Markup.Elapsed(t) => t
-                case _ => 0.0
-              }
-            (command_timings, session_timing)
-          }
-          catch {
-            case ERROR(msg) => ignore_error(msg)
-            case exn: java.lang.Error => ignore_error(Exn.message(exn))
-            case _: XML.Error => ignore_error("XML.Error")
-          }
-          finally { db.close() }
-      }
-    }
-
     def make_session_timing(
       sessions_structure: Sessions.Structure,
       timing: Map[String, Double]
@@ -90,7 +59,8 @@
       val graph = sessions_structure.build_graph
       val names = graph.keys
 
-      val timings = names.map(name => (name, load_timings(progress, store, name)))
+      val timings =
+        names.map(name => (name, Build_Process.Session_Timing.load(progress, store, name)))
       val command_timings =
         timings.map({ case (name, (ts, _)) => (name, ts) }).toMap.withDefaultValue(Nil)
       val session_timing =
diff -r f947e045fa61 -r 02308a0ddf30 src/Pure/Tools/build_process.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/build_process.scala	Sat Feb 11 11:42:13 2023 +0100
@@ -0,0 +1,46 @@
+/*  Title:      Pure/Tools/build_process.scala
+    Author:     Makarius
+
+Build process for sessions, with build database, optional heap, and
+optional presentation.
+*/
+
+package isabelle
+
+
+object Build_Process {
+  /* timings from session database */
+
+  type Session_Timing = (List[Properties.T], Double)
+
+  object Session_Timing {
+    val empty: Session_Timing = (Nil, 0.0)
+
+    def load(progress: Progress, store: Sessions.Store, session_name: String): Session_Timing = {
+      store.try_open_database(session_name) match {
+        case None => empty
+        case Some(db) =>
+          def ignore_error(msg: String) = {
+            progress.echo_warning("Ignoring bad database " + db +
+              " for session " + quote(session_name) + (if (msg == "") "" else ":\n" + msg))
+            empty
+          }
+          try {
+            val command_timings = store.read_command_timings(db, session_name)
+            val session_timing =
+              store.read_session_timing(db, session_name) match {
+                case Markup.Elapsed(t) => t
+                case _ => 0.0
+              }
+            (command_timings, session_timing)
+          }
+          catch {
+            case ERROR(msg) => ignore_error(msg)
+            case exn: java.lang.Error => ignore_error(Exn.message(exn))
+            case _: XML.Error => ignore_error("XML.Error")
+          }
+          finally { db.close() }
+      }
+    }
+  }
+}