more explicit session name, in anticipation of variants like "session.document", "session.browser_info";
authorwenzelm
Wed, 01 Mar 2023 21:15:20 +0100
changeset 77464 8008ce0f2488
parent 77463 4e8bec105ce5
child 77465 ecfe6dac3a3e
more explicit session name, in anticipation of variants like "session.document", "session.browser_info";
src/Pure/Tools/build_job.scala
src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_job.scala	Wed Mar 01 21:07:59 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Mar 01 21:15:20 2023 +0100
@@ -39,6 +39,8 @@
 
   /* build session */
 
+  def is_session_name(job_name: String): Boolean = !Long_Name.is_qualified(job_name)
+
   object Session_Context {
     def load(
       name: String,
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 21:07:59 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 21:15:20 2023 +0100
@@ -551,7 +551,7 @@
     }
     else None
 
-  protected def start_job(session_name: String): Unit = {
+  protected def start_session(session_name: String): Unit = {
     val ancestor_results = synchronized {
       _state.get_results(build_context.sessions(session_name).ancestors)
     }
@@ -671,7 +671,8 @@
 
         synchronized { next_job(_state) } match {
           case Some(name) =>
-            start_job(name)
+            if (Build_Job.is_session_name(name)) start_session(name)
+            else error("Unsupported build job name " + quote(name))
           case None =>
             sync_database()
             sleep()