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](