src/Tools/jEdit/src/theories_dockable.scala
author wenzelm
Mon, 29 Jul 2013 13:43:12 +0200
changeset 52763 3b5f4f2ff108
parent 52759 a20631db9c8a
child 52769 0827b6f5de44
permissions -rw-r--r--
always init GUI state;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
     1
/*  Title:      Tools/jEdit/src/theories_dockable.scala
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
     3
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
     4
Dockable window for theories managed by prover.
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
     5
*/
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
     6
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
     8
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
     9
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    10
import isabelle._
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    11
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    12
import scala.actors.Actor._
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    13
import scala.swing.{FlowPanel, Button, TextArea, Label, ListView, Alignment, ScrollPane, Component,
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    14
  BoxPanel, Orientation, RadioButton, ButtonGroup}
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents: 49245
diff changeset
    15
import scala.swing.event.{ButtonClicked, MouseClicked}
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    16
43520
cec9b95fa35d explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents: 43282
diff changeset
    17
import java.lang.System
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    18
import java.awt.{BorderLayout, Graphics2D, Insets, Color}
47588
1f8f1c2045fd tuned imports;
wenzelm
parents: 46918
diff changeset
    19
import javax.swing.{JList, BorderFactory}
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    20
import javax.swing.border.{BevelBorder, SoftBevelBorder, LineBorder}
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    21
44865
679f0d57e831 some keyboard shortcuts for important actions;
wenzelm
parents: 44864
diff changeset
    22
