src/Pure/PIDE/command.scala
changeset 38367 f7d2574dc3a6
parent 38363 af7f41a8a0a8
child 38370 8b15d0f98962
     1.1 --- a/src/Pure/PIDE/command.scala	Thu Aug 12 17:37:58 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Thu Aug 12 17:55:23 2010 +0200
     1.3 @@ -141,6 +141,12 @@
     1.4          case _ => add_result(message)
     1.5        }
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* unparsed dummy commands */
    1.10 +
    1.11 +  def unparsed(source: String) =
    1.12 +    new Command(Document.NO_ID, List(Token(Token.Kind.UNPARSED, source)))
    1.13  }
    1.14  
    1.15  
    1.16 @@ -156,6 +162,8 @@
    1.17    def is_ignored: Boolean = span.forall(_.is_ignored)
    1.18    def is_malformed: Boolean = !is_command && !is_ignored
    1.19  
    1.20 +  def is_unparsed = id == Document.NO_ID
    1.21 +
    1.22    def name: String = if (is_command) span.head.content else ""
    1.23    override def toString =
    1.24      id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")