some color scheme for theory status;

--- a/src/Pure/PIDE/isar_document.scala	Sat Sep 10 16:30:08 2011 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Sat Sep 10 20:22:22 2011 +0200
@@ -63,6 +63,9 @@
   }
 
   sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
+  {
+    def total: Int = unprocessed + running + finished + failed
+  }
 
   def node_status(
     state: Document.State, version: Document.Version, node: Document.Node): Node_Status =

--- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Sep 10 16:30:08 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Sep 10 20:22:22 2011 +0200
@@ -26,13 +26,14 @@
   val outdated_color = new Color(238, 227, 227)
   val running_color = new Color(97, 0, 97)
   val running1_color = new Color(97, 0, 97, 100)
-  val unfinished_color = new Color(255, 160, 160)
-  val unfinished1_color = new Color(255, 160, 160, 50)
+  val unprocessed_color = new Color(255, 160, 160)
+  val unprocessed1_color = new Color(255, 160, 160, 50)
 
   val light_color = new Color(240, 240, 240)
   val regular_color = new Color(192, 192, 192)
   val warning_color = new Color(255, 140, 0)
   val error_color = new Color(178, 34, 34)
+  val error1_color = new Color(178, 34, 34, 50)
   val bad_color = new Color(255, 106, 106, 100)
   val hilite_color = new Color(255, 204, 102, 100)
 
@@ -60,7 +61,7 @@
     else
       Isar_Document.command_status(state.status) match {
         case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
-        case Isar_Document.Unprocessed => Some(unfinished1_color)
+        case Isar_Document.Unprocessed => Some(unprocessed1_color)
         case _ => None
       }
   }
@@ -72,7 +73,7 @@
     else
       Isar_Document.command_status(state.status) match {
         case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
-        case Isar_Document.Unprocessed => Some(unfinished_color)
+        case Isar_Document.Unprocessed => Some(unprocessed_color)
         case Isar_Document.Failed => Some(error_color)
         case Isar_Document.Finished =>
           if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)

--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 16:30:08 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 20:22:22 2011 +0200
@@ -15,8 +15,8 @@
 import scala.swing.event.{ButtonClicked, SelectionChanged}
 
 import java.lang.System
-import java.awt.BorderLayout
-import javax.swing.JList
+import java.awt.{BorderLayout, Graphics}
+import javax.swing.{JList, DefaultListCellRenderer}
 import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
 import org.gjt.sp.jedit.{View, jEdit}
@@ -84,7 +84,35 @@
 
   /* component state -- owned by Swing thread */
 
-  private var nodes_status: Map[Document.Node.Name, String] = Map.empty
+  private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
+
+  val node_renderer = new DefaultListCellRenderer
+  {
+    override def paintComponent(gfx: Graphics)
+    {
+      super.paintComponent(gfx)
+      nodes_status.get(Document.Node.Name(getText, "", "")) match {
+        case Some(st) if st.total > 0 =>
+          val w = getWidth
+          val h = getHeight
+          var end = w
+          for {
+            (n, color) <- List(
+              (st.unprocessed, Isabelle_Markup.unprocessed1_color),
+              (st.running, Isabelle_Markup.running1_color),
+              (st.failed, Isabelle_Markup.error1_color)) }
+          {
+            gfx.setColor(color)
+            val v = (n * w / st.total) max (if (n > 0) 2 else 0)
+            gfx.fillRect(end - v, 0, v, h)
+            end -= v
+          }
+        case _ =>
+      }
+    }
+  }
+
+  status.peer.setCellRenderer(node_renderer)
 
   private def handle_changed(changed_nodes: Set[Document.Node.Name])
   {
@@ -98,14 +126,13 @@
         name <- changed_nodes
         node <- version.nodes.get(name)
         val status = Isar_Document.node_status(state, version, node)
-      } nodes_status1 += (name -> status.toString)
+      } nodes_status1 += (name -> status)
 
       if (nodes_status != nodes_status1) {
         nodes_status = nodes_status1
-        val order =
-          Library.sort_wrt((name: Document.Node.Name) => name.theory,
-            nodes_status.keySet.toList)
-        status.listData = order.map(name => name.theory + " " + nodes_status(name))
+        status.listData =
+          Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
+            .map(_.node)
       }
     }
   }