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