# HG changeset patch
# User wenzelm
# Date 1284753044 -7200
# Node ID 31290f54be1961dccc8b633159f46323ae5e728c
# Parent  5f318522e6fe0131b55617cfd2f5bd3e15c8e498
Isabelle_Markup.overview_color: indicate error / warning messages;

diff -r 5f318522e6fe -r 31290f54be19 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 17 21:49:34 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 17 21:50:44 2010 +0200
@@ -54,10 +54,13 @@
     if (snapshot.is_outdated) None
     else
       Isar_Document.command_status(state.status) match {
-        case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
+        case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
         case Isar_Document.Unprocessed => Some(unfinished_color)
         case Isar_Document.Failed => Some(error_color)
-        case _ => None
+        case Isar_Document.Finished =>
+          if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
+          else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
+          else None
       }
   }