src/Tools/jEdit/src/sledgehammer_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56918 a442dc6d244d
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
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@53711
    12
import scala.swing.{Button, Component, Label, TextField, 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@52908
    24
  val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@52908
    25
  set_content(pretty_text_area)
wenzelm@52908
    26
wenzelm@52908
    27
wenzelm@52908
    28
  /* query operation */
wenzelm@52908
    29
wenzelm@52935
    30
  private val process_indicator = new Process_Indicator
wenzelm@52935
    31
wenzelm@52935
    32
  private def consume_status(status: Query_Operation.Status.Value)
wenzelm@52935
    33
  {
wenzelm@52935
    34
    status match {
wenzelm@52935
    35
      case Query_Operation.Status.WAITING =>
wenzelm@52935
    36
        process_indicator.update("Waiting for evaluation of context ...", 5)
wenzelm@52935
    37
      case Query_Operation.Status.RUNNING =>
wenzelm@52935
    38
        process_indicator.update("Sledgehammering ...", 15)
wenzelm@54640
    39
      case Query_Operation.Status.FINISHED =>
wenzelm@52935
    40
        process_indicator.update(null, 0)
wenzelm@52935
    41
    }
wenzelm@52935
    42
  }
wenzelm@52935
    43
wenzelm@52908
    44
  private val sledgehammer =
wenzelm@52971
    45
    new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status _,
wenzelm@52908
    46
      (snapshot, results, body) =>
wenzelm@52908
    47
        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@52908
    48
wenzelm@52908
    49
wenzelm@52908
    50
  /* resize */
wenzelm@52908
    51
wenzelm@52908
    52
  private var zoom_factor = 100
wenzelm@52908
    53
wenzelm@52908
    54
  private def handle_resize()
wenzelm@52908
    55
  {
wenzelm@56662
    56
    Swing_Thread.require {}
wenzelm@52908
    57
wenzelm@55825
    58
    pretty_text_area.resize(
wenzelm@55825
    59
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
wenzelm@52908
    60
  }
wenzelm@52908
    61
wenzelm@52908
    62
  private val delay_resize =
wenzelm@52908
    63
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@52908
    64
wenzelm@52908
    65
  addComponentListener(new ComponentAdapter {
wenzelm@52908
    66
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@52908
    67
  })
wenzelm@52908
    68
wenzelm@52908
    69
wenzelm@52908
    70
  /* controls */
wenzelm@52908
    71
wenzelm@52908
    72
  private def clicked {
wenzelm@56623
    73
    PIDE.options.string("sledgehammer_provers") = provers.getText
wenzelm@53057
    74
    sledgehammer.apply_query(List(provers.getText, isar_proofs.selected.toString))
wenzelm@52908
    75
  }
wenzelm@52908
    76
wenzelm@52939
    77
  private val provers_label = new Label("Provers:") {
wenzelm@54367
    78
    tooltip =
wenzelm@56622
    79
      GUI.tooltip_lines(
wenzelm@56622
    80
        "Automatic provers as space-separated list, e.g.\ne spass remote_vampire")
wenzelm@52908
    81
  }
wenzelm@52908
    82
wenzelm@52908
    83
  private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
wenzelm@52933
    84
    override def processKeyEvent(evt: KeyEvent)
wenzelm@52933
    85
    {
wenzelm@52933
    86
      if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
wenzelm@52933
    87
      super.processKeyEvent(evt)
wenzelm@52933
    88
    }
wenzelm@52908
    89
    setToolTipText(provers_label.tooltip)
wenzelm@53055
    90
    setColumns(30)
wenzelm@52908
    91
  }
wenzelm@52908
    92
wenzelm@56623
    93
  private def update_provers()
wenzelm@56623
    94
  {
wenzelm@56623
    95
    val new_provers = PIDE.options.string("sledgehammer_provers")
wenzelm@56623
    96
    if (new_provers != provers.getText) {
wenzelm@56623
    97
      provers.setText(new_provers)
wenzelm@56623
    98
      if (provers.getCaret != null)
wenzelm@56623
    99
        provers.getCaret.setDot(0)
wenzelm@56623
   100
    }
wenzelm@56623
   101
  }
wenzelm@56623
   102
wenzelm@52908
   103
  private val isar_proofs = new CheckBox("Isar proofs") {
wenzelm@52908
   104
    tooltip = "Specify whether Isar proofs should be output in addition to metis line"
wenzelm@52908
   105
    selected = false
wenzelm@52908
   106
  }
wenzelm@52908
   107
wenzelm@52908
   108
  private val apply_query = new Button("Apply") {
wenzelm@52908
   109
    tooltip = "Search for first-order proof using automatic theorem provers"
wenzelm@52908
   110
    reactions += { case ButtonClicked(_) => clicked }
wenzelm@52908
   111
  }
wenzelm@52908
   112
wenzelm@52931
   113
  private val cancel_query = new Button("Cancel") {
wenzelm@52939
   114
    tooltip = "Interrupt unfinished sledgehammering"
wenzelm@52931
   115
    reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() }
wenzelm@52931
   116
  }
wenzelm@52931
   117
wenzelm@52908
   118
  private val locate_query = new Button("Locate") {
wenzelm@52908
   119
    tooltip = "Locate context of current query within source text"
wenzelm@52908
   120
    reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
wenzelm@52908
   121
  }
wenzelm@52908
   122
wenzelm@52908
   123
  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
wenzelm@52908
   124
    tooltip = "Zoom factor for output font size"
wenzelm@52908
   125
  }
wenzelm@52908
   126
wenzelm@52908
   127
  private val controls =
wenzelm@53711
   128
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@53057
   129
      provers_label, Component.wrap(provers), isar_proofs,
wenzelm@52935
   130
      process_indicator.component, apply_query, cancel_query, locate_query, zoom)
wenzelm@52908
   131
  add(controls.peer, BorderLayout.NORTH)
wenzelm@53787
   132
wenzelm@53847
   133
  override def focusOnDefaultComponent { provers.requestFocus }
wenzelm@56624
   134
wenzelm@56624
   135
wenzelm@56715
   136
  /* main */
wenzelm@56624
   137
wenzelm@56715
   138
  private val main =
wenzelm@56715
   139
    Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@56715
   140
      case _: Session.Global_Options => Swing_Thread.later { update_provers(); handle_resize() }
wenzelm@56624
   141
    }
wenzelm@56624
   142
wenzelm@56624
   143
  override def init()
wenzelm@56624
   144
  {
wenzelm@56715
   145
    PIDE.session.global_options += main
wenzelm@56624
   146
    update_provers()
wenzelm@56624
   147
    handle_resize()
wenzelm@56624
   148
    sledgehammer.activate()
wenzelm@56624
   149
  }
wenzelm@56624
   150
wenzelm@56624
   151
  override def exit()
wenzelm@56624
   152
  {
wenzelm@56624
   153
    sledgehammer.deactivate()
wenzelm@56715
   154
    PIDE.session.global_options -= main
wenzelm@56624
   155
    delay_resize.revoke()
wenzelm@56624
   156
  }
wenzelm@52908
   157
}