src/Tools/jEdit/src/theories_dockable.scala
author wenzelm
Wed, 15 Mar 2017 12:41:22 +0100
changeset 65256 c3d6dd17d626
parent 65246 848965b5befc
child 65355 403eabd73c9a
permissions -rw-r--r--
more explicit options; tuned signature;
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
53711
8ce7795256e1 improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents: 53178
diff changeset
    12
import scala.swing.{Button, TextArea, Label, ListView, Alignment,
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
    13
  ScrollPane, Component, CheckBox, BorderPanel}
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
    14
import scala.swing.event.{ButtonClicked, MouseClicked, MouseMoved}
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    15
53178
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
    16
import java.awt.{BorderLayout, Graphics2D, Color, Point, Dimension}
56389
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
    17
import javax.swing.{JList, BorderFactory, UIManager}
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
    18
import javax.swing.border.{BevelBorder, SoftBevelBorder}
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    19
44865
679f0d57e831 some keyboard shortcuts for important actions;
wenzelm
parents: 44864
diff changeset
    20
import org.gjt.sp.jedit.{View, jEdit}
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    21
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    22
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    23
class Theories_Dockable(view: View, position: String) extends Dockable(view, position)
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    24
{
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents: 48018
diff changeset
    25
  /* status */
39591
a43a723753e6 more content for Session_Dockable;
wenzelm
parents: 39589
diff changeset
    26
48021
d899be1cfe6d separate syslog dockable -- discontinued tendency of sub-window management via tabs;
wenzelm
parents: 48018
diff changeset
    27
  private val status = new ListView(Nil: List[Document.Node.Name]) {
56389
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
    28
    background =
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
    29
    {
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
    30
      // enforce default value
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
    31
      val c = UIManager.getDefaults.getColor("Panel.background")
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
    32
      new Color(c.getRed, c.getGreen, c.getBlue, c.getAlpha)
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
    33
    }
44991
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    34
    listenTo(mouse.clicks)
52817
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    35
    listenTo(mouse.moves)
44991
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    36
    reactions += {
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
    37
      case MouseClicked(_, point, _, clicks, _) =>
44991
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    38
        val index = peer.locationToIndex(point)
52817
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    39
        if (index >= 0) {
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    40
          if (in_checkbox(peer.indexToLocation(index), point)) {
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    41
            if (clicks == 1) Document_Model.node_required(listData(index), toggle = true)
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
    42
          }
65246
848965b5befc clarified singleton module;
wenzelm
parents: 65206
diff changeset
    43
          else if (clicks == 2) JEdit_Editor.goto_file(true, view, listData(index).node)
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
    44
        }
52817
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    45
      case MouseMoved(_, point, _) =>
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    46
        val index = peer.locationToIndex(point)
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    47
        if (index >= 0 && in_checkbox(peer.indexToLocation(index), point))
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    48
          tooltip = "Mark as required for continuous checking"
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    49
        else
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    50
          tooltip = null
44991
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    51
    }
d88f7fc62a40 double clicks switch to document node buffer;
wenzelm
parents: 44990
diff changeset
    52
  }
50250
267bd685a69f smarter list layout;
wenzelm
parents: 50209
diff changeset
    53
  status.peer.setLayoutOrientation(JList.HORIZONTAL_WRAP)
267bd685a69f smarter list layout;
wenzelm
parents: 50209
diff changeset
    54
  status.peer.setVisibleRowCount(0)
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
    55
  status.selection.intervalMode = ListView.IntervalMode.Single
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
    56
49038
2f0530b81c45 recovered ScrollPane from d899be1cfe6d;
wenzelm
parents: 48870
diff changeset
    57
  set_content(new ScrollPane(status))
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    58
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
    59
39593
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    60
  /* controls */
1a34187f0b97 basic setup for Session_Dockable controls;
wenzelm
parents: 39591
diff changeset
    61
65206
ff8c3c29a924 clarified Session.Phase;
wenzelm
parents: 64867
diff changeset
    62
  def phase_text(phase: Session.Phase): String = "Prover: " + phase.print
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    63
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    64
  private val session_phase = new Label(phase_text(PIDE.session.phase))
39697
d54242927fb1 tuned border;
wenzelm
parents: 39696
diff changeset
    65
  session_phase.border = new SoftBevelBorder(BevelBorder.LOWERED)
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50250
diff changeset
    66
  session_phase.tooltip = "Status of prover session"
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
    67
48018
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
    68
  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
    69
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56715
diff changeset
    70
    GUI_Thread.require {}
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 53176
diff changeset
    71
    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
    72
  }
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
    73
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
    74
  private val purge = new Button("Purge") {
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
    75
    tooltip = "Restrict document model to theories required for open editor buffers"
65246
848965b5befc clarified singleton module;
wenzelm
parents: 65206
diff changeset
    76
    reactions += { case ButtonClicked(_) => JEdit_Editor.purge() }
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
    77
  }
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
    78
