src/Tools/jEdit/src/sledgehammer_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 61750 c6c2508f94b8
child 65246 848965b5befc
permissions -rw-r--r--
tuned signature;
wenzelm@52908
     1
/*  Title:      Tools/jEdit/src/sledgehammer_dockable.scala
wenzelm@52908
     2
    Author:     Makarius
wenzelm@52908
     3
wenzelm@52908
     4
Dockable window for Sledgehammer.
wenzelm@52908
     5
*/
wenzelm@52908
     6
wenzelm@52908
     7
package isabelle.jedit
wenzelm@52908
     8
wenzelm@52908
     9
wenzelm@52908
    10
import isabelle._
wenzelm@52908
    11
wenzelm@61750
    12
import scala.swing.{Button, Component, Label, CheckBox}
wenzelm@52908
    13
import scala.swing.event.ButtonClicked
wenzelm@52908
    14
wenzelm@52908
    15
import java.awt.BorderLayout
wenzelm@52908
    16
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
wenzelm@52908
    17
wenzelm@52908
    18
import org.gjt.sp.jedit.View
wenzelm@52908
    19
import org.gjt.sp.jedit.gui.HistoryTextField
wenzelm@52908
    20
wenzelm@52908
    21
wenzelm@52908
    22
class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@52908
    23
{
wenzelm@61207
    24
  GUI_Thread.require {}
wenzelm@61207
    25
wenzelm@61207
    26
wenzelm@61207
    27
  /* text area */
wenzelm@61207
    28
wenzelm@52908
    29
  val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@52908
    30
  set_content(pretty_text_area)
wenzelm@52908
    31
wenzelm@56918
    32
  override def detach_operation = pretty_text_area.detach_operation
wenzelm@56918
    33
wenzelm@52908
    34
wenzelm@52908
    35
  /* query operation */
wenzelm@52908
    36
wenzelm@52935
    37
  private val process_indicator = new Process_Indicator
wenzelm@52935
    38
wenzelm@52935
    39
  private def consume_status(status: Query_Operation.Status.Value)
wenzelm@52935
    40
  {
wenzelm@52935
    41
    status match {
wenzelm@52935
    42
      case Query_Operation.Status.WAITING =>
wenzelm@52935
    43
        process_indicator.update("Waiting for evaluation of context ...", 5)
wenzelm@52935
    44
      case Query_Operation.Status.RUNNING =>
wenzelm@52935
    45
        process_indicator.update("Sledgehammering ...", 15)
wenzelm@54640
    46
      case Query_Operation.Status.FINISHED =>
wenzelm@52935
    47
        process_indicator.update(null, 0)
wenzelm@52935
    48
    }
wenzelm@52935
    49
  }
wenzelm@52935
    50
wenzelm@52908
    51
  private val sledgehammer =
wenzelm@52971
    52
    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
wenzelm@52908
    53
      (snapshot, results, body) =>
wenzelm@52908
    54
        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@52908
    55
wenzelm@52908
    56
wenzelm@52908
    57
  /* resize */
wenzelm@52908
    58
wenzelm@61207
    59
  private val delay_resize =
wenzelm@61207
    60
    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@61207
    61
wenzelm@61207
    62
  addComponentListener(new ComponentAdapter {
wenzelm@61207
    63
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@61207
    64
    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@61207
    65
  })
wenzelm@52908
    66
wenzelm@52908
    67
  private def handle_resize()
wenzelm@52908
    68
  {
wenzelm@57612
    69
    GUI_Thread.require {}
wenzelm@52908
    70
wenzelm@55825
    71
    pretty_text_area.resize(
wenzelm@57044
    72
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
wenzelm@52908
    73
  }
wenzelm@52908
    74
wenzelm@52908
    75
wenzelm@52908
    76
  /* controls */
wenzelm@52908
    77
wenzelm@52908
    78
  private def clicked {
wenzelm@60861
    79
    provers.addCurrentToHistory()
wenzelm@56623
    80
    PIDE.options.string("sledgehammer_provers") = provers.getText
wenzelm@60202
    81
    sledgehammer.apply_query(
wenzelm@60202
    82
      List(provers.getText, isar_proofs.selected.toString, try0.selected.toString))
wenzelm@52908
    83
  }
wenzelm@52908
    84
wenzelm@52939
    85
  private val provers_label = new Label("Provers:") {
wenzelm@54367
    86
    tooltip =
wenzelm@56622
    87
      GUI.tooltip_lines(
wenzelm@60278
    88
        "Automatic provers as space-separated list, e.g.\n" +
wenzelm@60278
    89
          PIDE.options.value.check_name("sledgehammer_provers").default_value)
wenzelm@52908
    90
  }
wenzelm@52908
    91
wenzelm@52908
    92
  private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
wenzelm@52933
    93
    override def processKeyEvent(evt: KeyEvent)
wenzelm@52933
    94
    {
wenzelm@52933
    95
      if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
wenzelm@52933
    96
      super.processKeyEvent(evt)
wenzelm@52933
    97
    }
wenzelm@52908
    98
    setToolTipText(provers_label.tooltip)
wenzelm@53055
    99
    setColumns(30)
wenzelm@52908
   100
  }
wenzelm@52908
   101
wenzelm@56623
   102
  private def update_provers()
wenzelm@56623
   103
  {
wenzelm@56623
   104
    val new_provers = PIDE.options.string("sledgehammer_provers")
wenzelm@56623
   105
    if (new_provers != provers.getText) {
wenzelm@56623
   106
      provers.setText(new_provers)
wenzelm@56623
   107
      if (provers.getCaret != null)
wenzelm@56623
   108
        provers.getCaret.setDot(0)
wenzelm@56623
   109
    }
wenzelm@56623
   110
  }
wenzelm@56623
   111
wenzelm@52908
   112
  private val isar_proofs = new CheckBox("Isar proofs") {
wenzelm@60202
   113
    tooltip = "Specify whether Isar proofs should be output in addition to \"by\" one-liner"
wenzelm@52908
   114
    selected = false
wenzelm@52908
   115
  }
wenzelm@52908
   116
wenzelm@60202
   117
  private val try0 = new CheckBox("Try methods") {
wenzelm@60202
   118
    tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
wenzelm@60202
   119
    selected = true
wenzelm@60202
   120
  }
wenzelm@60202
   121
wenzelm@56919
   122
  private val apply_query = new Button("<html><b>Apply</b></html>") {
wenzelm@52908
   123
    tooltip = "Search for first-order proof using automatic theorem provers"
wenzelm@52908
   124
    reactions += { case ButtonClicked(_) => clicked }
wenzelm@52908
   125
  }
wenzelm@52908
   126
wenzelm@52931
   127
  private val cancel_query = new Button("Cancel") {
wenzelm@52939
   128
    tooltip = "Interrupt unfinished sledgehammering"
wenzelm@52931
   129
    reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() }
wenzelm@52931
   130
  }
