src/Tools/jEdit/src/sledgehammer_dockable.scala
author wenzelm
Fri, 27 Nov 2015 18:47:39 +0100
changeset 61750 c6c2508f94b8
parent 61207 46fa8f71e0ed
child 65246 848965b5befc
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/sledgehammer_dockable.scala
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     3
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     4
Dockable window for Sledgehammer.
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     5
*/
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     6
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     8
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
     9
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    10
import isabelle._
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    11
61750
wenzelm
parents: 61207
diff changeset
    12
import scala.swing.{Button, Component, Label, CheckBox}
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    13
import scala.swing.event.ButtonClicked
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    14
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    15
import java.awt.BorderLayout
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    16
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    17
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    18
import org.gjt.sp.jedit.View
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    19
import org.gjt.sp.jedit.gui.HistoryTextField
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    20
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    21
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    22
class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position)
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    23
{
61207
wenzelm
parents: 60861
diff changeset
    24
  GUI_Thread.require {}
wenzelm
parents: 60861
diff changeset
    25
wenzelm
parents: 60861
diff changeset
    26
wenzelm
parents: 60861
diff changeset
    27
  /* text area */
wenzelm
parents: 60861
diff changeset
    28
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    29
  val pretty_text_area = new Pretty_Text_Area(view)
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    30
  set_content(pretty_text_area)
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    31
56918
a442dc6d244d clarified detach_operation: ignore empty output;
wenzelm
parents: 56715
diff changeset
    32
  override def detach_operation = pretty_text_area.detach_operation
a442dc6d244d clarified detach_operation: ignore empty output;
wenzelm
parents: 56715
diff changeset
    33
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    34
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    35
  /* query operation */
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    36
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    37
  private val process_indicator = new Process_Indicator
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    38
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    39
  private def consume_status(status: Query_Operation.Status.Value)
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    40
  {
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    41
    status match {
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    42
      case Query_Operation.Status.WAITING =>
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    43
        process_indicator.update("Waiting for evaluation of context ...", 5)
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    44
      case Query_Operation.Status.RUNNING =>
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    45
        process_indicator.update("Sledgehammering ...", 15)
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 54367
diff changeset
    46
      case Query_Operation.Status.FINISHED =>
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    47
        process_indicator.update(null, 0)
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    48
    }
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    49
  }
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
    50
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    51
  private val sledgehammer =
52971
31926d2c04ee tuned signature -- more abstract PIDE editor operations;
wenzelm
parents: 52939
diff changeset
    52
    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    53
      (snapshot, results, body) =>
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    54
        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    55
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    56
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    57
  /* resize */
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    58
61207
wenzelm
parents: 60861
diff changeset
    59
  private val delay_resize =
wenzelm
parents: 60861
diff changeset
    60
    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm
parents: 60861
diff changeset
    61
wenzelm
parents: 60861
diff changeset
    62
  addComponentListener(new ComponentAdapter {
wenzelm
parents: 60861
diff changeset
    63
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm
parents: 60861
diff changeset
    64
    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
wenzelm
parents: 60861
diff changeset
    65
  })
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    66
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    67
  private def handle_resize()
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    68
  {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57044
diff changeset
    69
    GUI_Thread.require {}
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    70
55825
694833e3e4a0 tuned signature -- separate module Font_Info;
wenzelm
parents: 55618
diff changeset
    71
    pretty_text_area.resize(
57044
042d6e58cb40 more uniform Font_Info.Zoom_Box;
wenzelm
parents: 56919
diff changeset
    72
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    73
  }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    74
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    75
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    76
  /* controls */
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    77
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    78
  private def clicked {
60861
fa77faa87d5f maintain history more often;
wenzelm
parents: 60750
diff changeset
    79
    provers.addCurrentToHistory()
56623
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
    80
    PIDE.options.string("sledgehammer_provers") = provers.getText
60202
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
    81
    sledgehammer.apply_query(
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
    82
      List(provers.getText, isar_proofs.selected.toString, try0.selected.toString))
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    83
  }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    84
52939
3b549ee12623 tuned GUI;
wenzelm
parents: 52935
diff changeset
    85
  private val provers_label = new Label("Provers:") {
54367
e358b79b533a tuned tooltips;
wenzelm
parents: 53872
diff changeset
    86
    tooltip =
56622
891d1b8b64fb clarified tooltip_lines: HTML.encode already takes care of newline (but not space);
wenzelm
parents: 55825
diff changeset
    87
      GUI.tooltip_lines(
60278
2a9bc6447779 clarified tooltip;
wenzelm
parents: 60202
diff changeset
    88
        "Automatic provers as space-separated list, e.g.\n" +
2a9bc6447779 clarified tooltip;
wenzelm
parents: 60202
diff changeset
    89
          PIDE.options.value.check_name("sledgehammer_provers").default_value)
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    90
  }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    91
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    92
  private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
52933
08bbd321ac4c more active "provers" field, which increases chances that its history is stored;
wenzelm
parents: 52931
diff changeset
    93
    override def processKeyEvent(evt: KeyEvent)
08bbd321ac4c more active "provers" field, which increases chances that its history is stored;
wenzelm
parents: 52931
diff changeset
    94
    {
08bbd321ac4c more active "provers" field, which increases chances that its history is stored;
wenzelm
parents: 52931
diff changeset
    95
      if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
08bbd321ac4c more active "provers" field, which increases chances that its history is stored;
wenzelm
parents: 52931
diff changeset
    96
      super.processKeyEvent(evt)
08bbd321ac4c more active "provers" field, which increases chances that its history is stored;
wenzelm
parents: 52931
diff changeset
    97
    }
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
    98
    setToolTipText(provers_label.tooltip)
53055
0fe8a9972eda some protocol to determine provers according to ML;
wenzelm
parents: 53049
diff changeset
    99
    setColumns(30)
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   100
  }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   101
56623
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   102
  private def update_provers()
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   103
  {
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   104
    val new_provers = PIDE.options.string("sledgehammer_provers")
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   105
    if (new_provers != provers.getText) {
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   106
      provers.setText(new_provers)
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   107
      if (provers.getCaret != null)
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   108
        provers.getCaret.setDot(0)
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   109
    }
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   110
  }
4675df68450e more elementary option sledgehammer_provers, avoiding complications of defaults from ML side (NB: guessing at number of cores does not make sense in PIDE);
wenzelm
parents: 56622
diff changeset
   111
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   112
  private val isar_proofs = new CheckBox("Isar proofs") {
60202
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
   113
    tooltip = "Specify whether Isar proofs should be output in addition to \"by\" one-liner"
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   114
    selected = false
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   115
  }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   116
60202
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
   117
  private val try0 = new CheckBox("Try methods") {
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
   118
    tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
   119
    selected = true
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
   120
  }
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
   121
56919
6389a8c1268a tuned GUI;
wenzelm
parents: 56918
diff changeset
   122
  private val apply_query = new Button("<html><b>Apply</b></html>") {
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   123
    tooltip = "Search for first-order proof using automatic theorem provers"
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   124
    reactions += { case ButtonClicked(_) => clicked }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   125
  }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   126
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52908
diff changeset
   127
  private val cancel_query = new Button("Cancel") {
52939
3b549ee12623 tuned GUI;
wenzelm
parents: 52935
diff changeset
   128
    tooltip = "Interrupt unfinished sledgehammering"
52931
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52908
diff changeset
   129
    reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() }
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52908
diff changeset
   130
  }
