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() } }