# HG changeset patch
# User wenzelm
# Date 1459861104 -7200
# Node ID 2d5959cf3c1ac5055695bf65274a2e594de16038
# Parent  007c454d0d0fe0d0de1fdb34f375aad8ec5a2ceb
tuned;

diff -r 007c454d0d0f -r 2d5959cf3c1a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 04 23:58:48 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 05 14:58:24 2016 +0200
@@ -18,9 +18,6 @@
 {
   /* info */
 
-  val ROOT = Path.explode("ROOT")
-  val ROOTS = Path.explode("ROOTS")
-
   def is_pure(name: String): Boolean = name == "Pure"
 
   sealed case class Info(
@@ -141,6 +138,9 @@
 
   /* parser */
 
+  val ROOT = Path.explode("ROOT")
+  val ROOTS = Path.explode("ROOTS")
+
   private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
@@ -156,7 +156,7 @@
       (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
       IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
 
-  object Parser extends Parse.Parser
+  private object Parser extends Parse.Parser
   {
     private abstract class Entry
     private sealed case class Chapter(name: String) extends Entry