# HG changeset patch
# User wenzelm
# Date 1708541975 -3600
# Node ID 0554a32a6ef4ff37d98cbeebc1678267458dcf8d
# Parent  ade429ddb1fc7fc1d68a8f626e0569cceaff061e
clarified signature;

diff -r ade429ddb1fc -r 0554a32a6ef4 src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Wed Feb 21 19:54:17 2024 +0100
+++ b/src/Pure/Admin/build_history.scala	Wed Feb 21 19:59:35 2024 +0100
@@ -282,7 +282,7 @@
       build_out_progress.echo("Reading session build info ...")
       val session_build_info =
         build_info.finished_sessions.flatMap { session_name =>
-          val database = isabelle_output + store.log_db(session_name)
+          val database = isabelle_output + Store.log_db(session_name)
 
           if (database.is_file) {
             using(SQLite.open_database(database)) { db =>
@@ -309,8 +309,8 @@
       build_out_progress.echo("Reading ML statistics ...")
       val ml_statistics =
         build_info.finished_sessions.flatMap { session_name =>
-          val database = isabelle_output + store.log_db(session_name)
-          val log_gz = isabelle_output + store.log_gz(session_name)
+          val database = isabelle_output + Store.log_db(session_name)
+          val log_gz = isabelle_output + Store.log_gz(session_name)
 
           val properties =
             if (database.is_file) {
@@ -336,7 +336,7 @@
       build_out_progress.echo("Reading error messages ...")
       val session_errors =
         build_info.failed_sessions.flatMap { session_name =>
-          val database = isabelle_output + store.log_db(session_name)
+          val database = isabelle_output + Store.log_db(session_name)
           val errors =
             if (database.is_file) {
               try {
diff -r ade429ddb1fc -r 0554a32a6ef4 src/Pure/Build/store.scala
--- a/src/Pure/Build/store.scala	Wed Feb 21 19:54:17 2024 +0100
+++ b/src/Pure/Build/store.scala	Wed Feb 21 19:59:35 2024 +0100
@@ -18,6 +18,14 @@
   ): Store = new Store(options, build_cluster, cache)
 
 
+  /* file names */
+
+  def heap(name: String): Path = Path.basic(name)
+  def log(name: String): Path = Path.basic("log") + Path.basic(name)
+  def log_db(name: String): Path = log(name).db
+  def log_gz(name: String): Path = log(name).gz
+
+
   /* session */
 
   final class Session private[Store](
@@ -295,22 +303,17 @@
 
   /* file names */
 
-  def heap(name: String): Path = Path.basic(name)
-  def log(name: String): Path = Path.basic("log") + Path.basic(name)
-  def log_db(name: String): Path = log(name).db
-  def log_gz(name: String): Path = log(name).gz
-
-  def output_heap(name: String): Path = output_dir + heap(name)
-  def output_log(name: String): Path = output_dir + log(name)
-  def output_log_db(name: String): Path = output_dir + log_db(name)
-  def output_log_gz(name: String): Path = output_dir + log_gz(name)
+  def output_heap(name: String): Path = output_dir + Store.heap(name)
+  def output_log(name: String): Path = output_dir + Store.log(name)
+  def output_log_db(name: String): Path = output_dir + Store.log_db(name)
+  def output_log_gz(name: String): Path = output_dir + Store.log_gz(name)
 
 
   /* session */
 
   def get_session(name: String): Store.Session = {
-    val heap = input_dirs.view.map(_ + store.heap(name)).find(_.is_file)
-    val log_db = input_dirs.view.map(_ + store.log_db(name)).find(_.is_file)
+    val heap = input_dirs.view.map(_ + Store.heap(name)).find(_.is_file)
+    val log_db = input_dirs.view.map(_ + Store.log_db(name)).find(_.is_file)
     new Store.Session(name, heap, log_db, input_dirs)
   }
 
@@ -402,7 +405,7 @@
     else {
       (for {
         dir <- input_dirs.view
-        path = dir + log_db(name) if path.is_file
+        path = dir + Store.log_db(name) if path.is_file
         db <- check(SQLite.open_database(path))
       } yield db).headOption
     }
@@ -434,7 +437,7 @@
       for {
         dir <-
           (if (system_heaps) List(user_output_dir, system_output_dir) else List(user_output_dir))
-        file <- List(heap(name), log_db(name), log(name), log_gz(name))
+        file <- List(Store.heap(name), Store.log_db(name), Store.log(name), Store.log_gz(name))
         path = dir + file if path.is_file
       } yield path.file.delete