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"