src/Pure/PIDE/command.scala
changeset 47012 0e246130486b
parent 46910 3e068ef04b42
child 47459 373e456149cc
     1.1 --- a/src/Pure/PIDE/command.scala	Sun Mar 18 22:09:00 2012 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Mon Mar 19 14:59:31 2012 +0100
     1.3 @@ -92,9 +92,6 @@
     1.4      new Command(id, node_name, span.toList, source)
     1.5    }
     1.6  
     1.7 -  def apply(node_name: Document.Node.Name, toks: List[Token]): Command =
     1.8 -    Command(Document.no_id, node_name, toks)
     1.9 -
    1.10    def unparsed(source: String): Command =
    1.11      Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
    1.12  
    1.13 @@ -131,11 +128,13 @@
    1.14  
    1.15    def is_defined: Boolean = id != Document.no_id
    1.16  
    1.17 -  def is_command: Boolean = !span.isEmpty && span.head.is_command
    1.18 -  def is_ignored: Boolean = span.forall(_.is_ignored)
    1.19 -  def is_malformed: Boolean = !is_command && !is_ignored
    1.20 +  val is_ignored: Boolean = span.forall(_.is_ignored)
    1.21 +  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed))
    1.22 +  def is_command: Boolean = !is_ignored && !is_malformed
    1.23  
    1.24 -  def name: String = if (is_command) span.head.content else ""
    1.25 +  def name: String =
    1.26 +    span.find(_.is_command) match { case Some(tok) => tok.content case _ => "" }
    1.27 +
    1.28    override def toString =
    1.29      id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
    1.30