position parser as in ML;

--- a/src/Pure/Isar/parse.scala	Fri Mar 13 21:35:48 2015 +0100
+++ b/src/Pure/Isar/parse.scala	Sat Mar 14 16:56:11 2015 +0100
@@ -25,31 +25,42 @@
       if (!filter_proper || in.atEnd || in.first.is_proper) in
       else proper(in.rest)
 
-    def token(s: String, pred: Elem => Boolean): Parser[(Elem, Token.Pos)] =
-      new Parser[(Elem, Token.Pos)] {
+    private def proper_position: Parser[Position.T] =
+      new Parser[Position.T] {
+        def apply(raw_input: Input) =
+        {
+          val in = proper(raw_input)
+          val pos =
+            in.pos match {
+              case pos: Token.Pos => pos
+              case _ => Token.Pos.none
+            }
+          Success(if (in.atEnd) pos.position() else pos.position(in.first), in)
+        }
+      }
+
+    def position[A](parser: Parser[A]): Parser[(A, Position.T)] =
+      proper_position ~ parser ^^ { case x ~ y => (y, x) }
+
+    def token(s: String, pred: Elem => Boolean): Parser[Elem] =
+      new Parser[Elem] {
         def apply(raw_input: Input) =
         {
           val in = proper(raw_input)
           if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in)
           else {
-            val pos =
-              in.pos match {
-                case pos: Token.Pos => pos
-                case _ => Token.Pos.none
-              }
             val token = in.first
-            if (pred(token)) Success((token, pos), proper(in.rest))
+            if (pred(token)) Success(token, proper(in.rest))
             else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)
           }
         }
       }
 
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
-      token(s, pred) ^^ { case (tok, _) => tok.content }
+      token(s, pred) ^^ (_.content)
 
-    def command(name: String): Parser[Position.T] =
-      token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
-        { case (tok, pos) => pos.position(tok) }
+    def command(name: String): Parser[String] =
+      atom("command " + quote(name), tok => tok.is_command && tok.source == name)
 
     def $$$(name: String): Parser[String] =
       atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)

--- a/src/Pure/System/options.scala	Fri Mar 13 21:35:48 2015 +0100
+++ b/src/Pure/System/options.scala	Sat Mar 14 16:56:11 2015 +0100
@@ -93,9 +93,9 @@
     {
       command(SECTION) ~! text ^^
         { case _ ~ a => (options: Options) => options.set_section(a) } |
-      opt(command(PUBLIC)) ~ command(OPTION) ~! (option_name ~ $$$(":") ~ option_type ~
+      opt(command(PUBLIC)) ~ position(command(OPTION)) ~! (option_name ~ $$$(":") ~ option_type ~
       $$$("=") ~ option_value ~ ($$$("--") ~! text ^^ { case _ ~ x => x } | success(""))) ^^
-        { case a ~ pos ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
+        { case a ~ ((_, pos)) ~ (b ~ _ ~ c ~ _ ~ d ~ e) =>
             (options: Options) => options.declare(a.isDefined, pos, b, c, d, e) }
     }
 

--- a/src/Pure/Tools/build.scala	Fri Mar 13 21:35:48 2015 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 14 16:56:11 2015 +0100
@@ -242,7 +242,7 @@
               { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~
             rep1(path)) ^^ { case _ ~ (x ~ y) => y.map((x, _)) }
 
-      command(SESSION) ~!
+      position(command(SESSION)) ~!
         (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 (_, pos) ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
             Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
     }