# HG changeset patch
# User wenzelm
# Date 1358201320 -3600
# Node ID 3a1edaa0dc6d9e371a2af4224ee6944a21982097
# Parent  a9c1b1428e873ebe5f207e7fa22366b32d2b6ec7
more prominent status ticks;
is_running takes priority -- important to spot unstable parts that are re-run after edits;

diff -r a9c1b1428e87 -r 3a1edaa0dc6d src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Jan 14 22:33:53 2013 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Jan 14 23:08:40 2013 +0100
@@ -180,10 +180,10 @@
           ((Protocol.Status.init, 0) /: results) {
             case ((s1, p1), Text.Info(_, (s2, p2))) => (s1 + s2, p1 max p2) }
 
-        if (pri == Rendering.warning_pri) Some(warning_color)
+        if (status.is_running) Some(running_color)
+        else if (pri == Rendering.warning_pri) Some(warning_color)
         else if (pri == Rendering.error_pri) Some(error_color)
         else if (status.is_unprocessed) Some(unprocessed_color)
-        else if (status.is_running) Some(running_color)
         else if (status.is_failed) Some(error_color)
         else None
       }
diff -r a9c1b1428e87 -r 3a1edaa0dc6d src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Mon Jan 14 22:33:53 2013 +0100
+++ b/src/Tools/jEdit/src/text_overview.scala	Mon Jan 14 23:08:40 2013 +0100
@@ -22,7 +22,7 @@
   private val buffer = doc_view.model.buffer
 
   private val WIDTH = 10
-  private val HEIGHT = 2
+  private val HEIGHT = 4
 
   private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines
 
diff -r a9c1b1428e87 -r 3a1edaa0dc6d src/Tools/jEdit/src/theories_dockable.scala
--- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Jan 14 22:33:53 2013 +0100
+++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Jan 14 23:08:40 2013 +0100
@@ -99,7 +99,7 @@
               (st.failed, PIDE.options.color_value("error_color"))) }
           {
             gfx.setColor(color)
-            val v = (n * w / st.total) max (if (n > 0) 2 else 0)
+            val v = (n * w / st.total) max (if (n > 0) 4 else 0)
             gfx.fillRect(end - v, insets.top, v, h)
             end -= v
           }