# HG changeset patch
# User wenzelm
# Date 1346416504 -7200
# Node ID d7a1973b063cabee6d3f6f8bc9e6bcba16d910fd
# Parent  4680c4046814d6a9420134d15e71b6ffcc1b178f
more markup for failed goal forks, reusing "bad";

diff -r 4680c4046814 -r d7a1973b063c src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Aug 31 13:23:25 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Aug 31 14:35:04 2012 +0200
@@ -48,6 +48,11 @@
                 val props = Position.purge(atts)
                 val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
+              case XML.Elem(Markup(name, atts), args) =>
+                val range = command.proper_range
+                val props = Position.purge(atts)
+                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
+                state.add_markup(info)
               case _ =>
                 // FIXME System.err.println("Ignored report message: " + msg)
                 state
diff -r 4680c4046814 -r d7a1973b063c src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Aug 31 13:23:25 2012 +0200
+++ b/src/Pure/goal.ML	Fri Aug 31 14:35:04 2012 +0200
@@ -136,10 +136,12 @@
               val task = the (Future.worker_task ());
               val _ = status task [Isabelle_Markup.running];
               val result = Exn.capture (Future.interruptible_task e) ();
+              val _ = status task [Isabelle_Markup.finished, Isabelle_Markup.joined];
               val _ =
-                status task
-                  ([Isabelle_Markup.finished, Isabelle_Markup.joined] @
-                    (if is_some (Exn.get_res result) then [] else [Isabelle_Markup.failed]));
+                if is_some (Exn.get_res result) then ()
+                else
+                  (status task [Isabelle_Markup.failed];
+                   Output.report (Markup.markup_only Isabelle_Markup.bad));
             in Exn.release result end);
       val _ = status (Future.task_of future) [Isabelle_Markup.forked];
     in future end) ();
diff -r 4680c4046814 -r d7a1973b063c src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 31 13:23:25 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Aug 31 14:35:04 2012 +0200
@@ -292,10 +292,10 @@
             })
         color <-
           (result match {
-            case (Some(status), _) =>
+            case (Some(status), opt_color) =>
               if (status.is_unprocessed) Some(unprocessed1_color)
               else if (status.is_running) Some(running1_color)
-              else None
+              else opt_color
             case (_, opt_color) => opt_color
           })
       } yield Text.Info(r, color)