# HG changeset patch
# User wenzelm
# Date 1677666654 -3600
# Node ID c10fa027caa06dadbff1ad1723476e03596bf810
# Parent  9bd6c78b3b77a3f0b16cb7afa38a8fa331624fe6
tuned comments and outline;

diff -r 9bd6c78b3b77 -r c10fa027caa0 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 28 20:37:57 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 11:30:54 2023 +0100
@@ -13,7 +13,7 @@
 
 
 object Build_Process {
-  /* static context */
+  /** static context **/
 
   object Session_Context {
     def empty(session: String, timeout: Time): Session_Context =
@@ -154,7 +154,8 @@
   }
 
 
-  /* dynamic state */
+
+  /** dynamic state **/
 
   case class Entry(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) {
     def is_ready: Boolean = deps.isEmpty
@@ -226,7 +227,8 @@
   }
 
 
-  /* SQL data model */
+
+  /** SQL data model **/
 
   object Data {
     val database = Path.explode("$ISABELLE_HOME_USER/build.db")
@@ -506,9 +508,13 @@
 }
 
 
-/* main process */
+
+/** main process **/
 
-class Build_Process(protected val build_context: Build_Process.Context) extends AutoCloseable {
+class Build_Process(protected val build_context: Build_Process.Context)
+extends AutoCloseable {
+  /* context */
+
   protected val store: Sessions.Store = build_context.store
   protected val build_options: Options = store.options
   protected val build_deps: Sessions.Deps = build_context.deps
@@ -522,6 +528,9 @@
       case log_file => Logger.make(Some(Path.explode(log_file)))
     }
 
+
+  /* database */
+
   protected val database: Option[SQL.Database] =
     if (!build_options.bool("build_database_test")) None
     else if (store.database_server) Some(store.open_database_server())
@@ -534,7 +543,29 @@
 
   def close(): Unit = database.foreach(_.close())
 
-  // global state
+  protected def setup_database(): Unit =
+    for (db <- database) {
+      synchronized {
+        db.transaction {
+          Build_Process.Data.init_database(db, build_context)
+        }
+      }
+      db.rebuild()
+    }
+  protected def sync_database(): Unit =
+    for (db <- database) {
+      synchronized {
+        db.transaction {
+          _state =
+            Build_Process.Data.update_database(
+              db, build_context.instance, build_context.hostname, _state)
+        }
+      }
+    }
+
+
+  /* global state */
+
   protected var _state: Build_Process.State = init_state(Build_Process.State())
 
   protected def init_state(state: Build_Process.State): Build_Process.State = {
@@ -647,25 +678,8 @@
     }
   }
 
-  protected def setup_database(): Unit =
-    for (db <- database) {
-      synchronized {
-        db.transaction {
-          Build_Process.Data.init_database(db, build_context)
-        }
-      }
-      db.rebuild()
-    }
-  protected def sync_database(): Unit =
-    for (db <- database) {
-      synchronized {
-        db.transaction {
-          _state =
-            Build_Process.Data.update_database(
-              db, build_context.instance, build_context.hostname, _state)
-        }
-      }
-    }
+
+  /* run */
 
   protected def sleep(): Unit =
     Isabelle_Thread.interrupt_handler(_ => progress.stop()) {