clarified position;
authorwenzelm
Wed Mar 25 13:45:52 2015 +0100 (2015-03-25)
changeset 598116b0d9e8ac227
parent 59810 e749a0f2f401
child 59812 675d0c692c41
clarified position;
src/Pure/System/options.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/System/options.scala	Wed Mar 25 13:31:47 2015 +0100
     1.2 +++ b/src/Pure/System/options.scala	Wed Mar 25 13:45:52 2015 +0100
     1.3 @@ -93,9 +93,9 @@
     1.4      {
     1.5        command(SECTION) ~! text ^^
     1.6          { case _ ~ a => (options: Options) => options.set_section(a) } |
     1.7 -      opt(command(PUBLIC)) ~ position(command(OPTION)) ~! (option_name ~ $$$(":") ~ option_type ~
     1.8 +      opt(command(PUBLIC)) ~ command(OPTION) ~! (position(option_name) ~ $$$(":") ~ option_type ~
     1.9        $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
    1.10 -        { case a ~ ((_, pos)) ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
    1.11 +        { case a ~ _ ~ ((b, pos) ~ _ ~ c ~ _ ~ d ~ e) =>
    1.12              (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
    1.13      }
    1.14  
     2.1 --- a/src/Pure/Tools/build.scala	Wed Mar 25 13:31:47 2015 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 25 13:45:52 2015 +0100
     2.3 @@ -242,8 +242,8 @@
     2.4                { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
     2.5              rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
     2.6  
     2.7 -      position(command(SESSION)) ~!
     2.8 -        (session_name ~
     2.9 +      command(SESSION) ~!
    2.10 +        (position(session_name) ~
    2.11            (($$$("(") ~! (rep1(name) <~ $$$(")")) ^^ { case _ ~ x => x }) | success(Nil)) ~
    2.12            (($$$(IN) ~! path ^^ { case _ ~ x => x }) | success(".")) ~
    2.13            ($$$("=") ~!
    2.14 @@ -253,7 +253,7 @@
    2.15                rep1(theories) ~
    2.16                (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
    2.17                (rep(document_files) ^^ (x => x.flatten))))) ^^
    2.18 -        { case (_, pos) ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    2.19 +        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
    2.20              Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
    2.21      }
    2.22