# HG changeset patch
# User wenzelm
# Date 1427287552 -3600
# Node ID 6b0d9e8ac227689a1c6ae12b294a3356e86607a7
# Parent  e749a0f2f401f3c377893e350a1b3dc1e3aaa0f0
clarified position;

diff -r e749a0f2f401 -r 6b0d9e8ac227 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Wed Mar 25 13:31:47 2015 +0100
+++ b/src/Pure/System/options.scala	Wed Mar 25 13:45:52 2015 +0100
@@ -93,9 +93,9 @@
     {
       command(SECTION) ~! text ^^
         { case _ ~ a => (options: Options) => options.set_section(a) } |
-      opt(command(PUBLIC)) ~ position(command(OPTION)) ~! (option_name ~ $$$(":") ~ option_type ~
+      opt(command(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
       $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
-        { case a ~ ((_, pos)) ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
+        { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) =>
             (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
     }
 
diff -r e749a0f2f401 -r 6b0d9e8ac227 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Wed Mar 25 13:31:47 2015 +0100
+++ b/src/Pure/Tools/build.scala	Wed Mar 25 13:45:52 2015 +0100
@@ -242,8 +242,8 @@
               { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
             rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
 
-      position(command(SESSION)) ~!
-        (session_name ~
+      command(SESSION) ~!
+        (position(session_name) ~
           (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
           (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
           ($$$("=") ~!
@@ -253,7 +253,7 @@
               rep1(theories) ~
               (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
               (rep(document_files) ^^ (x => x.flatten))))) ^^
-        { case (_, pos) ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
+        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
     }