# HG changeset patch
# User wenzelm
# Date 1677701720 -3600
# Node ID 8008ce0f2488a13e1a5c41c3b25ddd14a6a6ef54
# Parent  4e8bec105ce5a1b5070f1394ef2947e17d31c770
more explicit session name, in anticipation of variants like "session.document", "session.browser_info";

diff -r 4e8bec105ce5 -r 8008ce0f2488 src/Pure/Tools/build_job.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,
diff -r 4e8bec105ce5 -r 8008ce0f2488 src/Pure/Tools/build_process.scala
--- 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()