--- 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) ~!