src/Tools/jEdit/src/session_dockable.scala

--- 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)
       }
     }
   }