clarified command span classification: strict Command.is_command, permissive Command.name;

--- a/src/Pure/Isar/token.scala	Sun Mar 18 22:09:00 2012 +0100
+++ b/src/Pure/Isar/token.scala	Mon Mar 19 14:59:31 2012 +0100
@@ -81,6 +81,7 @@
   def is_space: Boolean = kind == Token.Kind.SPACE
   def is_comment: Boolean = kind == Token.Kind.COMMENT
   def is_ignored: Boolean = is_space || is_comment
+  def is_unparsed: Boolean = kind == Token.Kind.UNPARSED
 
   def is_begin: Boolean = kind == Token.Kind.KEYWORD && source == "begin"
   def is_end: Boolean = kind == Token.Kind.COMMAND && source == "end"

--- a/src/Pure/PIDE/command.scala	Sun Mar 18 22:09:00 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Mon Mar 19 14:59:31 2012 +0100
@@ -92,9 +92,6 @@
     new Command(id, node_name, span.toList, source)
   }
 
-  def apply(node_name: Document.Node.Name, toks: List[Token]): Command =
-    Command(Document.no_id, node_name, toks)
-
   def unparsed(source: String): Command =
     Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
 
@@ -131,11 +128,13 @@
 
   def is_defined: Boolean = id != Document.no_id
 
-  def is_command: Boolean = !span.isEmpty && span.head.is_command
-  def is_ignored: Boolean = span.forall(_.is_ignored)
-  def is_malformed: Boolean = !is_command && !is_ignored
+  val is_ignored: Boolean = span.forall(_.is_ignored)
+  val is_malformed: Boolean = !is_ignored && (!span.head.is_command || span.exists(_.is_unparsed))
+  def is_command: Boolean = !is_ignored && !is_malformed
 
-  def name: String = if (is_command) span.head.content else ""
+  def name: String =
+    span.find(_.is_command) match { case Some(tok) => tok.content case _ => "" }
+
   override def toString =
     id + "/" + (if (is_command) name else if (is_ignored) "IGNORED" else "MALFORMED")
 

--- a/src/Pure/Thy/thy_syntax.scala	Sun Mar 18 22:09:00 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Mar 19 14:59:31 2012 +0100
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(node_name, span)))
+      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
       result()
     }
   }
@@ -224,12 +224,12 @@
     commands: Linear_Set[Command]): Linear_Set[Command] =
   {
     commands.iterator.find(cmd => !cmd.is_defined) match {
-      case Some(first_unparsed) =>
+      case Some(first_undefined) =>
         val first =
-          commands.reverse_iterator(first_unparsed).
+          commands.reverse_iterator(first_undefined).
             dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
         val last =
-          commands.iterator(first_unparsed).
+          commands.iterator(first_undefined).
             dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
         val range =
           commands.iterator(first).takeWhile(_ != last).toList ::: List(last)