changeset 48599 | 5e64b7770f35 |
parent 47459 | 373e456149cc |
child 48718 | 73e6c22e2d94 |
--- a/src/Pure/PIDE/command.scala Mon Jul 30 12:08:25 2012 +0200 +++ b/src/Pure/PIDE/command.scala Mon Jul 30 13:42:45 2012 +0200 @@ -128,7 +128,7 @@ def is_defined: Boolean = id != Document.no_id - val is_ignored: Boolean = span.forall(_.is_ignored) + val is_ignored: Boolean = !span.exists(_.is_proper) val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed)) def is_command: Boolean = !is_ignored && !is_malformed