more explicit session name, in anticipation of variants like "session.document", "session.browser_info";
--- 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()