some color scheme for theory status;
authorwenzelm
Sat Sep 10 20:22:22 2011 +0200 (2011-09-10)
changeset 448660eb8284a64bd
parent 44865 679f0d57e831
child 44867 79d3d74e7cbb
some color scheme for theory status;
src/Pure/PIDE/isar_document.scala
src/Tools/jEdit/src/isabelle_markup.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Sat Sep 10 16:30:08 2011 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Sat Sep 10 20:22:22 2011 +0200
     1.3 @@ -63,6 +63,9 @@
     1.4    }
     1.5  
     1.6    sealed case class Node_Status(unprocessed: Int, running: Int, finished: Int, failed: Int)
     1.7 +  {
     1.8 +    def total: Int = unprocessed + running + finished + failed
     1.9 +  }
    1.10  
    1.11    def node_status(
    1.12      state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
     2.1 --- a/src/Tools/jEdit/src/isabelle_markup.scala	Sat Sep 10 16:30:08 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/isabelle_markup.scala	Sat Sep 10 20:22:22 2011 +0200
     2.3 @@ -26,13 +26,14 @@
     2.4    val outdated_color = new Color(238, 227, 227)
     2.5    val running_color = new Color(97, 0, 97)
     2.6    val running1_color = new Color(97, 0, 97, 100)
     2.7 -  val unfinished_color = new Color(255, 160, 160)
     2.8 -  val unfinished1_color = new Color(255, 160, 160, 50)
     2.9 +  val unprocessed_color = new Color(255, 160, 160)
    2.10 +  val unprocessed1_color = new Color(255, 160, 160, 50)
    2.11  
    2.12    val light_color = new Color(240, 240, 240)
    2.13    val regular_color = new Color(192, 192, 192)
    2.14    val warning_color = new Color(255, 140, 0)
    2.15    val error_color = new Color(178, 34, 34)
    2.16 +  val error1_color = new Color(178, 34, 34, 50)
    2.17    val bad_color = new Color(255, 106, 106, 100)
    2.18    val hilite_color = new Color(255, 204, 102, 100)
    2.19  
    2.20 @@ -60,7 +61,7 @@
    2.21      else
    2.22        Isar_Document.command_status(state.status) match {
    2.23          case Isar_Document.Forked(i) if i > 0 => Some(running1_color)
    2.24 -        case Isar_Document.Unprocessed => Some(unfinished1_color)
    2.25 +        case Isar_Document.Unprocessed => Some(unprocessed1_color)
    2.26          case _ => None
    2.27        }
    2.28    }
    2.29 @@ -72,7 +73,7 @@
    2.30      else
    2.31        Isar_Document.command_status(state.status) match {
    2.32          case Isar_Document.Forked(i) => if (i > 0) Some(running_color) else None
    2.33 -        case Isar_Document.Unprocessed => Some(unfinished_color)
    2.34 +        case Isar_Document.Unprocessed => Some(unprocessed_color)
    2.35          case Isar_Document.Failed => Some(error_color)
    2.36          case Isar_Document.Finished =>
    2.37            if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 16:30:08 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 20:22:22 2011 +0200
     3.3 @@ -15,8 +15,8 @@
     3.4  import scala.swing.event.{ButtonClicked, SelectionChanged}
     3.5  
     3.6  import java.lang.System
     3.7 -import java.awt.BorderLayout
     3.8 -import javax.swing.JList
     3.9 +import java.awt.{BorderLayout, Graphics}
    3.10 +import javax.swing.{JList, DefaultListCellRenderer}
    3.11  import javax.swing.border.{BevelBorder, SoftBevelBorder}
    3.12  
    3.13  import org.gjt.sp.jedit.{View, jEdit}
    3.14 @@ -84,7 +84,35 @@
    3.15  
    3.16    /* component state -- owned by Swing thread */
    3.17  
    3.18 -  private var nodes_status: Map[Document.Node.Name, String] = Map.empty
    3.19 +  private var nodes_status: Map[Document.Node.Name, Isar_Document.Node_Status] = Map.empty
    3.20 +
    3.21 +  val node_renderer = new DefaultListCellRenderer
    3.22 +  {
    3.23 +    override def paintComponent(gfx: Graphics)
    3.24 +    {
    3.25 +      super.paintComponent(gfx)
    3.26 +      nodes_status.get(Document.Node.Name(getText, "", "")) match {
    3.27 +        case Some(st) if st.total > 0 =>
    3.28 +          val w = getWidth
    3.29 +          val h = getHeight
    3.30 +          var end = w
    3.31 +          for {
    3.32 +            (n, color) <- List(
    3.33 +              (st.unprocessed, Isabelle_Markup.unprocessed1_color),
    3.34 +              (st.running, Isabelle_Markup.running1_color),
    3.35 +              (st.failed, Isabelle_Markup.error1_color)) }
    3.36 +          {
    3.37 +            gfx.setColor(color)
    3.38 +            val v = (n * w / st.total) max (if (n > 0) 2 else 0)
    3.39 +            gfx.fillRect(end - v, 0, v, h)
    3.40 +            end -= v
    3.41 +          }
    3.42 +        case _ =>
    3.43 +      }
    3.44 +    }
    3.45 +  }
    3.46 +
    3.47 +  status.peer.setCellRenderer(node_renderer)
    3.48  
    3.49    private def handle_changed(changed_nodes: Set[Document.Node.Name])
    3.50    {
    3.51 @@ -98,14 +126,13 @@
    3.52          name <- changed_nodes
    3.53          node <- version.nodes.get(name)
    3.54          val status = Isar_Document.node_status(state, version, node)
    3.55 -      } nodes_status1 += (name -> status.toString)
    3.56 +      } nodes_status1 += (name -> status)
    3.57  
    3.58        if (nodes_status != nodes_status1) {
    3.59          nodes_status = nodes_status1
    3.60 -        val order =
    3.61 -          Library.sort_wrt((name: Document.Node.Name) => name.theory,
    3.62 -            nodes_status.keySet.toList)
    3.63 -        status.listData = order.map(name => name.theory + " " + nodes_status(name))
    3.64 +        status.listData =
    3.65 +          Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
    3.66 +            .map(_.node)
    3.67        }
    3.68      }
    3.69    }