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,350 @@
/* 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_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
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(): 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,115 @@
/* 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(): 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))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
/* 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,148 @@
/* 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_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
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(): 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/pretty_text_area.scala b/src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala
+++ b/src/Tools/jEdit/src/pretty_text_area.scala
@@ -1,240 +1,243 @@
/* Title: Tools/jEdit/src/pretty_text_area.scala
Author: Makarius
GUI component for pretty-printed text with markup, rendered like jEdit
text area.
*/
package isabelle.jedit
import isabelle._
import java.awt.{Color, Font, Toolkit, Window}
import java.awt.event.{InputEvent, KeyEvent}
import java.awt.im.InputMethodRequests
import javax.swing.JTextField
import javax.swing.event.{DocumentListener, DocumentEvent}
import scala.swing.{Label, Component}
import scala.util.matching.Regex
import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction}
import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler}
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
import org.gjt.sp.jedit.syntax.SyntaxStyle
import org.gjt.sp.jedit.gui.KeyEventTranslator
import org.gjt.sp.util.{SyntaxUtilities, Log}
class Pretty_Text_Area(
view: View,
close_action: () => Unit = () => (),
propagate_keys: Boolean = false
) extends JEditEmbeddedTextArea {
text_area =>
GUI_Thread.require {}
private var current_font_info: Font_Info = Font_Info.main()
private var current_body: XML.Body = Nil
private var current_base_snapshot = Document.Snapshot.init
private var current_base_results = Command.Results.empty
private var current_rendering: JEdit_Rendering =
JEdit_Rendering.text(current_base_snapshot, Nil)._2
private var future_refresh: Option[Future[Unit]] = None
private val rich_text_area =
new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
get_search_pattern _, () => (), caret_visible = false, enable_hovering = true)
private var current_search_pattern: Option[Regex] = None
def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_pattern }
def get_background(): Option[Color] = None
def refresh(): Unit = {
GUI_Thread.require {}
val font = current_font_info.font
getPainter.setFont(font)
getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
getPainter.setFractionalFontMetricsEnabled(jEdit.getBooleanProperty("view.fracFontMetrics"))
getPainter.setStyles(
SyntaxUtilities.loadStyles(current_font_info.family, current_font_info.size.round))
getPainter.setLineExtraSpacing(jEdit.getIntegerProperty("options.textarea.lineSpacing", 0))
val fold_line_style = new Array[SyntaxStyle](4)
for (i <- 0 to 3) {
fold_line_style(i) =
SyntaxUtilities.parseStyle(
jEdit.getProperty("view.style.foldLine." + i),
current_font_info.family, current_font_info.size.round, true)
}
getPainter.setFoldLineStyle(fold_line_style)
getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
get_background().foreach { bg => getPainter.setBackground(bg); getGutter.setBackground(bg) }
getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
getGutter.setBorder(0,
jEdit.getColorProperty("view.gutter.focusBorderColor"),
jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
getPainter.getBackground)
getGutter.setFoldPainter(view.getTextArea.getFoldPainter)
getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
if (getWidth > 0) {
val metric = JEdit_Lib.pretty_metric(getPainter)
val margin = ((getPainter.getWidth.toDouble / metric.unit) max 20.0).floor
val snapshot = current_base_snapshot
val results = current_base_results
val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric)
future_refresh.foreach(_.cancel())
future_refresh =
Some(Future.fork {
val (text, rendering) =
try { JEdit_Rendering.text(snapshot, formatted_body, results = results) }
catch { case exn: Throwable => Log.log(Log.ERROR, this, exn); throw exn }
Exn.Interrupt.expose()
GUI_Thread.later {
current_rendering = rendering
JEdit_Lib.buffer_edit(getBuffer) {
rich_text_area.active_reset()
getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
JEdit_Lib.buffer_undo_in_progress(getBuffer, setText(text))
setCaretPosition(0)
}
}
})
}
}
def resize(font_info: Font_Info): Unit = {
GUI_Thread.require {}
current_font_info = font_info
refresh()
}
+ def zoom(factor: Int): Unit =
+ resize(Font_Info.main(PIDE.options.real("jedit_font_scale") * factor / 100))
+
def update(
base_snapshot: Document.Snapshot,
base_results: Command.Results,
body: XML.Body
): Unit = {
GUI_Thread.require {}
require(!base_snapshot.is_outdated, "document snapshot outdated")
current_base_snapshot = base_snapshot
current_base_results = base_results
current_body = body
refresh()
}
def detach(): Unit = {
GUI_Thread.require {}
Info_Dockable(view, current_base_snapshot, current_base_results, current_body)
}
def detach_operation: Option[() => Unit] =
if (current_body.isEmpty) None else Some(() => detach())
/* common GUI components */
val search_label: Component = new Label("Search:") {
tooltip = "Search and highlight output via regular expression"
}
val search_field: Component =
Component.wrap(new Completion_Popup.History_Text_Field("isabelle-search") {
private val input_delay =
Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) {
search_action(this)
}
getDocument.addDocumentListener(new DocumentListener {
def changedUpdate(e: DocumentEvent): Unit = input_delay.invoke()
def insertUpdate(e: DocumentEvent): Unit = input_delay.invoke()
def removeUpdate(e: DocumentEvent): Unit = input_delay.invoke()
})
setColumns(20)
setToolTipText(search_label.tooltip)
setFont(GUI.imitate_font(getFont, scale = 1.2))
})
private val search_field_foreground = search_field.foreground
private def search_action(text_field: JTextField): Unit = {
val (pattern, ok) =
text_field.getText match {
case null | "" => (None, true)
case s =>
val re = Library.make_regex(s)
(re, re.isDefined)
}
if (current_search_pattern != pattern) {
current_search_pattern = pattern
text_area.getPainter.repaint()
}
text_field.setForeground(
if (ok) search_field_foreground
else current_rendering.color(Rendering.Color.error))
}
/* key handling */
override def getInputMethodRequests: InputMethodRequests = null
inputHandlerProvider =
new DefaultInputHandlerProvider(new TextAreaInputHandler(text_area) {
override def getAction(action: String): JEditBeanShellAction =
text_area.getActionContext.getAction(action)
override def processKeyEvent(evt: KeyEvent, from: Int, global: Boolean): Unit = {}
override def handleKey(key: KeyEventTranslator.Key, dry_run: Boolean): Boolean = false
})
addKeyListener(JEdit_Lib.key_listener(
key_pressed = { (evt: KeyEvent) =>
val strict_control =
JEdit_Lib.command_modifier(evt) && !JEdit_Lib.shift_modifier(evt)
evt.getKeyCode match {
case KeyEvent.VK_C | KeyEvent.VK_INSERT
if strict_control && text_area.getSelectionCount != 0 =>
Registers.copy(text_area, '$')
evt.consume()
case KeyEvent.VK_A
if strict_control =>
text_area.selectAll
evt.consume()
case KeyEvent.VK_ESCAPE =>
if (Isabelle.dismissed_popups(view)) evt.consume()
case _ =>
}
if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
},
key_typed = { (evt: KeyEvent) =>
if (propagate_keys) JEdit_Lib.propagate_key(view, evt)
})
)
/* init */
getPainter.setStructureHighlightEnabled(false)
getPainter.setLineHighlightEnabled(false)
getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
getBuffer.setStringProperty("noWordSep", "_'?⇩")
rich_text_area.activate()
}
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,340 +1,335 @@
/* 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(): 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: 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 = { 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: 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: 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))
- }
- }
+ GUI_Thread.require { operations.foreach(_.pretty_text_area.zoom(zoom.factor)) }
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,184 @@
/* 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(): 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 do_paint(): Unit =
+ GUI_Thread.later { pretty_text_area.zoom(zoom.factor) }
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,159 @@
/* 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))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
/* 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(): 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,137 @@
/* 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))
- }
+ private def handle_resize(): Unit =
+ GUI_Thread.require { pretty_text_area.zoom(zoom.factor) }
/* 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(): 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()
}
}