treat all messages except status as results;
report ignored status reports;
invoke command.changed only for actual change;
tuned;

--- a/src/Tools/jEdit/src/prover/State.scala	Sun Sep 06 15:31:25 2009 +0200
+++ b/src/Tools/jEdit/src/prover/State.scala	Sun Sep 06 15:43:02 2009 +0200
@@ -2,6 +2,7 @@
  * Accumulating results from prover
  *
  * @author Fabian Immler, TU Munich
+ * @author Makarius
  */
 
 package isabelle.prover
@@ -64,63 +65,50 @@
     refs.find(t => t.start <= pos && pos < t.stop)
 
 
-
   /* message dispatch */
 
   def + (message: XML.Tree): State =
   {
     val changed: State =
       message match {
-        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WRITELN) :: _, _)
-          | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.PRIORITY) :: _, _)
-          | XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.WARNING) :: _, _) =>
-          add_result(message)
-        case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.ERROR) :: _, _) =>
-          set_status(Command.Status.FAILED).add_result(message)
         case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
-          (this /: elems) ((st, e) =>
-            e match {
-              // command status
-              case XML.Elem(Markup.UNPROCESSED, _, _) =>
-                st.set_status(Command.Status.UNPROCESSED)
-              case XML.Elem(Markup.FINISHED, _, _) =>
-                st.set_status(Command.Status.FINISHED)
-              case XML.Elem(Markup.FAILED, _, _) =>
-                st.set_status(Command.Status.FAILED)
-              case XML.Elem(kind, attr, body) =>
-                val (begin, end) = Position.offsets_of(attr)
-                if (begin.isDefined && end.isDefined) {
-                  if (kind == Markup.ML_TYPING) {
-                    val info = body.first.asInstanceOf[XML.Text].content
-                    st.add_markup(
-                      command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
-                  }
-                  else if (kind == Markup.ML_REF) {
-                    body match {
-                      case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
-                        st.add_markup(command.markup_node(
-                          begin.get - 1, end.get - 1,
-                          Command.RefInfo(
-                            Position.file_of(attr),
-                            Position.line_of(attr),
-                            Position.id_of(attr),
-                            Position.offset_of(attr))))
-                      case _ => st
-                    }
-                  }
-                  else {
-                    st.add_markup(
-                      command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
+          (this /: elems)((state, elem) =>
+            elem match {
+              case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
+              case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
+              case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
+              case XML.Elem(kind, atts, body) =>
+                val (begin, end) = Position.offsets_of(atts)
+                if (begin.isEmpty || end.isEmpty) state
+                else if (kind == Markup.ML_TYPING) {
+                  val info = body.first.asInstanceOf[XML.Text].content   // FIXME proper match!?
+                  state.add_markup(
+                    command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
+                }
+                else if (kind == Markup.ML_REF) {
+                  body match {
+                    case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+                      state.add_markup(command.markup_node(
+                        begin.get - 1, end.get - 1,
+                        Command.RefInfo(
+                          Position.file_of(atts),
+                          Position.line_of(atts),
+                          Position.id_of(atts),
+                          Position.offset_of(atts))))
+                    case _ => state
                   }
                 }
-                else st
-              case _ => st
+                else {
+                  state.add_markup(
+                    command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
+                }
+              case _ =>
+                System.err.println("ignored status report: " + elem)
+                state
             })
-        case _ =>
-          System.err.println("ignored: " + message)
-          this
+        case _ => add_result(message)
       }
-    command.changed()
+    if (!(this eq changed)) command.changed()
     changed
   }
 }