# HG changeset patch
# User wenzelm
# Date 1607257340 -3600
# Node ID 03803bbfdca35a4ac7157eedb7aac768a56ca8c4
# Parent  ffae996e9c08683a5fda0f598df79cdb1732accd
tuned signature;

diff -r ffae996e9c08 -r 03803bbfdca3 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Dec 06 13:03:26 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sun Dec 06 13:22:20 2020 +0100
@@ -19,6 +19,9 @@
 {
   /* session and theory names */
 
+  val ROOT: Path = Path.explode("ROOT")
+  val ROOTS: Path = Path.explode("ROOTS")
+
   val root_name: String = "ROOT"
   val theory_name: String = "Pure.Sessions"
 
@@ -834,9 +837,6 @@
 
   /* parser */
 
-  val ROOT: Path = Path.explode("ROOT")
-  val ROOTS: Path = Path.explode("ROOTS")
-
   private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
diff -r ffae996e9c08 -r 03803bbfdca3 src/Pure/Tools/mkroot.scala
--- a/src/Pure/Tools/mkroot.scala	Sun Dec 06 13:03:26 2020 +0100
+++ b/src/Pure/Tools/mkroot.scala	Sun Dec 06 13:22:20 2020 +0100
@@ -32,7 +32,7 @@
     val name = proper_string(session_name) getOrElse session_dir.absolute_file.getName
     val parent = proper_string(session_parent) getOrElse Isabelle_System.getenv("ISABELLE_LOGIC")
 
-    val root_path = session_dir + Path.explode("ROOT")
+    val root_path = session_dir + Sessions.ROOT
     if (root_path.file.exists) error("Cannot overwrite existing " + root_path)
 
     val document_path = session_dir + Path.explode("document")