# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1718094655 -7200
# Node ID f05a71fa1a3f7661e5d524f9ae4d4a02c9bce3ef
# Parent  595b362ab8510a8feed45a91b4ce7b035ddfc9bc
tuned comments;

diff -r 595b362ab851 -r f05a71fa1a3f src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jun 11 08:58:22 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jun 11 10:30:55 2024 +0200
@@ -12,7 +12,7 @@
 
 
 object Build_Manager {
-  /* task state synchronized via db */
+  /** task state synchronized via db **/
 
   object Component {
     def parse(s: String): Component =
@@ -252,7 +252,7 @@
   }
 
 
-  /* SQL data model */
+  /** SQL data model **/
 
   object private_data extends SQL.Data("isabelle_build_manager") {
     /* tables */
@@ -591,7 +591,7 @@
   }
 
 
-  /* running build manager processes */
+  /** running build manager processes **/
 
   abstract class Loop_Process[A](name: String, store: Store, progress: Progress)
     extends Runnable {
@@ -1187,7 +1187,7 @@
   }
 
 
-  /* context */
+  /** context **/
 
   case class Context(store: Store, task: Task, id: Long) {
     def name = Build.name(task.kind, id)
@@ -1207,7 +1207,7 @@
   }
 
 
-  /* build process */
+  /** build process **/
 
   object Build_Process {
     def open(context: Context): Build_Process = new Build_Process(context.open_ssh(), context)
@@ -1274,7 +1274,7 @@
   }
 
 
-  /* build manager store */
+  /** build manager store **/
 
   case class Store(options: Options) {
     val base_dir = Path.explode(options.string("build_manager_dir"))
@@ -1324,6 +1324,8 @@
   }
 
 
+  /** build manager server **/
+
   /* build manager */
 
   def build_manager(
@@ -1416,7 +1418,7 @@
     })
 
 
-  /* restore build manager database */
+  /** restore build manager database **/
 
   def build_manager_database(options: Options, progress: Progress = new Progress): Unit = {
     val store = Store(options)
@@ -1478,6 +1480,8 @@
     })
 
 
+  /** build manager client */
+
   /* build task */
 
   def build_task(