src/Pure/Isar/token.scala
changeset 59715 4f0d0e4ad68d
parent 59706 bf6ca55aae13
child 59735 24bee1b11fce
--- a/src/Pure/Isar/token.scala	Mon Mar 16 11:30:54 2015 +0100
+++ b/src/Pure/Isar/token.scala	Mon Mar 16 13:32:31 2015 +0100
@@ -161,6 +161,7 @@
     val start: Pos = new Pos(1, 1, "", "")
     def file(file: String): Pos = new Pos(1, 1, file, "")
     def id(id: String): Pos = new Pos(0, 1, "", id)
+    val command: Pos = id(Markup.COMMAND)
   }
 
   final class Pos private[Token](