src/Pure/PIDE/command.scala
changeset 43662 e3175ec00311
parent 43520 cec9b95fa35d
child 43714 3749d1e6dde9
--- a/src/Pure/PIDE/command.scala	Mon Jul 04 22:11:32 2011 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Jul 04 22:25:33 2011 +0200
@@ -80,10 +80,10 @@
   /* dummy commands */
 
   def unparsed(source: String): Command =
-    new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
+    new Command(Document.no_id, List(Token(Token.Kind.UNPARSED, source)))
 
   def span(toks: List[Token]): Command =
-    new Command(Document.NO_ID, toks)
+    new Command(Document.no_id, toks)
 }
 
 
@@ -97,7 +97,7 @@
   def is_ignored: Boolean = span.forall(_.is_ignored)
   def is_malformed: Boolean = !is_command && !is_ignored
 
-  def is_unparsed = id == Document.NO_ID
+  def is_unparsed = id == Document.no_id
 
   def name: String = if (is_command) span.head.content else ""
   override def toString =