--- 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(