53715
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53711
diff changeset
    79
  private val continuous_checking = new Isabelle.Continuous_Checking
54652
07ee041537a5 non-focusable button, to avoid second interpretation of SPACE in C+e SPACE (isabelle.set-node-required);
wenzelm
parents: 53715
diff changeset
    80
  continuous_checking.focusable = false
44776
47e8c8daccae added "check" button: adhoc change to full buffer perspective;
wenzelm
parents: 44775
diff changeset
    81
65256
c3d6dd17d626 more explicit options;
wenzelm
parents: 65246
diff changeset
    82
  private val logic = JEdit_Sessions.logic_selector(PIDE.options.value, 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 =
64867
e7220f4de11f support "purge" operation on document model;
wenzelm
parents: 64854
diff changeset
    85
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(purge, continuous_checking, 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
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56715
diff changeset
    89
  /* component state -- owned by GUI thread */
44609
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
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
    92
  private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
    93
52817
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    94
  private def in_checkbox(loc0: Point, p: Point): Boolean =
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    95
    Node_Renderer_Component != null &&
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    96
      (Node_Renderer_Component.checkbox_geometry match {
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    97
        case Some((loc, size)) =>
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    98
          loc0.x + loc.x <= p.x && p.x < loc0.x + size.width &&
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
    99
          loc0.y + loc.y <= p.y && p.y < loc0.y + size.height
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
   100
        case None => false
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
   101
      })
408fb2e563df added home-made tooltips;
wenzelm
parents: 52816
diff changeset
   102
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   103
  private object Node_Renderer_Component extends BorderPanel
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   104
  {
56389
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
   105
    opaque = true
53176
f88635e1c52e clarified border (again, see also 7ce3ebc268a1);
wenzelm
parents: 52980
diff changeset
   106
    border = BorderFactory.createEmptyBorder(2, 2, 2, 2)
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   107
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   108
    var node_name = Document.Node.Name.empty
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   109
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   110
    var checkbox_geometry: Option[(Point, Dimension)] = None
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   111
    val checkbox = new CheckBox {
52819
7ce3ebc268a1 proper border (again) -- avoid NPE on Windows;
wenzelm
parents: 52817
diff changeset
   112
      opaque = false
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   113
      override def paintComponent(gfx: Graphics2D)
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   114
      {
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   115
        super.paintComponent(gfx)
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   116
        if (location != null && size != null)
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   117
          checkbox_geometry = Some((location, size))
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   118
      }
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   119
    }
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   120
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   121
    val label = new Label {
56389
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
   122
      background = view.getTextArea.getPainter.getBackground
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
   123
      foreground = view.getTextArea.getPainter.getForeground
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
   124
      border =
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
   125
        BorderFactory.createCompoundBorder(
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
   126
          BorderFactory.createLineBorder(foreground, 1),
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
   127
          BorderFactory.createEmptyBorder(1, 1, 1, 1))
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   128
      opaque = false
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   129
      xAlignment = Alignment.Leading
52809
e750169a5884 paint unassigned/unchanged nodes as unprocessed -- relevant for editor_continuous_checking = false;
wenzelm
parents: 52807
diff changeset
   130
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   131
      override def paintComponent(gfx: Graphics2D)
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   132
      {
53178
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   133
        def paint_segment(x: Int, w: Int, color: Color)
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   134
        {
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   135
          gfx.setColor(color)
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   136
          gfx.fillRect(x, 0, w, size.height)
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   137
        }
50900
6d80709ab862 separate color ranges by 1px to improve discernment of overall theory status;
wenzelm
parents: 50895
diff changeset
   138
56389
e49561ae3b65 tuned rendering for 5 different look-and-feels;
wenzelm
parents: 56372
diff changeset
   139
        paint_segment(0, size.width, background)
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   140
        nodes_status.get(node_name) match {
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   141
          case Some(st) if st.total > 0 =>
53178
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   142
            val segments =
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   143
              List(
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   144
                (st.unprocessed, PIDE.options.color_value("unprocessed1_color")),
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   145
                (st.running, PIDE.options.color_value("running_color")),
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   146
                (st.warned, PIDE.options.color_value("warning_color")),
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   147
                (st.failed, PIDE.options.color_value("error_color"))
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   148
              ).filter(_._1 > 0)
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   149
56407
8e7ebc4b30f1 tuned rendering -- take 1px line border into account;
wenzelm
parents: 56389
diff changeset
   150
            ((size.width - 1) /: segments)({ case (last, (n, color)) =>
8e7ebc4b30f1 tuned rendering -- take 1px line border into account;
wenzelm
parents: 56389
diff changeset
   151
              val w = (n * ((size.width - 2) - segments.length) / st.total) max 4
53178
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   152
              paint_segment(last - w, w, color)
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   153
              last - w - 1
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   154
            })
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   155
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   156
          case _ =>
53178
0a3a5f606b2a more precise painting;
wenzelm
parents: 53177
diff changeset
   157
            paint_segment(0, size.width, PIDE.options.color_value("unprocessed1_color"))
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   158
        }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   159
        super.paintComponent(gfx)
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   160
      }
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   161
    }
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   162
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   163
    layout(checkbox) = BorderPanel.Position.West
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   164
    layout(label) = BorderPanel.Position.Center
44866
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   165
  }
0eb8284a64bd some color scheme for theory status;
wenzelm
parents: 44865
diff changeset
   166
44990
wenzelm
parents: 44989
diff changeset
   167
  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
   168
  {
64443
857acb970dfa back to stable scala-2.11.8;
wenzelm
parents: 64442
diff changeset
   169
    def componentFor(list: ListView[_], isSelected: Boolean,
64442
85adb337e32f updated to scala-2.12.0;
wenzelm
parents: 62973
diff changeset
   170
      focused: Boolean, name: Document.Node.Name, index: Int): Component =
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   171
    {
44990
wenzelm
parents: 44989
diff changeset
   172
      val component = Node_Renderer_Component
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   173
      component.node_name = name
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   174
      component.checkbox.selected = nodes_required.contains(name)
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 52809
diff changeset
   175
      component.label.text = name.theory
44990
wenzelm
parents: 44989
diff changeset
   176
      component
44957
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   177
    }
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   178
  }
098dd95349e7 more elaborate Node_Renderer, which paints node_name.theory only;
wenzelm
parents: 44867
diff changeset
   179
  status.renderer = new Node_Renderer
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   180
45011
436ea69d5d37 more careful treatment of initial update, similar to output panel;
wenzelm
parents: 44991
diff changeset
   181
  private def handle_update(restriction: Option[Set[Document.Node.Name]] = None)
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   182
  {
62052
8bcbf1c93119 node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
wenzelm
parents: 61716
diff changeset
   183
    GUI_Thread.require {}
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 53176
diff changeset
   184
62052
8bcbf1c93119 node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
wenzelm
parents: 61716
diff changeset
   185
    val snapshot = PIDE.session.snapshot()
57619
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   186
    val nodes = snapshot.version.nodes
44613
a3255c85327b crude display of node status;
wenzelm
parents: 44609
diff changeset
   187
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 53176
diff changeset
   188
    val iterator =
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57612
diff changeset
   189
      restriction match {
57619
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   190
        case Some(names) => names.iterator.map(name => (name, nodes(name)))
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   191
        case None => nodes.iterator
57615
df1b3452d71c more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents: 57612
diff changeset
   192
      }
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 53176
diff changeset
   193
    val nodes_status1 =
62052
8bcbf1c93119 node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
wenzelm
parents: 61716
diff changeset
   194
      (nodes_status /: iterator)({ case (status, (name, node)) =>
64854
f5aa712e6250 tuned signature;
wenzelm
parents: 64817
diff changeset
   195
          if (!name.is_theory || PIDE.resources.base.loaded_theories(name.theory) || node.is_empty)
57619
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   196
            status
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 53176
diff changeset
   197
          else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
44672
07dad1433cd7 some support to prune_history;
wenzelm
parents: 44641
diff changeset
   198
57619
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   199
    val nodes_status2 =
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   200
      nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))
dcd69422b953 clarified display;
wenzelm
parents: 57617
diff changeset
   201
62052
8bcbf1c93119 node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
wenzelm
parents: 61716
diff changeset
   202
    if (nodes_status != nodes_status2) {
8bcbf1c93119 node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
wenzelm
parents: 61716
diff changeset
   203
      nodes_status = nodes_status2
8bcbf1c93119 node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
wenzelm
parents: 61716
diff changeset
   204
      status.listData = nodes.topological_order.filter(nodes_status.isDefinedAt(_))
8bcbf1c93119 node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
wenzelm
parents: 61716
diff changeset
   205
    }
44609
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   206
  }
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   207
6ec4a5eb2fc0 some support for theory status overview;
wenzelm
parents: 44335
diff changeset
   208
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   209
  /* main */
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   210
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   211
  private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   212
    Session.Consumer[Any](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   213
      case phase: Session.Phase =>
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56715
diff changeset
   214
        GUI_Thread.later { handle_phase(phase) }
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
   215
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   216
      case _: Session.Global_Options =>
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 56715
diff changeset
   217
        GUI_Thread.later {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   218
          continuous_checking.load()
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   219
          logic.load ()
64817
0bb6b582bb4f separate Buffer_Model vs. File_Model;
wenzelm
parents: 64813
diff changeset
   220
          nodes_required = Document_Model.required_nodes()
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   221
          status.repaint()
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   222
        }
49247
ffd9ad9dc35b more detailed option tooltip;
wenzelm
parents: 49246
diff changeset
   223
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   224
      case changed: Session.Commands_Changed =>
62052
8bcbf1c93119 node_status update is back on GUI thread (reverting 3ad2b2055ffc) -- avoid potential deadlock of GUI_Thread.now during shutdown, when GUI thread is already terminated;
wenzelm
parents: 61716
diff changeset
   225
        GUI_Thread.later { handle_update(Some(changed.nodes)) }
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   226
    }
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   227
48018
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   228
  override def init()
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   229
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   230
    PIDE.session.phase_changed += main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   231
    PIDE.session.global_options += main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   232
    PIDE.session.commands_changed += main
53177
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 53176
diff changeset
   233
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 53176
diff changeset
   234
    handle_phase(PIDE.session.phase)
dcac8d837b9c more uniform treatment of Swing_Thread context switch: prefer asynchronous Swing_Thread.later from actor;
wenzelm
parents: 53176
diff changeset
   235
    handle_update()
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
   236
  }
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
   237
48018
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   238
  override def exit()
b941dd7df92a make double sure that GUI components are up-to-date after init;
wenzelm
parents: 48014
diff changeset
   239
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   240
    PIDE.session.phase_changed -= main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   241
    PIDE.session.global_options -= main
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   242
    PIDE.session.commands_changed -= main
39635
5cd8545a070b added Session_Dockable.session_phase label;
wenzelm
parents: 39629
diff changeset
   243
  }
39515
57ceabb0bb8e basic setup for prover session panel;
wenzelm
parents:
diff changeset
   244
}