# HG changeset patch
# User wenzelm
# Date 1262702672 -3600
# Node ID dc932fc1b9063676b39ded67a1619aef7035b5f0
# Parent  b5025782a4edc006112456cc29a1b57b09c81db7
more token discriminators;

diff -r b5025782a4ed -r dc932fc1b906 src/Pure/Isar/outer_lex.scala
--- a/src/Pure/Isar/outer_lex.scala	Tue Jan 05 15:44:06 2010 +0100
+++ b/src/Pure/Isar/outer_lex.scala	Tue Jan 05 15:44:32 2010 +0100
@@ -33,6 +33,7 @@
 
   sealed case class Token(val kind: Token_Kind.Value, val source: String)
   {
+    def is_command: Boolean = kind == Token_Kind.COMMAND
     def is_delimited: Boolean =
       kind == Token_Kind.STRING ||
       kind == Token_Kind.ALT_STRING ||
@@ -48,6 +49,7 @@
     def is_space: Boolean = kind == Token_Kind.SPACE
     def is_comment: Boolean = kind == Token_Kind.COMMENT
     def is_proper: Boolean = !(is_space || is_comment)
+    def is_unparsed: Boolean = kind == Token_Kind.UNPARSED
 
     def content: String =
       if (kind == Token_Kind.STRING) Scan.Lexicon.empty.quoted_content("\"", source)