--- a/src/Pure/PIDE/command.scala Thu Aug 12 17:37:58 2010 +0200
+++ b/src/Pure/PIDE/command.scala Thu Aug 12 17:55:23 2010 +0200
@@ -141,6 +141,12 @@
case _ => add_result(message)
}
}
+
+
+ /* unparsed dummy commands */
+
+ def unparsed(source: String) =
+ new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
}
@@ -156,6 +162,8 @@
def is_ignored: Boolean = span.forall(_.is_ignored)
def is_malformed: Boolean = !is_command && !is_ignored
+ def is_unparsed = id == Document.NO_ID
+
def name: String = if (is_command) span.head.content else ""
override def toString =
id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")