diff --git a/src/Tools/Graphview/graph_panel.scala b/src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala
+++ b/src/Tools/Graphview/graph_panel.scala
@@ -1,342 +1,342 @@
/* Title: Tools/Graphview/graph_panel.scala
Author: Markus Kaiser, TU Muenchen
Author: Makarius
GUI panel for graph layout.
*/
package isabelle.graphview
import isabelle._
import java.awt.{Dimension, Graphics2D, Point, Rectangle}
import java.awt.geom.{AffineTransform, Point2D}
import javax.imageio.ImageIO
import javax.swing.{JScrollPane, JComponent, SwingUtilities}
import javax.swing.border.EmptyBorder
import scala.swing.{BorderPanel, Button, CheckBox, Action, FileChooser, Panel, ScrollPane}
import scala.swing.event.{Event, Key, MousePressed, MouseDragged, MouseClicked, MouseEvent}
class Graph_Panel(val graphview: Graphview) extends BorderPanel {
graph_panel =>
/** graph **/
/* painter */
private val painter = new Panel {
override def paint(gfx: Graphics2D): Unit = {
super.paintComponent(gfx)
gfx.setColor(graphview.background_color)
gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
gfx.transform(Transform())
graphview.paint(gfx)
}
}
def set_preferred_size(): Unit = {
val box = graphview.bounding_box()
val s = Transform.scale_discrete
painter.preferredSize = new Dimension((box.width * s).ceil.toInt, (box.height * s).ceil.toInt)
painter.revalidate()
}
def refresh(): Unit = {
if (painter != null) {
set_preferred_size()
painter.repaint()
}
}
def scroll_to_node(node: Graph_Display.Node): Unit = {
val gap = graphview.metrics.gap
val info = graphview.layout.get_node(node)
val t = Transform()
val p =
t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null)
val q =
t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null)
painter.peer.scrollRectToVisible(
new Rectangle(p.getX.toInt, p.getY.toInt,
(q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt))
}
/* scrollable graph pane */
private val graph_pane: ScrollPane = new ScrollPane(painter) {
tooltip = ""
override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
override def getToolTipText(event: java.awt.event.MouseEvent): String =
graphview.find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
case Some(node) =>
graphview.model.full_graph.get_node(node) match {
case Nil => null
case content =>
graphview.make_tooltip(graph_pane.peer, event.getX, event.getY, content)
}
case None => null
}
}
horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
listenTo(mouse.moves)
listenTo(mouse.clicks)
reactions +=
{
case MousePressed(_, p, _, _, _) =>
Mouse_Interaction.pressed(p)
painter.repaint()
case MouseDragged(_, to, _) =>
Mouse_Interaction.dragged(to)
painter.repaint()
case e @ MouseClicked(_, p, m, n, _) =>
Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer))
painter.repaint()
}
contents = painter
}
graph_pane.peer.getVerticalScrollBar.setUnitIncrement(10)
/* transform */
def rescale(s: Double): Unit = {
Transform.scale = s
if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt)
refresh()
}
def fit_to_window(): Unit = {
Transform.fit_to_window()
refresh()
}
private object Transform {
private var _scale: Double = 1.0
def scale: Double = _scale
def scale_=(s: Double): Unit = {
_scale = (s min 10.0) max 0.1
}
def scale_discrete: Double = {
val font_height = GUI.line_metrics(graphview.metrics.font).getHeight.toInt
(scale * font_height).floor / font_height
}
def apply(): AffineTransform = {
val box = graphview.bounding_box()
val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)
t.translate(- box.x, - box.y)
t
}
def fit_to_window(): Unit = {
if (graphview.visible_graph.is_empty)
rescale(1.0)
else {
val box = graphview.bounding_box()
rescale((size.width / box.width) min (size.height / box.height))
}
}
def pane_to_graph_coordinates(at: Point2D): Point2D = {
val s = Transform.scale_discrete
val p = Transform().inverseTransform(graph_pane.peer.getViewport.getViewPosition, null)
p.setLocation(p.getX + at.getX / s, p.getY + at.getY / s)
p
}
}
/* interaction */
graphview.model.Colors.events += { case _ => painter.repaint() }
graphview.model.Mutators.events += { case _ => painter.repaint() }
private object Mouse_Interaction {
private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) =
(new Point(0, 0), Nil, Nil)
def pressed(at: Point): Unit = {
val c = Transform.pane_to_graph_coordinates(at)
val l =
graphview.find_node(c) match {
case Some(node) =>
if (graphview.Selection.contains(node)) graphview.Selection.get()
else List(node)
case None => Nil
}
val d =
l match {
case Nil => graphview.find_dummy(c).toList
case _ => Nil
}
draginfo = (at, l, d)
}
def dragged(to: Point): Unit = {
val (from, p, d) = draginfo
val s = Transform.scale_discrete
val dx = to.x - from.x
val dy = to.y - from.y
(p, d) match {
case (Nil, Nil) =>
val r = graph_pane.peer.getViewport.getViewRect
r.translate(- dx, - dy)
painter.peer.scrollRectToVisible(r)
case (Nil, ds) =>
ds.foreach(d => graphview.translate_vertex(d, dx / s, dy / s))
case (ls, _) =>
ls.foreach(l => graphview.translate_vertex(Layout.Node(l), dx / s, dy / s))
}
draginfo = (to, p, d)
}
def clicked(at: Point, m: Key.Modifiers, clicks: Int, right_click: Boolean): Unit = {
val c = Transform.pane_to_graph_coordinates(at)
if (clicks < 2) {
if (right_click) {
// FIXME
if (false) {
val menu = Popups(graph_panel, graphview.find_node(c), graphview.Selection.get())
menu.show(graph_pane.peer, at.x, at.y)
}
}
else {
(graphview.find_node(c), m) match {
case (Some(node), Key.Modifier.Control) => graphview.Selection.add(node)
case (None, Key.Modifier.Control) =>
case (Some(node), Key.Modifier.Shift) => graphview.Selection.add(node)
case (None, Key.Modifier.Shift) =>
case (Some(node), _) =>
graphview.Selection.clear()
graphview.Selection.add(node)
case (None, _) =>
graphview.Selection.clear()
}
}
}
}
}
/** controls **/
private val mutator_dialog =
new Mutator_Dialog(graphview, graphview.model.Mutators, "Filters", "Hide", false)
private val color_dialog =
new Mutator_Dialog(graphview, graphview.model.Colors, "Colorations")
private val chooser = new FileChooser {
fileSelectionMode = FileChooser.SelectionMode.FilesOnly
title = "Save image (.png or .pdf)"
}
private val show_content = new CheckBox() {
selected = graphview.show_content
action = Action("Show content") {
graphview.show_content = selected
graphview.update_layout()
refresh()
}
tooltip = "Show full node content within graph layout"
}
private val show_arrow_heads = new CheckBox() {
selected = graphview.show_arrow_heads
action = Action("Show arrow heads") {
graphview.show_arrow_heads = selected
painter.repaint()
}
tooltip = "Draw edges with explicit arrow heads"
}
private val show_dummies = new CheckBox() {
selected = graphview.show_dummies
action = Action("Show dummies") {
graphview.show_dummies = selected
painter.repaint()
}
tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging"
}
private val save_image = new Button {
action = Action("Save image") {
chooser.showSaveDialog(this) match {
case FileChooser.Result.Approve =>
try { Graph_File.write(chooser.selectedFile, graphview) }
catch {
case ERROR(msg) => GUI.error_dialog(this.peer, "Error", GUI.scrollable_text(msg))
}
case _ =>
}
}
tooltip = "Save current graph layout as PNG or PDF"
}
- private val zoom = new GUI.Zoom_Box { def changed() = rescale(0.01 * factor) }
+ private val zoom = new GUI.Zoom_Box { def changed(): Unit = rescale(0.01 * factor) }
private val fit_window = new Button {
action = Action("Fit to window") { fit_to_window() }
tooltip = "Zoom to fit window width and height"
}
private val update_layout = new Button {
action = Action("Update layout") {
graphview.update_layout()
refresh()
}
tooltip = "Regenerate graph layout according to built-in algorithm"
}
private val editor_style = new CheckBox() {
selected = graphview.editor_style
action = Action("Editor style") {
graphview.editor_style = selected
graphview.update_layout()
refresh()
}
tooltip = "Use editor font and colors for painting"
}
private val colorations = new Button { action = Action("Colorations") { color_dialog.open() } }
private val filters = new Button { action = Action("Filters") { mutator_dialog.open() } }
private val controls =
Wrap_Panel(
List(show_content, show_arrow_heads, show_dummies,
save_image, zoom, fit_window, update_layout, editor_style)) // FIXME colorations, filters
/** main layout **/
layout(graph_pane) = BorderPanel.Position.Center
layout(controls) = BorderPanel.Position.North
rescale(1.0)
}
diff --git a/src/Tools/jEdit/src/debugger_dockable.scala b/src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala
+++ b/src/Tools/jEdit/src/debugger_dockable.scala
@@ -1,354 +1,354 @@
/* Title: Tools/jEdit/src/debugger_dockable.scala
Author: Makarius
Dockable window for Isabelle/ML debugger.
*/
package isabelle.jedit
import isabelle._
import java.awt.{BorderLayout, Dimension}
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent, FocusAdapter, FocusEvent,
MouseEvent, MouseAdapter}
import javax.swing.{JTree, JMenuItem}
import javax.swing.tree.{DefaultMutableTreeNode, DefaultTreeModel, TreeSelectionModel}
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener}
import scala.collection.immutable.SortedMap
import scala.swing.{Button, Label, Component, ScrollPane, SplitPane, Orientation,
CheckBox, BorderPanel}
import scala.swing.event.ButtonClicked
import org.gjt.sp.jedit.{jEdit, View}
import org.gjt.sp.jedit.menu.EnhancedMenuItem
import org.gjt.sp.jedit.textarea.JEditTextArea
object Debugger_Dockable {
/* breakpoints */
def get_breakpoint(text_area: JEditTextArea, offset: Text.Offset): Option[(Command, Long)] = {
GUI_Thread.require {}
Document_View.get(text_area) match {
case Some(doc_view) =>
val rendering = doc_view.get_rendering()
val range = JEdit_Lib.point_range(text_area.getBuffer, offset)
rendering.breakpoint(range)
case None => None
}
}
/* context menu */
def context_menu(text_area: JEditTextArea, offset: Text.Offset): List[JMenuItem] =
if (PIDE.session.debugger.is_active() && get_breakpoint(text_area, offset).isDefined) {
val context = jEdit.getActionContext()
val name = "isabelle.toggle-breakpoint"
List(new EnhancedMenuItem(context.getAction(name).getLabel, name, context))
}
else Nil
}
class Debugger_Dockable(view: View, position: String) extends Dockable(view, position) {
GUI_Thread.require {}
private val debugger = PIDE.session.debugger
/* component state -- owned by GUI thread */
private var current_snapshot = Document.Snapshot.init
private var current_threads: Debugger.Threads = SortedMap.empty
private var current_output: List[XML.Tree] = Nil
/* pretty text area */
val pretty_text_area = new Pretty_Text_Area(view)
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
private def handle_resize(): Unit = {
GUI_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
private def handle_update(): Unit = {
GUI_Thread.require {}
val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot)
val (new_threads, new_output) = debugger.status(tree_selection())
if (new_threads != current_threads)
update_tree(new_threads)
if (new_output != current_output)
pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output))
current_snapshot = new_snapshot
current_threads = new_threads
current_output = new_output
}
/* tree view */
private val root = new DefaultMutableTreeNode("Threads")
val tree = new JTree(root)
tree.setRowHeight(0)
tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION)
def tree_selection(): Option[Debugger.Context] =
tree.getLastSelectedPathComponent match {
case node: DefaultMutableTreeNode =>
node.getUserObject match {
case c: Debugger.Context => Some(c)
case _ => None
}
case _ => None
}
def thread_selection(): Option[String] = tree_selection().map(_.thread_name)
private def update_tree(threads: Debugger.Threads): Unit = {
val thread_contexts =
(for ((a, b) <- threads.iterator)
yield Debugger.Context(a, b)).toList
val new_tree_selection =
tree_selection() match {
case Some(c) if thread_contexts.contains(c) => Some(c)
case Some(c) if thread_contexts.exists(t => c.thread_name == t.thread_name) =>
Some(c.reset)
case _ => thread_contexts.headOption
}
tree.clearSelection
root.removeAllChildren
for (thread <- thread_contexts) {
val thread_node = new DefaultMutableTreeNode(thread)
for ((debug_state, i) <- thread.debug_states.zipWithIndex)
thread_node.add(new DefaultMutableTreeNode(thread.select(i)))
root.add(thread_node)
}
tree.getModel.asInstanceOf[DefaultTreeModel].reload(root)
tree.expandRow(0)
for (i <- Range.inclusive(tree.getRowCount - 1, 1, -1)) tree.expandRow(i)
new_tree_selection match {
case Some(c) =>
val i =
(for (t <- thread_contexts.iterator.takeWhile(t => c.thread_name != t.thread_name))
yield t.size).sum
tree.addSelectionRow(i + c.index + 1)
case None =>
}
tree.revalidate()
}
def update_vals(): Unit = {
tree_selection() match {
case Some(c) if c.stack_state.isDefined =>
debugger.print_vals(c, sml_button.selected, context_field.getText)
case Some(c) =>
debugger.clear_output(c.thread_name)
case None =>
}
}
tree.addTreeSelectionListener(
new TreeSelectionListener {
override def valueChanged(e: TreeSelectionEvent): Unit = {
update_focus()
update_vals()
}
})
tree.addMouseListener(
new MouseAdapter {
override def mouseClicked(e: MouseEvent): Unit = {
val click = tree.getPathForLocation(e.getX, e.getY)
if (click != null && e.getClickCount == 1)
update_focus()
}
})
private val tree_pane = new ScrollPane(Component.wrap(tree))
tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
tree_pane.minimumSize = new Dimension(200, 100)
/* controls */
private val break_button = new CheckBox("Break") {
tooltip = "Break running threads at next possible breakpoint"
selected = debugger.is_break()
reactions += { case ButtonClicked(_) => debugger.set_break(selected) }
}
private val continue_button = new Button("Continue") {
tooltip = "Continue program on current thread, until next breakpoint"
reactions += { case ButtonClicked(_) => thread_selection().map(debugger.continue) }
}
private val step_button = new Button("Step") {
tooltip = "Single-step in depth-first order"
reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step) }
}
private val step_over_button = new Button("Step over") {
tooltip = "Single-step within this function"
reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_over) }
}
private val step_out_button = new Button("Step out") {
tooltip = "Single-step outside this function"
reactions += { case ButtonClicked(_) => thread_selection().map(debugger.step_out) }
}
private val context_label = new Label("Context:") {
tooltip = "Isabelle/ML context: type theory, Proof.context, Context.generic"
}
private val context_field =
new Completion_Popup.History_Text_Field("isabelle-debugger-context") {
override def processKeyEvent(evt: KeyEvent): Unit = {
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
eval_expression()
super.processKeyEvent(evt)
}
setColumns(20)
setToolTipText(context_label.tooltip)
setFont(GUI.imitate_font(getFont, scale = 1.2))
}
private val expression_label = new Label("ML:") {
tooltip = "Isabelle/ML or Standard ML expression"
}
private val expression_field =
new Completion_Popup.History_Text_Field("isabelle-debugger-expression") {
override def processKeyEvent(evt: KeyEvent): Unit = {
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER)
eval_expression()
super.processKeyEvent(evt)
}
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
setToolTipText(expression_label.tooltip)
setFont(GUI.imitate_font(getFont, scale = 1.2))
}
private val eval_button = new Button("Eval") {
tooltip = "Evaluate ML expression within optional context"
reactions += { case ButtonClicked(_) => eval_expression() }
}
private def eval_expression(): Unit = {
context_field.addCurrentToHistory()
expression_field.addCurrentToHistory()
tree_selection() match {
case Some(c) if c.debug_index.isDefined =>
debugger.eval(c, sml_button.selected, context_field.getText, expression_field.getText)
case _ =>
}
}
private val sml_button = new CheckBox("SML") {
tooltip = "Official Standard ML instead of Isabelle/ML"
selected = false
}
- private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
List(
break_button, continue_button, step_button, step_over_button, step_out_button,
context_label, Component.wrap(context_field),
expression_label, Component.wrap(expression_field), eval_button, sml_button,
pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
/* focus */
override def focusOnDefaultComponent(): Unit = eval_button.requestFocus()
addFocusListener(new FocusAdapter {
override def focusGained(e: FocusEvent): Unit = update_focus()
})
private def update_focus(): Unit = {
for (c <- tree_selection()) {
debugger.set_focus(c)
for {
pos <- c.debug_position
link <- PIDE.editor.hyperlink_position(false, current_snapshot, pos)
} link.follow(view)
}
JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint())
}
/* main panel */
val main_panel: SplitPane = new SplitPane(Orientation.Vertical) {
oneTouchExpandable = true
leftComponent = tree_pane
rightComponent = Component.wrap(pretty_text_area)
}
set_content(main_panel)
/* main */
private val main =
Session.Consumer[Any](getClass.getName) {
case _: Session.Global_Options =>
GUI_Thread.later { handle_resize() }
case Debugger.Update =>
GUI_Thread.later {
break_button.selected = debugger.is_break()
handle_update()
}
}
override def init(): Unit = {
PIDE.session.global_options += main
PIDE.session.debugger_updates += main
debugger.init()
handle_update()
jEdit.propertiesChanged()
}
override def exit(): Unit = {
PIDE.session.global_options -= main
PIDE.session.debugger_updates -= main
delay_resize.revoke()
debugger.exit()
jEdit.propertiesChanged()
}
/* resize */
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
}
diff --git a/src/Tools/jEdit/src/info_dockable.scala b/src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala
+++ b/src/Tools/jEdit/src/info_dockable.scala
@@ -1,119 +1,119 @@
/* Title: Tools/jEdit/src/info_dockable.scala
Author: Makarius
Dockable window with info text.
*/
package isabelle.jedit
import isabelle._
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter, WindowFocusListener, WindowEvent}
import org.gjt.sp.jedit.View
object Info_Dockable {
/* implicit arguments -- owned by GUI thread */
private var implicit_snapshot = Document.Snapshot.init
private var implicit_results = Command.Results.empty
private var implicit_info: XML.Body = Nil
private def set_implicit(
snapshot: Document.Snapshot,
results: Command.Results,
info: XML.Body
): Unit = {
GUI_Thread.require {}
implicit_snapshot = snapshot
implicit_results = results
implicit_info = info
}
private def reset_implicit(): Unit =
set_implicit(Document.Snapshot.init, Command.Results.empty, Nil)
def apply(
view: View,
snapshot: Document.Snapshot,
results: Command.Results,
info: XML.Body
): Unit = {
set_implicit(snapshot, results, info)
view.getDockableWindowManager.floatDockableWindow("isabelle-info")
}
}
class Info_Dockable(view: View, position: String) extends Dockable(view, position) {
/* component state -- owned by GUI thread */
private val snapshot = Info_Dockable.implicit_snapshot
private val results = Info_Dockable.implicit_results
private val info = Info_Dockable.implicit_info
private val window_focus_listener =
new WindowFocusListener {
def windowGainedFocus(e: WindowEvent): Unit =
Info_Dockable.set_implicit(snapshot, results, info)
def windowLostFocus(e: WindowEvent): Unit =
Info_Dockable.reset_implicit()
}
/* pretty text area */
private val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
pretty_text_area.update(snapshot, results, info)
- private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private def handle_resize(): Unit = {
GUI_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
/* resize */
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
private val controls =
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
/* main */
private val main =
Session.Consumer[Session.Global_Options](getClass.getName) {
case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
}
override def init(): Unit = {
GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
PIDE.session.global_options += main
handle_resize()
}
override def exit(): Unit = {
GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
PIDE.session.global_options -= main
delay_resize.revoke()
}
}
diff --git a/src/Tools/jEdit/src/output_dockable.scala b/src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala
+++ b/src/Tools/jEdit/src/output_dockable.scala
@@ -1,152 +1,152 @@
/* Title: Tools/jEdit/src/output_dockable.scala
Author: Makarius
Dockable window with result message output.
*/
package isabelle.jedit
import isabelle._
import scala.swing.{Button, CheckBox}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
import org.gjt.sp.jedit.View
class Output_Dockable(view: View, position: String) extends Dockable(view, position) {
/* component state -- owned by GUI thread */
private var do_update = true
private var current_output: List[XML.Tree] = Nil
/* pretty text area */
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
private def handle_resize(): Unit = {
GUI_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = {
GUI_Thread.require {}
for {
snapshot <- PIDE.editor.current_node_snapshot(view)
if follow && !snapshot.is_outdated
} {
val (command, results) =
PIDE.editor.current_command(view, snapshot) match {
case Some(command) => (command, snapshot.command_results(command))
case None => (Command.empty, Command.Results.empty)
}
val new_output =
if (restriction.isEmpty || restriction.get.contains(command))
Rendering.output_messages(results)
else current_output
if (current_output != new_output) {
pretty_text_area.update(snapshot, results, Pretty.separate(new_output))
current_output = new_output
}
}
}
/* controls */
private def output_state: Boolean = PIDE.options.bool("editor_output_state")
private def output_state_=(b: Boolean): Unit = {
if (output_state != b) {
PIDE.options.bool("editor_output_state") = b
PIDE.session.update_options(PIDE.options.value)
PIDE.editor.flush_edits(hidden = true)
PIDE.editor.flush()
}
}
private val output_state_button = new CheckBox("Proof state") {
tooltip = "Output of proof state (normally shown on State panel)"
reactions += { case ButtonClicked(_) => output_state = selected }
selected = output_state
}
private val auto_update_button = new CheckBox("Auto update") {
tooltip = "Indicate automatic update following cursor movement"
reactions += {
case ButtonClicked(_) => do_update = this.selected; handle_update(do_update, None) }
selected = do_update
}
private val update_button = new Button("Update") {
tooltip = "Update display according to the command at cursor position"
reactions += { case ButtonClicked(_) => handle_update(true, None) }
}
- private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
List(output_state_button, auto_update_button,
update_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
/* main */
private val main =
Session.Consumer[Any](getClass.getName) {
case _: Session.Global_Options =>
GUI_Thread.later {
handle_resize()
output_state_button.selected = output_state
handle_update(do_update, None)
}
case changed: Session.Commands_Changed =>
val restriction = if (changed.assignment) None else Some(changed.commands)
GUI_Thread.later { handle_update(do_update, restriction) }
case Session.Caret_Focus =>
GUI_Thread.later { handle_update(do_update, None) }
}
override def init(): Unit = {
PIDE.session.global_options += main
PIDE.session.commands_changed += main
PIDE.session.caret_focus += main
handle_update(true, None)
}
override def exit(): Unit = {
PIDE.session.global_options -= main
PIDE.session.commands_changed -= main
PIDE.session.caret_focus -= main
delay_resize.revoke()
}
/* resize */
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
}
diff --git a/src/Tools/jEdit/src/query_dockable.scala b/src/Tools/jEdit/src/query_dockable.scala
--- a/src/Tools/jEdit/src/query_dockable.scala
+++ b/src/Tools/jEdit/src/query_dockable.scala
@@ -1,341 +1,340 @@
/* Title: Tools/jEdit/src/query_dockable.scala
Author: Makarius
Dockable window for query operations.
*/
package isabelle.jedit
import isabelle._
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
import javax.swing.{JComponent, JTextField}
import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
ComboBox, TabbedPane, BorderPanel}
import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
import org.gjt.sp.jedit.View
object Query_Dockable {
private abstract class Operation(view: View) {
val pretty_text_area = new Pretty_Text_Area(view)
def query_operation: Query_Operation[View]
def query: JComponent
def select(): Unit
def page: TabbedPane.Page
}
}
class Query_Dockable(view: View, position: String) extends Dockable(view, position) {
/* common GUI components */
- private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private def make_query(
property: String,
tooltip: String,
apply_query: () => Unit
): Completion_Popup.History_Text_Field = {
new Completion_Popup.History_Text_Field(property) {
override def processKeyEvent(evt: KeyEvent): Unit = {
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
super.processKeyEvent(evt)
}
{ val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
setColumns(40)
setToolTipText(tooltip)
setFont(GUI.imitate_font(getFont, scale = 1.2))
}
}
/* consume status */
def consume_status(
process_indicator: Process_Indicator,
status: Query_Operation.Status.Value
): Unit = {
status match {
case Query_Operation.Status.WAITING =>
process_indicator.update("Waiting for evaluation of context ...", 5)
case Query_Operation.Status.RUNNING =>
process_indicator.update("Running find operation ...", 15)
case Query_Operation.Status.FINISHED =>
process_indicator.update(null, 0)
}
}
/* find theorems */
- private val find_theorems = new Query_Dockable.Operation(view) {
+ private val find_theorems: Query_Dockable.Operation = new Query_Dockable.Operation(view) {
/* query */
private val process_indicator = new Process_Indicator
val query_operation =
new Query_Operation(PIDE.editor, view, "find_theorems",
consume_status(process_indicator, _),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
private def apply_query(): Unit = {
query.addCurrentToHistory()
query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
}
private val query_label = new Label("Find:") {
tooltip =
GUI.tooltip_lines(
"Search criteria for find operation, e.g.\n\"_ = _\" \"(+)\" name: Group -name: monoid")
}
val query: Completion_Popup.History_Text_Field =
make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
/* GUI page */
private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
tooltip = "Limit of displayed results"
- verifier = (s: String) =>
- s match { case Value.Int(x) => x >= 0 case _ => false }
+ verifier = { case Value.Int(x) => x >= 0 case _ => false }
listenTo(keys)
reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
}
private val allow_dups = new CheckBox("Duplicates") {
tooltip = "Show all versions of matching theorems"
selected = false
reactions += { case ButtonClicked(_) => apply_query() }
}
private val apply_button = new Button("Apply") {
tooltip = "Find theorems meeting specified criteria"
reactions += { case ButtonClicked(_) => apply_query() }
}
private val control_panel =
Wrap_Panel(
List(query_label, Component.wrap(query), limit, allow_dups,
process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_field))
def select(): Unit = { control_panel.contents += zoom }
val page =
new TabbedPane.Page("Find Theorems", new BorderPanel {
layout(control_panel) = BorderPanel.Position.North
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
}, apply_button.tooltip)
}
/* find consts */
- private val find_consts = new Query_Dockable.Operation(view) {
+ private val find_consts: Query_Dockable.Operation = new Query_Dockable.Operation(view) {
/* query */
private val process_indicator = new Process_Indicator
val query_operation =
new Query_Operation(PIDE.editor, view, "find_consts",
consume_status(process_indicator, _),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
private val query_label = new Label("Find:") {
tooltip = GUI.tooltip_lines("Name / type patterns for constants")
}
val query: Completion_Popup.History_Text_Field =
make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
private def apply_query(): Unit = {
query.addCurrentToHistory()
query_operation.apply_query(List(query.getText))
}
/* GUI page */
private val apply_button = new Button("Apply") {
tooltip = "Find constants by name / type patterns"
reactions += { case ButtonClicked(_) => apply_query() }
}
private val control_panel =
Wrap_Panel(
List(
query_label, Component.wrap(query), process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_field))
def select(): Unit = { control_panel.contents += zoom }
val page =
new TabbedPane.Page("Find Constants", new BorderPanel {
layout(control_panel) = BorderPanel.Position.North
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
}, apply_button.tooltip)
}
/* print operation */
private val print_operation = new Query_Dockable.Operation(view) {
/* items */
private class Item(val name: String, description: String, sel: Boolean) {
- val checkbox = new CheckBox(name) {
+ val checkbox: CheckBox = new CheckBox(name) {
tooltip = "Print " + description
selected = sel
reactions += { case ButtonClicked(_) => apply_query() }
}
}
private var _items: List[Item] = Nil
private def selected_items(): List[String] =
for (item <- _items if item.checkbox.selected) yield item.name
private def update_items(): List[Item] = {
val old_items = _items
def was_selected(name: String): Boolean =
old_items.find(item => item.name == name) match {
case None => false
case Some(item) => item.checkbox.selected
}
_items =
for ((name, description) <- Print_Operation.get(PIDE.session))
yield new Item(name, description, was_selected(name))
_items
}
/* query */
private val process_indicator = new Process_Indicator
val query_operation =
new Query_Operation(PIDE.editor, view, "print_operation",
consume_status(process_indicator, _),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
private def apply_query(): Unit =
query_operation.apply_query(selected_items())
private val query_label = new Label("Print:")
def query: JComponent = apply_button.peer
update_items()
/* GUI page */
private val apply_button = new Button("Apply") {
tooltip = "Apply to current context"
listenTo(keys)
reactions += {
case ButtonClicked(_) => apply_query()
case evt @ KeyPressed(_, Key.Enter, 0, _) =>
evt.peer.consume()
apply_query()
}
}
private val control_panel = Wrap_Panel()
def select(): Unit = {
control_panel.contents.clear()
control_panel.contents += query_label
update_items().foreach(item => control_panel.contents += item.checkbox)
control_panel.contents ++=
List(process_indicator.component, apply_button,
pretty_text_area.search_label, pretty_text_area.search_field, zoom)
}
val page =
new TabbedPane.Page("Print Context", new BorderPanel {
layout(control_panel) = BorderPanel.Position.North
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
}, "Print information from context")
}
/* operations */
private val operations = List(find_theorems, find_consts, print_operation)
private val operations_pane = new TabbedPane {
pages ++= operations.map(_.page)
listenTo(selection)
reactions += { case SelectionChanged(_) => select_operation() }
}
private def get_operation(): Option[Query_Dockable.Operation] =
try { Some(operations(operations_pane.selection.index)) }
catch { case _: IndexOutOfBoundsException => None }
private def select_operation(): Unit = {
for (op <- get_operation()) { op.select(); op.query.requestFocus() }
operations_pane.revalidate()
}
override def focusOnDefaultComponent(): Unit = {
for (op <- get_operation()) op.query.requestFocus()
}
select_operation()
set_content(operations_pane)
override def detach_operation: Option[() => Unit] =
get_operation() match {
case None => None
case Some(op) => op.pretty_text_area.detach_operation
}
/* resize */
private def handle_resize(): Unit =
GUI_Thread.require {
for (op <- operations) {
op.pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
}
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
/* main */
private val main =
Session.Consumer[Session.Global_Options](getClass.getName) {
case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
}
override def init(): Unit = {
PIDE.session.global_options += main
handle_resize()
operations.foreach(op => op.query_operation.activate())
}
override def exit(): Unit = {
operations.foreach(op => op.query_operation.deactivate())
PIDE.session.global_options -= main
delay_resize.revoke()
}
}
diff --git a/src/Tools/jEdit/src/simplifier_trace_window.scala b/src/Tools/jEdit/src/simplifier_trace_window.scala
--- a/src/Tools/jEdit/src/simplifier_trace_window.scala
+++ b/src/Tools/jEdit/src/simplifier_trace_window.scala
@@ -1,188 +1,188 @@
/* Title: Tools/jEdit/src/simplifier_trace_window.scala
Author: Lars Hupel
Trace window with tree-style view of the simplifier trace.
*/
package isabelle.jedit
import isabelle._
import scala.annotation.tailrec
import scala.collection.immutable.SortedMap
import scala.swing.{BorderPanel, CheckBox, Component, Dimension, Frame, Label, TextField}
import scala.swing.event.{Key, KeyPressed}
import scala.util.matching.Regex
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
import javax.swing.SwingUtilities
import org.gjt.sp.jedit.View
private object Simplifier_Trace_Window {
sealed trait Trace_Tree {
// FIXME replace with immutable tree builder
var children: SortedMap[Long, Either[Simplifier_Trace.Item.Data, Elem_Tree]] = SortedMap.empty
val serial: Long
val parent: Option[Trace_Tree]
val markup: String
def interesting: Boolean
def tree_children: List[Elem_Tree] = children.values.toList.collect {
case Right(tree) => tree
}
}
final class Root_Tree(val serial: Long) extends Trace_Tree {
val parent = None
val interesting = true
val markup = ""
def format: XML.Body =
Pretty.separate(tree_children.flatMap(_.format))
}
final class Elem_Tree(data: Simplifier_Trace.Item.Data, val parent: Option[Trace_Tree])
extends Trace_Tree {
val serial = data.serial
val markup = data.markup
lazy val interesting: Boolean =
data.markup == Markup.SIMP_TRACE_STEP ||
data.markup == Markup.SIMP_TRACE_LOG ||
tree_children.exists(_.interesting)
private def body_contains(regex: Regex, body: XML.Body): Boolean =
body.exists(tree => regex.findFirstIn(XML.content(tree)).isDefined)
def format: Option[XML.Tree] = {
def format_hint(data: Simplifier_Trace.Item.Data): XML.Tree =
Pretty.block(Pretty.separate(XML.Text(data.text) :: data.content))
lazy val bodies: XML.Body =
children.values.toList.collect {
case Left(data) => Some(format_hint(data))
case Right(tree) if tree.interesting => tree.format
}.flatten.map(item =>
XML.Elem(Markup(Markup.ITEM, Nil), List(item))
)
val all = XML.Text(data.text) :: data.content ::: bodies
val res = XML.Elem(Markup(Markup.TEXT_FOLD, Nil), List(Pretty.block(Pretty.separate(all))))
if (bodies != Nil)
Some(res)
else
None
}
}
@tailrec
def walk_trace(rest: List[Simplifier_Trace.Item.Data], lookup: Map[Long, Trace_Tree]): Unit =
rest match {
case Nil =>
()
case head :: tail =>
lookup.get(head.parent) match {
case Some(parent) =>
if (head.markup == Markup.SIMP_TRACE_HINT) {
head.props match {
case Simplifier_Trace.Success(x)
if x ||
parent.markup == Markup.SIMP_TRACE_LOG ||
parent.markup == Markup.SIMP_TRACE_STEP =>
parent.children += ((head.serial, Left(head)))
case _ =>
// ignore
}
walk_trace(tail, lookup)
}
else if (head.markup == Markup.SIMP_TRACE_IGNORE) {
parent.parent match {
case None =>
Output.error_message(
"Simplifier_Trace_Window: malformed ignore message with parent " + head.parent)
case Some(tree) =>
tree.children -= head.parent
walk_trace(tail, lookup)
}
}
else {
val entry = new Elem_Tree(head, Some(parent))
parent.children += ((head.serial, Right(entry)))
walk_trace(tail, lookup + (head.serial -> entry))
}
case None =>
Output.error_message("Simplifier_Trace_Window: unknown parent " + head.parent)
}
}
}
class Simplifier_Trace_Window(
view: View,
snapshot: Document.Snapshot,
trace: Simplifier_Trace.Trace
) extends Frame {
GUI_Thread.require {}
private val pretty_text_area = new Pretty_Text_Area(view)
- private val zoom = new Font_Info.Zoom_Box { def changed() = do_paint() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = do_paint() }
size = new Dimension(500, 500)
contents = new BorderPanel {
layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
}
private val tree = trace.entries.headOption match {
case Some(first) =>
val tree = new Simplifier_Trace_Window.Root_Tree(first.parent)
Simplifier_Trace_Window.walk_trace(trace.entries, Map(first.parent -> tree))
tree
case None =>
new Simplifier_Trace_Window.Root_Tree(0)
}
do_update()
open()
do_paint()
def do_update(): Unit = {
val xml = tree.format
pretty_text_area.update(snapshot, Command.Results.empty, xml)
}
def do_paint(): Unit = {
GUI_Thread.later {
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
}
def handle_resize(): Unit = do_paint()
/* resize */
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
peer.addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
/* controls */
private val controls =
Wrap_Panel(List(pretty_text_area.search_label, pretty_text_area.search_field, zoom))
peer.add(controls.peer, BorderLayout.NORTH)
}
diff --git a/src/Tools/jEdit/src/sledgehammer_dockable.scala b/src/Tools/jEdit/src/sledgehammer_dockable.scala
--- a/src/Tools/jEdit/src/sledgehammer_dockable.scala
+++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala
@@ -1,163 +1,163 @@
/* Title: Tools/jEdit/src/sledgehammer_dockable.scala
Author: Makarius
Dockable window for Sledgehammer.
*/
package isabelle.jedit
import isabelle._
import scala.swing.{Button, Component, Label, CheckBox}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
import org.gjt.sp.jedit.View
import org.gjt.sp.jedit.gui.HistoryTextField
class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position) {
GUI_Thread.require {}
/* text area */
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
/* query operation */
private val process_indicator = new Process_Indicator
private def consume_status(status: Query_Operation.Status.Value): Unit = {
status match {
case Query_Operation.Status.WAITING =>
process_indicator.update("Waiting for evaluation of context ...", 5)
case Query_Operation.Status.RUNNING =>
process_indicator.update("Sledgehammering ...", 15)
case Query_Operation.Status.FINISHED =>
process_indicator.update(null, 0)
}
}
private val sledgehammer =
new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status,
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
/* resize */
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
private def handle_resize(): Unit = {
GUI_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
/* controls */
private def clicked: Unit = {
provers.addCurrentToHistory()
PIDE.options.string("sledgehammer_provers") = provers.getText
sledgehammer.apply_query(
List(provers.getText, isar_proofs.selected.toString, try0.selected.toString))
}
private val provers_label = new Label("Provers:") {
tooltip =
GUI.tooltip_lines(
"Automatic provers as space-separated list, e.g.\n" +
PIDE.options.value.check_name("sledgehammer_provers").default_value)
}
private val provers = new HistoryTextField("isabelle-sledgehammer-provers") {
override def processKeyEvent(evt: KeyEvent): Unit = {
if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
super.processKeyEvent(evt)
}
setToolTipText(provers_label.tooltip)
setColumns(30)
}
private def update_provers(): Unit = {
val new_provers = PIDE.options.string("sledgehammer_provers")
if (new_provers != provers.getText) {
provers.setText(new_provers)
if (provers.getCaret != null)
provers.getCaret.setDot(0)
}
}
private val isar_proofs = new CheckBox("Isar proofs") {
tooltip = "Specify whether Isar proofs should be output in addition to \"by\" one-liner"
selected = false
}
private val try0 = new CheckBox("Try methods") {
tooltip = "Try standard proof methods like \"auto\" and \"blast\" as alternatives to \"metis\""
selected = true
}
private val apply_query = new Button("Apply") {
tooltip = "Search for first-order proof using automatic theorem provers"
reactions += { case ButtonClicked(_) => clicked }
}
private val cancel_query = new Button("Cancel") {
tooltip = "Interrupt unfinished sledgehammering"
reactions += { case ButtonClicked(_) => sledgehammer.cancel_query() }
}
private val locate_query = new Button("Locate") {
tooltip = "Locate context of current query within source text"
reactions += { case ButtonClicked(_) => sledgehammer.locate_query() }
}
- private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
List(provers_label, Component.wrap(provers), isar_proofs, try0,
process_indicator.component, apply_query, cancel_query, locate_query, zoom))
add(controls.peer, BorderLayout.NORTH)
override def focusOnDefaultComponent(): Unit = provers.requestFocus()
/* main */
private val main =
Session.Consumer[Session.Global_Options](getClass.getName) {
case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() }
}
override def init(): Unit = {
PIDE.session.global_options += main
update_provers()
handle_resize()
sledgehammer.activate()
}
override def exit(): Unit = {
sledgehammer.deactivate()
PIDE.session.global_options -= main
delay_resize.revoke()
}
}
diff --git a/src/Tools/jEdit/src/state_dockable.scala b/src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala
+++ b/src/Tools/jEdit/src/state_dockable.scala
@@ -1,141 +1,141 @@
/* Title: Tools/jEdit/src/state_dockable.scala
Author: Makarius
Dockable window for proof state output.
*/
package isabelle.jedit
import isabelle._
import scala.swing.{Button, CheckBox}
import scala.swing.event.ButtonClicked
import java.awt.BorderLayout
import java.awt.event.{ComponentEvent, ComponentAdapter}
import org.gjt.sp.jedit.View
class State_Dockable(view: View, position: String) extends Dockable(view, position) {
GUI_Thread.require {}
/* text area */
val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation
private val print_state =
new Query_Operation(PIDE.editor, view, "print_state", _ => (),
(snapshot, results, body) =>
pretty_text_area.update(snapshot, results, Pretty.separate(body)))
/* resize */
private val delay_resize =
Delay.first(PIDE.options.seconds("editor_update_delay"), gui = true) { handle_resize() }
addComponentListener(new ComponentAdapter {
override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
})
private def handle_resize(): Unit = {
GUI_Thread.require {}
pretty_text_area.resize(
Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
}
/* update */
def update_request(): Unit =
GUI_Thread.require { print_state.apply_query(Nil) }
def update(): Unit = {
GUI_Thread.require {}
PIDE.editor.current_node_snapshot(view) match {
case Some(snapshot) =>
(PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
case (Some(command1), Some(command2)) if command1.id == command2.id =>
case _ => update_request()
}
case None =>
}
}
/* auto update */
private var auto_update_enabled = true
private def auto_update(): Unit =
GUI_Thread.require { if (auto_update_enabled) update() }
/* controls */
private val auto_update_button = new CheckBox("Auto update") {
tooltip = "Indicate automatic update following cursor movement"
reactions += { case ButtonClicked(_) => auto_update_enabled = this.selected; auto_update() }
selected = auto_update_enabled
}
private val update_button = new Button("Update") {
tooltip = "Update display according to the command at cursor position"
reactions += { case ButtonClicked(_) => update_request() }
}
private val locate_button = new Button("Locate") {
tooltip = "Locate printed command within source text"
reactions += { case ButtonClicked(_) => print_state.locate_query() }
}
- private val zoom = new Font_Info.Zoom_Box { def changed() = handle_resize() }
+ private val zoom = new Font_Info.Zoom_Box { def changed(): Unit = handle_resize() }
private val controls =
Wrap_Panel(
List(auto_update_button, update_button,
locate_button, pretty_text_area.search_label, pretty_text_area.search_field, zoom))
add(controls.peer, BorderLayout.NORTH)
/* main */
private val main =
Session.Consumer[Any](getClass.getName) {
case _: Session.Global_Options =>
GUI_Thread.later { handle_resize() }
case changed: Session.Commands_Changed =>
if (changed.assignment) GUI_Thread.later { auto_update() }
case Session.Caret_Focus =>
GUI_Thread.later { auto_update() }
}
override def init(): Unit = {
PIDE.session.global_options += main
PIDE.session.commands_changed += main
PIDE.session.caret_focus += main
handle_resize()
print_state.activate()
auto_update()
}
override def exit(): Unit = {
print_state.deactivate()
PIDE.session.caret_focus -= main
PIDE.session.global_options -= main
PIDE.session.commands_changed -= main
delay_resize.revoke()
}
}