renamed dockable "Prover Session" to "Theories";
authorwenzelm
Fri Nov 30 21:30:24 2012 +0100 (2012-11-30)
changeset 50299f70b3712040f
parent 50298 1426d478ccda
child 50300 6658097758ba
renamed dockable "Prover Session" to "Theories";
more uniform Library.lowercase/uppercase;
src/Pure/System/options.scala
src/Pure/System/standard_system.scala
src/Pure/library.scala
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/dockables.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/session_dockable.scala
src/Tools/jEdit/src/symbols_dockable.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Pure/System/options.scala	Fri Nov 30 21:28:35 2012 +0100
     1.2 +++ b/src/Pure/System/options.scala	Fri Nov 30 21:30:24 2012 +0100
     1.3 @@ -7,7 +7,6 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.util.Locale
     1.8  import java.util.Calendar
     1.9  
    1.10  
    1.11 @@ -22,7 +21,7 @@
    1.12  
    1.13    sealed abstract class Type
    1.14    {
    1.15 -    def print: String = toString.toLowerCase(Locale.ENGLISH)
    1.16 +    def print: String = Library.lowercase(toString)
    1.17    }
    1.18    case object Bool extends Type
    1.19    case object Int extends Type
     2.1 --- a/src/Pure/System/standard_system.scala	Fri Nov 30 21:28:35 2012 +0100
     2.2 +++ b/src/Pure/System/standard_system.scala	Fri Nov 30 21:30:24 2012 +0100
     2.3 @@ -9,7 +9,6 @@
     2.4  
     2.5  import java.lang.System
     2.6  import java.util.regex.Pattern
     2.7 -import java.util.Locale
     2.8  import java.net.URL
     2.9  import java.io.{File => JFile}
    2.10  
    2.11 @@ -94,7 +93,7 @@
    2.12        val rest =
    2.13          posix_path match {
    2.14            case Cygdrive(drive, rest) =>
    2.15 -            result_path ++= (drive.toUpperCase(Locale.ENGLISH) + ":" + JFile.separator)
    2.16 +            result_path ++= (Library.uppercase(drive) + ":" + JFile.separator)
    2.17              rest
    2.18            case Named_Root(root, rest) =>
    2.19              result_path ++= JFile.separator
    2.20 @@ -129,7 +128,7 @@
    2.21        jvm_path.replace('/', '\\') match {
    2.22          case Platform_Root(rest) => "/" + rest.replace('\\', '/')
    2.23          case Drive(letter, rest) =>
    2.24 -          "/cygdrive/" + letter.toLowerCase(Locale.ENGLISH) +
    2.25 +          "/cygdrive/" + Library.lowercase(letter) +
    2.26              (if (rest == "") "" else "/" + rest.replace('\\', '/'))
    2.27          case path => path.replace('\\', '/')
    2.28        }
     3.1 --- a/src/Pure/library.scala	Fri Nov 30 21:28:35 2012 +0100
     3.2 +++ b/src/Pure/library.scala	Fri Nov 30 21:30:24 2012 +0100
     3.3 @@ -85,9 +85,12 @@
     3.4      if (str.endsWith("\n")) str.substring(0, str.length - 1)
     3.5      else str
     3.6  
     3.7 +  def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
     3.8 +  def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
     3.9 +
    3.10    def capitalize(str: String): String =
    3.11      if (str.length == 0) str
    3.12 -    else str.substring(0, 1).toUpperCase(Locale.ENGLISH) + str.substring(1)
    3.13 +    else uppercase(str.substring(0, 1)) + str.substring(1)
    3.14  
    3.15  
    3.16    /* quote */
     4.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Fri Nov 30 21:28:35 2012 +0100
     4.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Fri Nov 30 21:30:24 2012 +0100
     4.3 @@ -35,10 +35,10 @@
     4.4    "src/rich_text_area.scala"
     4.5    "src/scala_console.scala"
     4.6    "src/sendback.scala"
     4.7 -  "src/session_dockable.scala"
     4.8    "src/symbols_dockable.scala"
     4.9    "src/syslog_dockable.scala"
    4.10    "src/text_overview.scala"
    4.11 +  "src/theories_dockable.scala"
    4.12    "src/token_markup.scala"
    4.13  )
    4.14  
     5.1 --- a/src/Tools/jEdit/src/Isabelle.props	Fri Nov 30 21:28:35 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Fri Nov 30 21:30:24 2012 +0100
     5.3 @@ -47,8 +47,8 @@
     5.4  
     5.5  #menu actions
     5.6  plugin.isabelle.jedit.Plugin.menu.label=Isabelle
     5.7 -plugin.isabelle.jedit.Plugin.menu=isabelle.session-panel isabelle.output-panel isabelle.graphview-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.symbols-panel isabelle.syslog-panel
     5.8 -isabelle.session-panel.label=Prover Session panel
     5.9 +plugin.isabelle.jedit.Plugin.menu=isabelle.theories-panel isabelle.output-panel isabelle.graphview-panel isabelle.raw-output-panel isabelle.protocol-panel isabelle.readme-panel isabelle.symbols-panel isabelle.syslog-panel
    5.10 +isabelle.theories-panel.label=Theories panel
    5.11  isabelle.output-panel.label=Output panel
    5.12  isabelle.graphview-panel.label=Graphview panel
    5.13  isabelle.raw-output-panel.label=Raw Output panel
    5.14 @@ -58,7 +58,7 @@
    5.15  isabelle.syslog-panel.label=Syslog panel
    5.16  
    5.17  #dockables
    5.18 -isabelle-session.title=Prover Session
    5.19 +isabelle-theories.title=Theories
    5.20  isabelle-output.title=Output
    5.21  isabelle-info.title=Info
    5.22  isabelle-graphview.title=Graphview
     6.1 --- a/src/Tools/jEdit/src/actions.xml	Fri Nov 30 21:28:35 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/actions.xml	Fri Nov 30 21:30:24 2012 +0100
     6.3 @@ -2,9 +2,9 @@
     6.4  <!DOCTYPE ACTIONS SYSTEM "actions.dtd">
     6.5  
     6.6  <ACTIONS>
     6.7 -	<ACTION NAME="isabelle.session-panel">
     6.8 +	<ACTION NAME="isabelle.theories-panel">
     6.9  		<CODE>
    6.10 -			wm.addDockableWindow("isabelle-session");
    6.11 +			wm.addDockableWindow("isabelle-theories");
    6.12  		</CODE>
    6.13  	</ACTION>
    6.14  	<ACTION NAME="isabelle.syslog-panel">
     7.1 --- a/src/Tools/jEdit/src/dockables.xml	Fri Nov 30 21:28:35 2012 +0100
     7.2 +++ b/src/Tools/jEdit/src/dockables.xml	Fri Nov 30 21:30:24 2012 +0100
     7.3 @@ -2,8 +2,8 @@
     7.4  <!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
     7.5  
     7.6  <DOCKABLES>
     7.7 -	<DOCKABLE NAME="isabelle-session" MOVABLE="TRUE">
     7.8 -		new isabelle.jedit.Session_Dockable(view, position);
     7.9 +	<DOCKABLE NAME="isabelle-theories" MOVABLE="TRUE">
    7.10 +		new isabelle.jedit.Theories_Dockable(view, position);
    7.11  	</DOCKABLE>
    7.12  	<DOCKABLE NAME="isabelle-syslog" MOVABLE="TRUE">
    7.13  		new isabelle.jedit.Syslog_Dockable(view, position);
     8.1 --- a/src/Tools/jEdit/src/isabelle.scala	Fri Nov 30 21:28:35 2012 +0100
     8.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Fri Nov 30 21:30:24 2012 +0100
     8.3 @@ -20,9 +20,9 @@
     8.4  
     8.5    private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
     8.6  
     8.7 -  def docked_session(view: View): Option[Session_Dockable] =
     8.8 -    wm(view).getDockableWindow("isabelle-session") match {
     8.9 -      case dockable: Session_Dockable => Some(dockable)
    8.10 +  def docked_theories(view: View): Option[Theories_Dockable] =
    8.11 +    wm(view).getDockableWindow("isabelle-theories") match {
    8.12 +      case dockable: Theories_Dockable => Some(dockable)
    8.13        case _ => None
    8.14      }
    8.15  
     9.1 --- a/src/Tools/jEdit/src/jEdit.props	Fri Nov 30 21:28:35 2012 +0100
     9.2 +++ b/src/Tools/jEdit/src/jEdit.props	Fri Nov 30 21:30:24 2012 +0100
     9.3 @@ -181,7 +181,7 @@
     9.4  isabelle-output.height=174
     9.5  isabelle-output.width=412
     9.6  isabelle-readme.dock-position=bottom
     9.7 -isabelle-session.dock-position=bottom
     9.8 +isabelle-theories.dock-position=bottom
     9.9  isabelle-symbols.dock-position=bottom
    9.10  line-end.shortcut=END
    9.11  line-home.shortcut=HOME
    10.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Fri Nov 30 21:28:35 2012 +0100
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,176 +0,0 @@
    10.4 -/*  Title:      Tools/jEdit/src/session_dockable.scala
    10.5 -    Author:     Makarius
    10.6 -
    10.7 -Dockable window for prover session management.
    10.8 -*/
    10.9 -
   10.10 -package isabelle.jedit
   10.11 -
   10.12 -
   10.13 -import isabelle._
   10.14 -
   10.15 -import scala.actors.Actor._
   10.16 -import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
   10.17 -import scala.swing.event.{ButtonClicked, MouseClicked}
   10.18 -
   10.19 -import java.lang.System
   10.20 -import java.awt.{BorderLayout, Graphics2D, Insets}
   10.21 -import javax.swing.{JList, BorderFactory}
   10.22 -import javax.swing.border.{BevelBorder, SoftBevelBorder}
   10.23 -
   10.24 -import org.gjt.sp.jedit.{View, jEdit}
   10.25 -
   10.26 -
   10.27 -class Session_Dockable(view: View, position: String) extends Dockable(view, position)
   10.28 -{
   10.29 -  /* status */
   10.30 -
   10.31 -  private val status = new ListView(Nil: List[Document.Node.Name]) {
   10.32 -    listenTo(mouse.clicks)
   10.33 -    reactions += {
   10.34 -      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
   10.35 -        val index = peer.locationToIndex(point)
   10.36 -        if (index >= 0) jEdit.openFile(view, listData(index).node)
   10.37 -    }
   10.38 -  }
   10.39 -  status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
   10.40 -  status.peer.setVisibleRowCount(0)
   10.41 -  status.selection.intervalMode = ListView.IntervalMode.Single
   10.42 -
   10.43 -  set_content(new ScrollPane(status))
   10.44 -
   10.45 -
   10.46 -  /* controls */
   10.47 -
   10.48 -  private val session_phase = new Label(PIDE.session.phase.toString)
   10.49 -  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   10.50 -  session_phase.tooltip = "Prover status"
   10.51 -
   10.52 -  private def handle_phase(phase: Session.Phase)
   10.53 -  {
   10.54 -    Swing_Thread.later { session_phase.text = " " + phase.toString + " " }
   10.55 -  }
   10.56 -
   10.57 -  private val cancel = new Button("Cancel") {
   10.58 -    reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
   10.59 -  }
   10.60 -  cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
   10.61 -
   10.62 -  private val check = new Button("Check") {
   10.63 -    reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
   10.64 -  }
   10.65 -  check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
   10.66 -
   10.67 -  private val logic = Isabelle_Logic.logic_selector(true)
   10.68 -
   10.69 -  private val controls =
   10.70 -    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
   10.71 -  add(controls.peer, BorderLayout.NORTH)
   10.72 -
   10.73 -
   10.74 -  /* component state -- owned by Swing thread */
   10.75 -
   10.76 -  private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
   10.77 -
   10.78 -  private object Node_Renderer_Component extends Label
   10.79 -  {
   10.80 -    opaque = false
   10.81 -    xAlignment = Alignment.Leading
   10.82 -    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
   10.83 -
   10.84 -    var node_name = Document.Node.Name.empty
   10.85 -    override def paintComponent(gfx: Graphics2D)
   10.86 -    {
   10.87 -      nodes_status.get(node_name) match {
   10.88 -        case Some(st) if st.total > 0 =>
   10.89 -          val size = peer.getSize()
   10.90 -          val insets = border.getBorderInsets(this.peer)
   10.91 -          val w = size.width - insets.left - insets.right
   10.92 -          val h = size.height - insets.top - insets.bottom
   10.93 -          var end = size.width - insets.right
   10.94 -          for {
   10.95 -            (n, color) <- List(
   10.96 -              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
   10.97 -              (st.running, PIDE.options.color_value("running_color")),
   10.98 -              (st.warned, PIDE.options.color_value("warning_color")),
   10.99 -              (st.failed, PIDE.options.color_value("error_color"))) }
  10.100 -          {
  10.101 -            gfx.setColor(color)
  10.102 -            val v = (n * w / st.total) max (if (n > 0) 2 else 0)
  10.103 -            gfx.fillRect(end - v, insets.top, v, h)
  10.104 -            end -= v
  10.105 -          }
  10.106 -        case _ =>
  10.107 -      }
  10.108 -      super.paintComponent(gfx)
  10.109 -    }
  10.110 -  }
  10.111 -
  10.112 -  private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
  10.113 -  {
  10.114 -    def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
  10.115 -      name: Document.Node.Name, index: Int): Component =
  10.116 -    {
  10.117 -      val component = Node_Renderer_Component
  10.118 -      component.node_name = name
  10.119 -      component.text = name.theory
  10.120 -      component
  10.121 -    }
  10.122 -  }
  10.123 -  status.renderer = new Node_Renderer
  10.124 -
  10.125 -  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
  10.126 -  {
  10.127 -    Swing_Thread.now {
  10.128 -      val snapshot = PIDE.session.snapshot()
  10.129 -
  10.130 -      val iterator =
  10.131 -        restriction match {
  10.132 -          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
  10.133 -          case None => snapshot.version.nodes.entries
  10.134 -        }
  10.135 -      val nodes_status1 =
  10.136 -        (nodes_status /: iterator)({ case (status, (name, node)) =>
  10.137 -            if (PIDE.thy_load.loaded_theories(name.theory)) status
  10.138 -            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
  10.139 -
  10.140 -      if (nodes_status != nodes_status1) {
  10.141 -        nodes_status = nodes_status1
  10.142 -        status.listData =
  10.143 -          snapshot.version.nodes.topological_order.filter(
  10.144 -            (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
  10.145 -      }
  10.146 -    }
  10.147 -  }
  10.148 -
  10.149 -
  10.150 -  /* main actor */
  10.151 -
  10.152 -  private val main_actor = actor {
  10.153 -    loop {
  10.154 -      react {
  10.155 -        case phase: Session.Phase => handle_phase(phase)
  10.156 -
  10.157 -        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
  10.158 -
  10.159 -        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
  10.160 -
  10.161 -        case bad => System.err.println("Session_Dockable: ignoring bad message " + bad)
  10.162 -      }
  10.163 -    }
  10.164 -  }
  10.165 -
  10.166 -  override def init()
  10.167 -  {
  10.168 -    PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
  10.169 -    PIDE.session.global_options += main_actor
  10.170 -    PIDE.session.commands_changed += main_actor; handle_update()
  10.171 -  }
  10.172 -
  10.173 -  override def exit()
  10.174 -  {
  10.175 -    PIDE.session.phase_changed -= main_actor
  10.176 -    PIDE.session.global_options -= main_actor
  10.177 -    PIDE.session.commands_changed -= main_actor
  10.178 -  }
  10.179 -}
    11.1 --- a/src/Tools/jEdit/src/symbols_dockable.scala	Fri Nov 30 21:28:35 2012 +0100
    11.2 +++ b/src/Tools/jEdit/src/symbols_dockable.scala	Fri Nov 30 21:30:24 2012 +0100
    11.3 @@ -10,16 +10,18 @@
    11.4  import isabelle._
    11.5  
    11.6  import java.awt.Font
    11.7 -import org.gjt.sp.jedit.View
    11.8  
    11.9  import scala.swing.event.ValueChanged
   11.10  import scala.swing.{Action, Button, FlowPanel, TabbedPane, TextField, BorderPanel, Label}
   11.11  
   11.12 +import org.gjt.sp.jedit.View
   11.13 +
   11.14 +
   11.15  class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
   11.16  {
   11.17    val searchspace =
   11.18      for ((group, symbols) <- Symbol.groups; sym <- symbols)
   11.19 -      yield (sym, sym.toLowerCase)
   11.20 +      yield (sym, Library.lowercase(sym))
   11.21  
   11.22    private class Symbol_Component(val symbol: String) extends Button
   11.23    {
   11.24 @@ -75,7 +77,8 @@
   11.25            val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
   11.26            results_panel.contents.clear
   11.27            val results =
   11.28 -            (searchspace filter (search.text.toLowerCase.split("\\s+") forall _._2.contains)
   11.29 +            (searchspace filter
   11.30 +              (Library.lowercase(search.text).split("\\s+") forall _._2.contains)
   11.31                take (max_results + 1)).toList
   11.32            for ((sym, _) <- results)
   11.33              results_panel.contents += new Symbol_Component(sym)
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Fri Nov 30 21:30:24 2012 +0100
    12.3 @@ -0,0 +1,179 @@
    12.4 +/*  Title:      Tools/jEdit/src/theories_dockable.scala
    12.5 +    Author:     Makarius
    12.6 +
    12.7 +Dockable window for theories managed by prover.
    12.8 +*/
    12.9 +
   12.10 +package isabelle.jedit
   12.11 +
   12.12 +
   12.13 +import isabelle._
   12.14 +
   12.15 +import scala.actors.Actor._
   12.16 +import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component}
   12.17 +import scala.swing.event.{ButtonClicked, MouseClicked}
   12.18 +
   12.19 +import java.lang.System
   12.20 +import java.awt.{BorderLayout, Graphics2D, Insets}
   12.21 +import javax.swing.{JList, BorderFactory}
   12.22 +import javax.swing.border.{BevelBorder, SoftBevelBorder}
   12.23 +
   12.24 +import org.gjt.sp.jedit.{View, jEdit}
   12.25 +
   12.26 +
   12.27 +class Theories_Dockable(view: View, position: String) extends Dockable(view, position)
   12.28 +{
   12.29 +  /* status */
   12.30 +
   12.31 +  private val status = new ListView(Nil: List[Document.Node.Name]) {
   12.32 +    listenTo(mouse.clicks)
   12.33 +    reactions += {
   12.34 +      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
   12.35 +        val index = peer.locationToIndex(point)
   12.36 +        if (index >= 0) jEdit.openFile(view, listData(index).node)
   12.37 +    }
   12.38 +  }
   12.39 +  status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
   12.40 +  status.peer.setVisibleRowCount(0)
   12.41 +  status.selection.intervalMode = ListView.IntervalMode.Single
   12.42 +
   12.43 +  set_content(new ScrollPane(status))
   12.44 +
   12.45 +
   12.46 +  /* controls */
   12.47 +
   12.48 +  def phase_text(phase: Session.Phase): String =
   12.49 +    "Prover: " + Library.lowercase(phase.toString)
   12.50 +
   12.51 +  private val session_phase = new Label(phase_text(PIDE.session.phase))
   12.52 +  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
   12.53 +  session_phase.tooltip = "Status of prover session"
   12.54 +
   12.55 +  private def handle_phase(phase: Session.Phase)
   12.56 +  {
   12.57 +    Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
   12.58 +  }
   12.59 +
   12.60 +  private val cancel = new Button("Cancel") {
   12.61 +    reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
   12.62 +  }
   12.63 +  cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
   12.64 +
   12.65 +  private val check = new Button("Check") {
   12.66 +    reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
   12.67 +  }
   12.68 +  check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
   12.69 +
   12.70 +  private val logic = Isabelle_Logic.logic_selector(true)
   12.71 +
   12.72 +  private val controls =
   12.73 +    new FlowPanel(FlowPanel.Alignment.Right)(check, cancel, session_phase, logic)
   12.74 +  add(controls.peer, BorderLayout.NORTH)
   12.75 +
   12.76 +
   12.77 +  /* component state -- owned by Swing thread */
   12.78 +
   12.79 +  private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
   12.80 +
   12.81 +  private object Node_Renderer_Component extends Label
   12.82 +  {
   12.83 +    opaque = false
   12.84 +    xAlignment = Alignment.Leading
   12.85 +    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
   12.86 +
   12.87 +    var node_name = Document.Node.Name.empty
   12.88 +    override def paintComponent(gfx: Graphics2D)
   12.89 +    {
   12.90 +      nodes_status.get(node_name) match {
   12.91 +        case Some(st) if st.total > 0 =>
   12.92 +          val size = peer.getSize()
   12.93 +          val insets = border.getBorderInsets(this.peer)
   12.94 +          val w = size.width - insets.left - insets.right
   12.95 +          val h = size.height - insets.top - insets.bottom
   12.96 +          var end = size.width - insets.right
   12.97 +          for {
   12.98 +            (n, color) <- List(
   12.99 +              (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
  12.100 +              (st.running, PIDE.options.color_value("running_color")),
  12.101 +              (st.warned, PIDE.options.color_value("warning_color")),
  12.102 +              (st.failed, PIDE.options.color_value("error_color"))) }
  12.103 +          {
  12.104 +            gfx.setColor(color)
  12.105 +            val v = (n * w / st.total) max (if (n > 0) 2 else 0)
  12.106 +            gfx.fillRect(end - v, insets.top, v, h)
  12.107 +            end -= v
  12.108 +          }
  12.109 +        case _ =>
  12.110 +      }
  12.111 +      super.paintComponent(gfx)
  12.112 +    }
  12.113 +  }
  12.114 +
  12.115 +  private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
  12.116 +  {
  12.117 +    def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
  12.118 +      name: Document.Node.Name, index: Int): Component =
  12.119 +    {
  12.120 +      val component = Node_Renderer_Component
  12.121 +      component.node_name = name
  12.122 +      component.text = name.theory
  12.123 +      component
  12.124 +    }
  12.125 +  }
  12.126 +  status.renderer = new Node_Renderer
  12.127 +
  12.128 +  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
  12.129 +  {
  12.130 +    Swing_Thread.now {
  12.131 +      val snapshot = PIDE.session.snapshot()
  12.132 +
  12.133 +      val iterator =
  12.134 +        restriction match {
  12.135 +          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
  12.136 +          case None => snapshot.version.nodes.entries
  12.137 +        }
  12.138 +      val nodes_status1 =
  12.139 +        (nodes_status /: iterator)({ case (status, (name, node)) =>
  12.140 +            if (PIDE.thy_load.loaded_theories(name.theory)) status
  12.141 +            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
  12.142 +
  12.143 +      if (nodes_status != nodes_status1) {
  12.144 +        nodes_status = nodes_status1
  12.145 +        status.listData =
  12.146 +          snapshot.version.nodes.topological_order.filter(
  12.147 +            (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
  12.148 +      }
  12.149 +    }
  12.150 +  }
  12.151 +
  12.152 +
  12.153 +  /* main actor */
  12.154 +
  12.155 +  private val main_actor = actor {
  12.156 +    loop {
  12.157 +      react {
  12.158 +        case phase: Session.Phase => handle_phase(phase)
  12.159 +
  12.160 +        case _: Session.Global_Options => Swing_Thread.later { logic.load () }
  12.161 +
  12.162 +        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
  12.163 +
  12.164 +        case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
  12.165 +      }
  12.166 +    }
  12.167 +  }
  12.168 +
  12.169 +  override def init()
  12.170 +  {
  12.171 +    PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
  12.172 +    PIDE.session.global_options += main_actor
  12.173 +    PIDE.session.commands_changed += main_actor; handle_update()
  12.174 +  }
  12.175 +
  12.176 +  override def exit()
  12.177 +  {
  12.178 +    PIDE.session.phase_changed -= main_actor
  12.179 +    PIDE.session.global_options -= main_actor
  12.180 +    PIDE.session.commands_changed -= main_actor
  12.181 +  }
  12.182 +}