tuned signature -- accomodate operations of ROOT files;
authorwenzelm
Tue Apr 29 12:00:50 2014 +0200 (2014-04-29)
changeset 56780e76467fed375
parent 56779 9823818588fb
child 56781 f2eb0f22589f
tuned signature -- accomodate operations of ROOT files;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Tue Apr 29 11:14:39 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Tue Apr 29 12:00:50 2014 +0200
     1.3 @@ -208,16 +208,16 @@
     1.4        (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
     1.5        IN + DESCRIPTION + OPTIONS + THEORIES + FILES + DOCUMENT_FILES
     1.6  
     1.7 -  private object Parser extends Parse.Parser
     1.8 +  object Parser extends Parse.Parser
     1.9    {
    1.10 -    val chapter: Parser[Chapter] =
    1.11 +    private val chapter: Parser[Chapter] =
    1.12      {
    1.13        val chapter_name = atom("chapter name", _.is_name)
    1.14  
    1.15        command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) }
    1.16      }
    1.17  
    1.18 -    val session_entry: Parser[Session_Entry] =
    1.19 +    private val session_entry: Parser[Session_Entry] =
    1.20      {
    1.21        val session_name = atom("session name", _.is_name)
    1.22