--- /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() }
+ }
+ }
+ }
+}