src/Pure/PIDE/command.scala
changeset 38367 f7d2574dc3a6
parent 38363 af7f41a8a0a8
child 38370 8b15d0f98962
--- 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")