# HG changeset patch
# User wenzelm
# Date 1676279850 -3600
# Node ID 2bf3217583335eef9b95b95f7cb422aa110fa25a
# Parent  9a60a2d19a4c2876f7107c6cb961b57a56540f16
clarified modules;

diff -r 9a60a2d19a4c -r 2bf321758333 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Feb 12 22:05:02 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Feb 13 10:17:30 2023 +0100
@@ -1331,6 +1331,18 @@
 
   /** persistent store **/
 
+  /** auxiliary **/
+
+  sealed case class Build_Info(
+    sources: SHA1.Shasum,
+    input_heaps: SHA1.Shasum,
+    output_heap: SHA1.Shasum,
+    return_code: Int,
+    uuid: String
+  ) {
+    def ok: Boolean = return_code == 0
+  }
+
   object Session_Info {
     val session_name = SQL.Column.string("session_name").make_primary_key
 
@@ -1345,7 +1357,7 @@
       List(session_name, session_timing, command_timings, theory_timings,
         ml_statistics, task_statistics, errors)
 
-    // Build.Session_Info
+    // Build_Info
     val sources = SQL.Column.string("sources")
     val input_heaps = SQL.Column.string("input_heaps")
     val output_heap = SQL.Column.string("output_heap")
@@ -1553,7 +1565,7 @@
       session_name: String,
       sources: Sources,
       build_log: Build_Log.Session_Info,
-      build: Build.Session_Info
+      build: Build_Info
     ): Unit = {
       db.transaction {
         write_sources(db, session_name, sources)
@@ -1596,7 +1608,7 @@
     def read_errors(db: SQL.Database, name: String): List[String] =
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors), cache = cache)
 
-    def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] = {
+    def read_build(db: SQL.Database, name: String): Option[Build_Info] = {
       if (db.tables.contains(Session_Info.table.name)) {
         db.using_statement(Session_Info.table.select(Nil,
           Session_Info.session_name.where_equal(name))) { stmt =>
@@ -1607,7 +1619,7 @@
               try { Option(res.string(Session_Info.uuid)).getOrElse("") }
               catch { case _: SQLException => "" }
             Some(
-              Build.Session_Info(
+              Build_Info(
                 SHA1.fake_shasum(res.string(Session_Info.sources)),
                 SHA1.fake_shasum(res.string(Session_Info.input_heaps)),
                 SHA1.fake_shasum(res.string(Session_Info.output_heap)),
diff -r 9a60a2d19a4c -r 2bf321758333 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Feb 12 22:05:02 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Feb 13 10:17:30 2023 +0100
@@ -9,22 +9,6 @@
 
 
 object Build {
-  /** auxiliary **/
-
-  /* persistent build info */
-
-  sealed case class Session_Info(
-    sources: SHA1.Shasum,
-    input_heaps: SHA1.Shasum,
-    output_heap: SHA1.Shasum,
-    return_code: Int,
-    uuid: String
-  ) {
-    def ok: Boolean = return_code == 0
-  }
-
-
-
   /** build with results **/
 
   class Results private[Build](
diff -r 9a60a2d19a4c -r 2bf321758333 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Feb 12 22:05:02 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Feb 13 10:17:30 2023 +0100
@@ -236,7 +236,7 @@
         build_log =
           if (process_result.timeout) build_log.error("Timeout") else build_log,
         build =
-          Build.Session_Info(build_deps.sources_shasum(session_name), input_heaps,
+          Sessions.Build_Info(build_deps.sources_shasum(session_name), input_heaps,
             output_heap, process_result.rc, UUID.random().toString)))
 
     // messages