ac6648c0c0fb cancel_query via direct access to the exec_id of the running query process;
wenzelm
parents: 52908
diff changeset
   131
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   132
  private val locate_query = new Button("Locate") {
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   133
    tooltip = "Locate context of current query within source text"
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   134
    reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   135
  }
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   136
61207
wenzelm
parents: 60861
diff changeset
   137
  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
wenzelm
parents: 60861
diff changeset
   138
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   139
  private val controls =
53711
8ce7795256e1 improved FlowLayout for wrapping of components over multiple lines;
wenzelm
parents: 53177
diff changeset
   140
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
60202
a95023a21725 added checkbox for try0;
wenzelm
parents: 57612
diff changeset
   141
      provers_label, Component.wrap(provers), isar_proofs, try0,
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52933
diff changeset
   142
      process_indicator.component, apply_query, cancel_query, locate_query, zoom)
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   143
  add(controls.peer, BorderLayout.NORTH)
53787
e64389fe2d2c focus on default component according to jEdit window management;
wenzelm
parents: 53711
diff changeset
   144
53847
104a08c2be9f focus text field, to capture key events even on Mac OS X look-and-feel;
wenzelm
parents: 53787
diff changeset
   145
  override def focusOnDefaultComponent { provers.requestFocus }
56624
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   146
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   147
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   148
  /* main */
56624
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   149
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   150
  private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   151
    Session.Consumer[Session.Global_Options](getClass.getName) {
57612
990ffb84489b clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents: 57044
diff changeset
   152
      case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() }
56624
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   153
    }
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   154
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   155
  override def init()
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   156
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   157
    PIDE.session.global_options += main
56624
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   158
    update_provers()
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   159
    handle_resize()
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   160
    sledgehammer.activate()
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   161
  }
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   162
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   163
  override def exit()
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   164
  {
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   165
    sledgehammer.deactivate()
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   166
    PIDE.session.global_options -= main
56624
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   167
    delay_resize.revoke()
7eed0fee0241 clarified actor plumbing;
wenzelm
parents: 56623
diff changeset
   168
  }
52908
3461985dcbc3 dockable window for Sledgehammer, based on asynchronous/parallel query operation;
wenzelm
parents:
diff changeset
   169
}