# HG changeset patch
# User wenzelm
# Date 1332182994 -3600
# Node ID 63e23fc6259bec875a27b895bf7514c5d66bfd04
# Parent  7bdac8e81f6d532f0bb7437ac82ae1704759e111# Parent  e203b7d7e08dee640b13453c129457aa15a2492e
merged

diff -r 7bdac8e81f6d -r 63e23fc6259b src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Mar 19 15:20:00 2012 +0000
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Mar 19 19:49:54 2012 +0100
@@ -130,7 +130,7 @@
     val _ =
       (case try (Thy_Header.the_keyword thy) name of
         SOME spec =>
-          if Option.map Keyword.spec spec = SOME kind then ()
+          if Option.map #1 spec = SOME (Keyword.kind_of kind) then ()
           else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
       | NONE =>
           if Context.theory_name thy = Context.PureN
diff -r 7bdac8e81f6d -r 63e23fc6259b src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Mar 19 15:20:00 2012 +0000
+++ b/src/Pure/Isar/token.scala	Mon Mar 19 19:49:54 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"
diff -r 7bdac8e81f6d -r 63e23fc6259b src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Mon Mar 19 15:20:00 2012 +0000
+++ b/src/Pure/PIDE/command.scala	Mon Mar 19 19:49:54 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")
 
diff -r 7bdac8e81f6d -r 63e23fc6259b src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Mar 19 15:20:00 2012 +0000
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Mar 19 19:49:54 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)
diff -r 7bdac8e81f6d -r 63e23fc6259b src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Mar 19 15:20:00 2012 +0000
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Mar 19 19:49:54 2012 +0100
@@ -154,8 +154,8 @@
   {
     Swing_Thread.require()
     val snapshot = model.snapshot()
-    was_updated = was_outdated && !snapshot.is_outdated
-    was_outdated = was_outdated || snapshot.is_outdated
+    was_updated &&= !snapshot.is_outdated
+    was_outdated ||= snapshot.is_outdated
     snapshot
   }