# HG changeset patch
# User wenzelm
# Date 1513423726 -3600
# Node ID f80bdbe76934ec6ddc9552dfef0638277f5df74e
# Parent  fca5f298809176cdbe89a1e3ebc56a37faa15b64
tuned;

diff -r fca5f2988091 -r f80bdbe76934 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Dec 16 12:27:10 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Dec 16 12:28:46 2017 +0100
@@ -696,8 +696,8 @@
     private val session_entry: Parser[Session_Entry] =
     {
       val option =
-        option_name ~ opt($$$("=") ~! option_value ^^
-          { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
+        option_name ~ opt($$$("=") ~! option_value ^^ { case _ ~ x => x }) ^^
+          { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
       val global =
@@ -713,8 +713,8 @@
 
       val document_files =
         $$$(DOCUMENT_FILES) ~!
-          (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
-              { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
+          (($$$("(") ~! ($$$(IN) ~ path ~ $$$(")")) ^^
+              { case _ ~ (_ ~ x ~ _) => x } | success("document")) ~
             rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
 
       command(SESSION) ~!