src/Pure/Isar/token.scala
changeset 43611 21a57a0c5f25
parent 43430 1ed88ddf1268
child 46943 ac1c41ea856d
--- a/src/Pure/Isar/token.scala	Thu Jun 30 16:50:26 2011 +0200
+++ b/src/Pure/Isar/token.scala	Thu Jun 30 19:24:09 2011 +0200
@@ -81,6 +81,9 @@
   def is_comment: Boolean = kind == Token.Kind.COMMENT
   def is_ignored: Boolean = is_space || is_comment
 
+  def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
+  def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"
+
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)
     else if (kind == Token.Kind.ALT_STRING) Scan.Lexicon.empty.quoted_content("`", source)