--- a/src/Pure/Build/sessions.scala Sun Aug 10 12:27:39 2025 +0200
+++ b/src/Pure/Build/sessions.scala Sun Aug 10 15:17:13 2025 +0200
@@ -619,11 +619,14 @@
chapter_defs: Chapter_Defs = Chapter_Defs.empty,
chapter: String = UNSORTED,
dir_selected: Boolean = false,
+ draft_session: Boolean = false
): Info = {
try {
- val name = entry.name
+ val name =
+ if (draft_session) DRAFT
+ else if (illegal_session(entry.name)) error("Illegal session name " + quote(entry.name))
+ else entry.name
- if (illegal_session(name)) error("Illegal session name " + quote(name))
if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")