1.1 --- a/src/Tools/jEdit/src/proofdocument/command.scala	Mon Jan 11 18:26:13 2010 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/command.scala	Mon Jan 11 18:26:38 2010 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    /* classification */
     1.5  
     1.6    def is_command: Boolean = !span.isEmpty && span.first.is_command
     1.7 -  def is_ignored: Boolean = span.forall(tok => tok.is_space || tok.is_comment)
     1.8 +  def is_ignored: Boolean = span.forall(_.is_ignored)
     1.9    def is_malformed: Boolean = !is_command && !is_ignored
    1.10  
    1.11    def name: String = if (is_command) span.first.content else ""