tuned;
authorwenzelm
Sat Dec 16 12:28:46 2017 +0100 (17 months ago)
changeset 67210f80bdbe76934
parent 67209 fca5f2988091
child 67211 9e9b78b8e6ca
tuned;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Sat Dec 16 12:27:10 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sat Dec 16 12:28:46 2017 +0100
     1.3 @@ -696,8 +696,8 @@
     1.4      private val session_entry: Parser[Session_Entry] =
     1.5      {
     1.6        val option =
     1.7 -        option_name ~ opt($$$("=") ~! option_value ^^
     1.8 -          { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
     1.9 +        option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
    1.10 +          { case x ~ y => (x, y) }
    1.11        val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
    1.12  
    1.13        val global =
    1.14 @@ -713,8 +713,8 @@
    1.15  
    1.16        val document_files =
    1.17          $$$(DOCUMENT_FILES) ~!
    1.18 -          (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
    1.19 -              { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
    1.20 +          (($$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^
    1.21 +              { case _ ~ (_ ~ x ~ _) => x } | success("document")) ~
    1.22              rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
    1.23  
    1.24        command(SESSION) ~!