# HG changeset patch
# User wenzelm
# Date 1677098310 -3600
# Node ID 5a84de89170dafff68ce0aa3cdc160ab49ab6b94
# Parent  885842575e2a662b6fe59a64cee911c9a4e95ae5
more operations to support management of jobs, e.g. from external database;

diff -r 885842575e2a -r 5a84de89170d src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Feb 22 21:35:55 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Feb 22 21:38:30 2023 +0100
@@ -12,15 +12,23 @@
 
 
 trait Build_Job {
-  def session_name: String
+  def job_name: String
   def numa_node: Option[Int] = None
   def start(): Unit = ()
   def terminate(): Unit = ()
   def is_finished: Boolean = false
   def join: Process_Result = Process_Result.undefined
+  def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, numa_node)
 }
 
 object Build_Job {
+  case class Abstract(
+    override val job_name: String,
+    override val numa_node: Option[Int]
+  ) extends Build_Job {
+    override def make_abstract: Abstract = this
+  }
+
   class Build_Session(progress: Progress,
     session_background: Sessions.Background,
     store: Sessions.Store,
@@ -31,6 +39,8 @@
     override val numa_node: Option[Int]
   ) extends Build_Job {
     def session_name: String = session_background.session_name
+    def job_name: String = session_name
+
     val info: Sessions.Info = session_background.sessions_structure(session_name)
     val options: Options = NUMA.policy_options(info.options, numa_node)