src/Pure/Isar/parse.scala

--- a/src/Pure/Isar/parse.scala	Tue Mar 10 13:55:10 2015 +0100
+++ b/src/Pure/Isar/parse.scala	Tue Mar 10 20:12:30 2015 +0100
@@ -49,7 +49,7 @@
 
     def command(name: String): Parser[Position.T] =
       token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^
-        { case (_, pos) => pos.position }
+        { case (tok, pos) => pos.position(tok) }
 
     def $$$(name: String): Parser[String] =
       atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)