wenzelm@52931
   131
wenzelm@52908
   132
  private val locate_query = new Button("Locate") {
wenzelm@52908
   133
    tooltip = "Locate context of current query within source text"
wenzelm@52908
   134
    reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
wenzelm@52908
   135
  }
wenzelm@52908
   136
wenzelm@61207
   137
  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
wenzelm@61207
   138
wenzelm@52908
   139
  private val controls =
wenzelm@53711
   140
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@60202
   141
      provers_label, Component.wrap(provers), isar_proofs, try0,
wenzelm@52935
   142
      process_indicator.component, apply_query, cancel_query, locate_query, zoom)
wenzelm@52908
   143
  add(controls.peer, BorderLayout.NORTH)
wenzelm@53787
   144
wenzelm@53847
   145
  override def focusOnDefaultComponent { provers.requestFocus }
wenzelm@56624
   146
wenzelm@56624
   147
wenzelm@56715
   148
  /* main */
wenzelm@56624
   149
wenzelm@56715
   150
  private val main =
wenzelm@56715
   151
    Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@57612
   152
      case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() }
wenzelm@56624
   153
    }
wenzelm@56624
   154
wenzelm@56624
   155
  override def init()
wenzelm@56624
   156
  {
wenzelm@56715
   157
    PIDE.session.global_options += main
wenzelm@56624
   158
    update_provers()
wenzelm@56624
   159
    handle_resize()
wenzelm@56624
   160
    sledgehammer.activate()
wenzelm@56624
   161
  }
wenzelm@56624
   162
wenzelm@56624
   163
  override def exit()
wenzelm@56624
   164
  {
wenzelm@56624
   165
    sledgehammer.deactivate()
wenzelm@56715
   166
    PIDE.session.global_options -= main
wenzelm@56624
   167
    delay_resize.revoke()
wenzelm@56624
   168
  }
wenzelm@52908
   169
}