# HG changeset patch
# User wenzelm
# Date 1398765650 -7200
# Node ID e76467fed375ccfefc41bb58120cea912f90a050
# Parent  9823818588fb93f27bbefa45bce53d073e73d519
tuned signature -- accomodate operations of ROOT files;

diff -r 9823818588fb -r e76467fed375 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 29 11:14:39 2014 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 29 12:00:50 2014 +0200
@@ -208,16 +208,16 @@
       (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
       IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES
 
-  private object Parser extends Parse.Parser
+  object Parser extends Parse.Parser
   {
-    val chapter: Parser[Chapter] =
+    private val chapter: Parser[Chapter] =
     {
       val chapter_name = atom("chapter name", _.is_name)
 
       command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
     }
 
-    val session_entry: Parser[Session_Entry] =
+    private val session_entry: Parser[Session_Entry] =
     {
       val session_name = atom("session name", _.is_name)