import org.gjt.sp.jedit.{View, jEdit}
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    23
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    24
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    25
class Theories_Dockable(view: View, position: String) extends Dockable(view, position)
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    26
{
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents: 48018
diff changeset
    27
  /* status */
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39589
diff changeset
    28
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents: 48018
diff changeset
    29
  private val status = new ListView(Nil: List[Document.Node.Name]) {
44991
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    30
    listenTo(mouse.clicks)
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    31
    reactions += {
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    32
      case MouseClicked(_, point, _, clicks, _) if clicks == 2 =>
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    33
        val index = peer.locationToIndex(point)
51534
123bd97fcea1 mixed theory/command entries;
wenzelm
parents: 50900
diff changeset
    34
        if (index >= 0) Hyperlink(listData(index).node).follow(view)
44991
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    35
    }
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    36
  }
50250
267bd685a69f smarter list layout;
wenzelm
parents: 50209
diff changeset
    37
  status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
267bd685a69f smarter list layout;
wenzelm
parents: 50209
diff changeset
    38
  status.peer.setVisibleRowCount(0)
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
    39
  status.selection.intervalMode = ListView.IntervalMode.Single
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
    40
49038
2f0530b81c45 recovered ScrollPane from d899be1cfe6d;
wenzelm
parents: 48870
diff changeset
    41
  set_content(new ScrollPane(status))
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    42
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    43
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    44
  /* controls */
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    45
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    46
  def phase_text(phase: Session.Phase): String =
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    47
    "Prover: " + Library.lowercase(phase.toString)
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    48
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    49
  private val session_phase = new Label(phase_text(PIDE.session.phase))
39697
d54242927fb1 tuned border;
wenzelm
parents: 39696
diff changeset
    50
  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    51
  session_phase.tooltip = "Status of prover session"
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    52
48018
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
    53
  private def handle_phase(phase: Session.Phase)
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
    54
  {
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    55
    Swing_Thread.later { session_phase.text = " " + phase_text(phase) + " " }
48018
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
    56
  }
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
    57
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    58
  private val execution_range = new BoxPanel(Orientation.Horizontal) {
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    59
    private def button(range: PIDE.Execution_Range.Value): RadioButton =
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    60
      new RadioButton(range.toString) {
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    61
        reactions += { case ButtonClicked(_) => PIDE.update_execution_range(range) }
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    62
      }
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    63
    private val label = new Label("Range:") { tooltip = "range of continuous document processing" }
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    64
    private val b1 = button(PIDE.Execution_Range.ALL)
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    65
    private val b2 = button(PIDE.Execution_Range.NONE)
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    66
    private val b3 = button(PIDE.Execution_Range.VISIBLE)
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    67
    private val group = new ButtonGroup(b1, b2, b3)
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    68
    contents ++= List(label, b1, b2, b3)
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    69
    border = new LineBorder(Color.GRAY)
44775
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
    70
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    71
    def load()
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    72
    {
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    73
      PIDE.execution_range() match {
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    74
        case PIDE.Execution_Range.ALL => group.select(b1)
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    75
        case PIDE.Execution_Range.NONE => group.select(b2)
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    76
        case PIDE.Execution_Range.VISIBLE => group.select(b3)
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    77
      }
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    78
    }
52763
3b5f4f2ff108 always init GUI state;
wenzelm
parents: 52759
diff changeset
    79
    load()
44776
47e8c8daccae added "check" button: adhoc change to full buffer perspective;
wenzelm
parents: 44775
diff changeset
    80
  }
47e8c8daccae added "check" button: adhoc change to full buffer perspective;
wenzelm
parents: 44775
diff changeset
    81
49246
248e66e8321f more systematic JEdit_Options.make_component;
wenzelm
parents: 49245
diff changeset
    82
  private val logic = Isabelle_Logic.logic_selector(true)
39702
d7c256cb2797 Session_Dockable: more startup controls;
wenzelm
parents: 39701
diff changeset
    83
44775
27930cf6f0f7 added "cancel" button based on cancel_execution, not interrupt (cf. 156be0e43336);
wenzelm
parents: 44734
diff changeset
    84
  private val controls =
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
    85
    new FlowPanel(FlowPanel.Alignment.Right)(execution_range, session_phase, logic)
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    86
  add(controls.peer, BorderLayout.NORTH)
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    87
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    88
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
    89
  /* component state -- owned by Swing thread */
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
    90
45709
87017fcbad83 clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;
wenzelm
parents: 45672
diff changeset
    91
  private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
    92
44990
wenzelm
parents: 44989
diff changeset
    93
  private object Node_Renderer_Component extends Label
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
    94
  {
44990
wenzelm
parents: 44989
diff changeset
    95
    opaque = false
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
    96
    xAlignment = Alignment.Leading
44989
5450ab3c677e explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents: 44981
diff changeset
    97
    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
    98
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
    99
    var node_name = Document.Node.Name.empty
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   100
    override def paintComponent(gfx: Graphics2D)
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   101
    {
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   102
      nodes_status.get(node_name) match {
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   103
        case Some(st) if st.total > 0 =>
50900
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   104
          val colors = List(
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   105
            (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   106
            (st.running, PIDE.options.color_value("running_color")),
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   107
            (st.warned, PIDE.options.color_value("warning_color")),
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   108
            (st.failed, PIDE.options.color_value("error_color")))
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   109
44958
86e4916825ee more precise painting;
wenzelm
parents: 44957
diff changeset
   110
          val size = peer.getSize()
51535
wenzelm
parents: 51534
diff changeset
   111
          val insets = border.getBorderInsets(peer)
44958
86e4916825ee more precise painting;
wenzelm
parents: 44957
diff changeset
   112
          val w = size.width - insets.left - insets.right
86e4916825ee more precise painting;
wenzelm
parents: 44957
diff changeset
   113
          val h = size.height - insets.top - insets.bottom
86e4916825ee more precise painting;
wenzelm
parents: 44957
diff changeset
   114
          var end = size.width - insets.right
50900
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   115
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   116
          for { (n, color) <- colors }
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   117
          {
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   118
            gfx.setColor(color)
50900
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   119
            val v = (n * (w - colors.length) / st.total) max (if (n > 0) 4 else 0)
44958
86e4916825ee more precise painting;
wenzelm
parents: 44957
diff changeset
   120
            gfx.fillRect(end - v, insets.top, v, h)
50900
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   121
            end = end - v - 1
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   122
          }
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   123
        case _ =>
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   124
      }
44867
79d3d74e7cbb stronger colors (as background);
wenzelm
parents: 44866
diff changeset
   125
      super.paintComponent(gfx)
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   126
    }
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   127
  }
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   128
44990
wenzelm
parents: 44989
diff changeset
   129
  private class Node_Renderer extends ListView.Renderer[Document.Node.Name]
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   130
  {
44990
wenzelm
parents: 44989
diff changeset
   131
    def componentFor(list: ListView[_], isSelected: Boolean, focused: Boolean,
wenzelm
parents: 44989
diff changeset
   132
      name: Document.Node.Name, index: Int): Component =
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   133
    {
44990
wenzelm
parents: 44989
diff changeset
   134
      val component = Node_Renderer_Component
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   135
      component.node_name = name
44989
5450ab3c677e explicit border independent of UI (cf. ad5883642a83, 2bec3b7514cf);
wenzelm
parents: 44981
diff changeset
   136
      component.text = name.theory
44990
wenzelm
parents: 44989
diff changeset
   137
      component
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   138
    }
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   139
  }
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   140
  status.renderer = new Node_Renderer
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   141
45011
436ea69d5d37 more careful treatment of initial update, similar to output panel;
wenzelm
parents: 44991
diff changeset
   142
  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   143
  {
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   144
    Swing_Thread.now {
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50183
diff changeset
   145
      val snapshot = PIDE.session.snapshot()
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44609
diff changeset
   146
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46688
diff changeset
   147
      val iterator =
54ea872b60ea more explicit development graph;
wenzelm
parents: 46688
diff changeset
   148
        restriction match {
54ea872b60ea more explicit development graph;
wenzelm
parents: 46688
diff changeset
   149
          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
54ea872b60ea more explicit development graph;
wenzelm
parents: 46688
diff changeset
   150
          case None => snapshot.version.nodes.entries
54ea872b60ea more explicit development graph;
wenzelm
parents: 46688
diff changeset
   151
        }
46681
c083a3f621c0 more abstract class Document.Version;
wenzelm
parents: 45709
diff changeset
   152
      val nodes_status1 =
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46688
diff changeset
   153
        (nodes_status /: iterator)({ case (status, (name, node)) =>
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50183
diff changeset
   154
            if (PIDE.thy_load.loaded_theories(name.theory)) status
46739
6024353549ca clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
wenzelm
parents: 46723
diff changeset
   155
            else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44641
diff changeset
   156
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44641
diff changeset
   157
      if (nodes_status != nodes_status1) {
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44641
diff changeset
   158
        nodes_status = nodes_status1
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   159
        status.listData =
46723
54ea872b60ea more explicit development graph;
wenzelm
parents: 46688
diff changeset
   160
          snapshot.version.nodes.topological_order.filter(
44960
640c2b957f16 graph traversal in topological order;
wenzelm
parents: 44958
diff changeset
   161
            (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   162
      }
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   163
    }
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   164
  }
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   165
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   166
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   167
  /* main actor */
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   168
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   169
  private val main_actor = actor {
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   170
    loop {
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   171
      react {
48018
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   172
        case phase: Session.Phase => handle_phase(phase)
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
   173
52759
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
   174
        case _: Session.Global_Options =>
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
   175
          Swing_Thread.later {
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
   176
            execution_range.load()
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
   177
            logic.load ()
a20631db9c8a support declarative editor_execution_range, instead of old-style check/cancel buttons;
wenzelm
parents: 51535
diff changeset
   178
          }
49247
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   179
45011
436ea69d5d37 more careful treatment of initial update, similar to output panel;
wenzelm
parents: 44991
diff changeset
   180
        case changed: Session.Commands_Changed => handle_update(Some(changed.nodes))
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   181
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
   182
        case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   183
      }
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   184
    }
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   185
  }
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   186
48018
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   187
  override def init()
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   188
  {
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50183
diff changeset
   189
    PIDE.session.phase_changed += main_actor; handle_phase(PIDE.session.phase)
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50183
diff changeset
   190
    PIDE.session.global_options += main_actor
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50183
diff changeset
   191
    PIDE.session.commands_changed += main_actor; handle_update()
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
   192
  }
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
   193
48018
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   194
  override def exit()
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   195
  {
50205
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50183
diff changeset
   196
    PIDE.session.phase_changed -= main_actor
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50183
diff changeset
   197
    PIDE.session.global_options -= main_actor
788c8263e634 renamed main plugin object to PIDE;
wenzelm
parents: 50183
diff changeset
   198
    PIDE.session.commands_changed -= main_actor
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
   199
  }
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   200
}