# HG changeset patch # User wenzelm # Date 1732303296 -3600 # Node ID 60696404b40a29d6011ecc6a1b5afc3a21740ee8 # Parent 53e61087bc6f4f5b3bd568fa58d67c508bbe2c0e# Parent d421a7c58530e71c15bd143bd114d7fcaffdc1f0 merged diff -r 53e61087bc6f -r 60696404b40a NEWS --- a/NEWS Fri Nov 22 16:05:42 2024 +0000 +++ b/NEWS Fri Nov 22 20:21:36 2024 +0100 @@ -139,6 +139,8 @@ - Highlighting works via mouse hovering alone, without requiring C-modifier. + - Search results are shown as tree view. + * An active highlight area in the input buffer or output panel may be turned into a text selection by using the ALT modifier. diff -r 53e61087bc6f -r 60696404b40a src/Pure/GUI/tree_view.scala --- a/src/Pure/GUI/tree_view.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Pure/GUI/tree_view.scala Fri Nov 22 20:21:36 2024 +0100 @@ -8,7 +8,7 @@ import javax.swing.JTree import javax.swing.tree.{MutableTreeNode, DefaultMutableTreeNode, DefaultTreeModel, - TreeSelectionModel} + TreeSelectionModel, TreeCellRenderer, DefaultTreeCellRenderer} object Tree_View { @@ -24,6 +24,24 @@ case _ => None } } + + class Cell_Renderer extends DefaultTreeCellRenderer { + def setup(value: AnyRef): Unit = setIcon(null) + + override def getTreeCellRendererComponent( + tree: JTree, + value: AnyRef, + selected: Boolean, + expanded: Boolean, + leaf: Boolean, + row: Int, + hasFocus: Boolean + ): java.awt.Component = { + super.getTreeCellRendererComponent(tree, value, selected, expanded, leaf, row, hasFocus) + setup(value) + this + } + } } class Tree_View( @@ -36,9 +54,12 @@ case _ => None } - def clear(): Unit = { + def init_model(body: => Unit): Unit = { clearSelection() root.removeAllChildren() + body + expandRow(0) + reload_model() } def reload_model(): Unit = @@ -50,6 +71,8 @@ /* init */ + setCellRenderer(new Tree_View.Cell_Renderer) + setRowHeight(0) if (single_selection_mode) { diff -r 53e61087bc6f -r 60696404b40a src/Tools/Graphview/tree_panel.scala --- a/src/Tools/Graphview/tree_panel.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/Graphview/tree_panel.scala Fri Nov 22 20:21:36 2024 +0100 @@ -12,7 +12,7 @@ import java.awt.{Dimension, Rectangle} import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter} import javax.swing.tree.TreePath -import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent} +import javax.swing.event.{DocumentListener, DocumentEvent} import scala.util.matching.Regex import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, Action} @@ -140,14 +140,9 @@ def refresh(): Unit = { val new_nodes = graphview.visible_graph.topological_order - if (new_nodes != nodes) { - tree.clear() - + if (nodes != new_nodes) { nodes = new_nodes - for (node <- nodes) tree.root.add(Tree_View.Node(node)) - - tree.expandRow(0) - tree.revalidate() + tree.init_model { for (node <- nodes) tree.root.add(Tree_View.Node(node)) } } revalidate() repaint() diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Fri Nov 22 20:21:36 2024 +0100 @@ -64,10 +64,17 @@ private var current_output: List[XML.Tree] = Nil - /* pretty text area */ + /* output area */ private val output: Output_Area = new Output_Area(view, root_name = "Threads") { + override def handle_search(search: Pretty_Text_Area.Search_Results): Unit = {} + + override def handle_tree_selection(e: TreeSelectionEvent): Unit = { + update_focus() + update_vals() + } + override def handle_update(): Unit = { val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) val (new_threads, new_output) = debugger.status(tree_selection()) @@ -89,7 +96,8 @@ override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation - output.init_gui(dockable, split = true) + output.setup(dockable) + set_content(output.split_pane) /* tree view */ @@ -112,18 +120,16 @@ case _ => thread_contexts.headOption } - output.tree.clear() - - for (thread <- thread_contexts) { - val thread_node = Tree_View.Node(thread) - for ((_, i) <- thread.debug_states.zipWithIndex) - thread_node.add(Tree_View.Node(thread.select(i))) - output.tree.root.add(thread_node) + output.tree.init_model { + for (thread <- thread_contexts) { + val thread_node = Tree_View.Node(thread) + for ((_, i) <- thread.debug_states.zipWithIndex) { + thread_node.add(Tree_View.Node(thread.select(i))) + } + output.tree.root.add(thread_node) + } } - output.tree.reload_model() - - output.tree.expandRow(0) for (i <- Range.inclusive(output.tree.getRowCount - 1, 1, -1)) output.tree.expandRow(i) new_tree_selection match { @@ -255,11 +261,6 @@ JEdit_Lib.jedit_text_areas(view.getBuffer).foreach(_.repaint()) } - output.tree.addTreeSelectionListener({ (e: TreeSelectionEvent) => - update_focus() - update_vals() - }) - /* main */ @@ -279,14 +280,14 @@ PIDE.session.global_options += main PIDE.session.debugger_updates += main debugger.init(dockable) - output.handle_update() + output.init() jEdit.propertiesChanged() } override def exit(): Unit = { PIDE.session.global_options -= main PIDE.session.debugger_updates -= main - output.delay_resize.revoke() + output.exit() debugger.exit(dockable) jEdit.propertiesChanged() } diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/document_dockable.scala --- a/src/Tools/jEdit/src/document_dockable.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/document_dockable.scala Fri Nov 22 20:21:36 2024 +0100 @@ -65,13 +65,16 @@ private val current_state = Synchronized(Document_Dockable.State.init()) private val process_indicator = new Process_Indicator - private val pretty_text_area = new Pretty_Text_Area(view) + private val output: Output_Area = new Output_Area(view) private val message_pane = new TabbedPane + override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation + + private def show_state(): Unit = GUI_Thread.later { val st = current_state.value - pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all) + output.pretty_text_area.update(Document.Snapshot.init, st.output_results, st.output_all) if (st.running) process_indicator.update("Running document build process ...", 15) else if (st.pending) process_indicator.update("Waiting for pending document content ...", 5) @@ -84,21 +87,6 @@ } - /* text area with zoom/resize */ - - override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation - - private def handle_resize(): Unit = pretty_text_area.zoom() - - private val delay_resize: Delay = - Delay.first(PIDE.session.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() - }) - - /* progress */ class Log_Progress extends Program_Progress(default_title = "build") { @@ -348,16 +336,18 @@ override def clicked(): Unit = cancel_process() } - private val output_controls = Wrap_Panel(List(cancel_button, pretty_text_area.zoom_component)) + private val output_controls = + Wrap_Panel(List(cancel_button, output.pretty_text_area.zoom_component)) private val output_page = new TabbedPane.Page("Output", new BorderPanel { layout(output_controls) = BorderPanel.Position.North - layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center + layout(output.text_pane) = BorderPanel.Position.Center }, "Results from document build process") message_pane.pages ++= List(input_page, output_page) + output.setup(dockable) set_content(message_pane) @@ -368,7 +358,7 @@ case _: Session.Global_Options => GUI_Thread.later { document_session.load() - handle_resize() + output.handle_resize() refresh_theories() } case changed: Session.Commands_Changed => @@ -397,14 +387,14 @@ init_state() PIDE.session.global_options += main PIDE.session.commands_changed += main - handle_resize() + output.init() delay_load.invoke() } override def exit(): Unit = { PIDE.session.global_options -= main PIDE.session.commands_changed -= main - delay_resize.revoke() + output.exit() PIDE.editor.document_exit(dockable) } } diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/info_dockable.scala --- a/src/Tools/jEdit/src/info_dockable.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/info_dockable.scala Fri Nov 22 20:21:36 2024 +0100 @@ -50,6 +50,9 @@ class Info_Dockable(view: View, position: String) extends Dockable(view, position) { + dockable => + + /* component state -- owned by GUI thread */ private val snapshot = Info_Dockable.implicit_snapshot @@ -65,47 +68,34 @@ } - /* pretty text area */ - - private val pretty_text_area = new Pretty_Text_Area(view) - set_content(pretty_text_area) + /* output text area */ - pretty_text_area.update(snapshot, results, info) - - private def handle_resize(): Unit = pretty_text_area.zoom() - - - /* resize */ + private val output: Output_Area = new Output_Area(view) + output.pretty_text_area.update(snapshot, results, info) - private val delay_resize = - Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } + private val controls = Wrap_Panel(output.pretty_text_area.search_zoom_components) + add(controls.peer, BorderLayout.NORTH) - 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(pretty_text_area.search_zoom_components) - - add(controls.peer, BorderLayout.NORTH) + output.setup(dockable) + set_content(output.split_pane) /* main */ private val main = Session.Consumer[Session.Global_Options](getClass.getName) { - case _: Session.Global_Options => GUI_Thread.later { handle_resize() } + case _: Session.Global_Options => GUI_Thread.later { output.handle_resize() } } override def init(): Unit = { GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener)) PIDE.session.global_options += main - handle_resize() + output.init() } override def exit(): Unit = { GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener)) PIDE.session.global_options -= main - delay_resize.revoke() + output.exit() } } diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/jedit_lib.scala --- a/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/jedit_lib.scala Fri Nov 22 20:21:36 2024 +0100 @@ -144,6 +144,10 @@ try { Some(buffer.getText(range.start, range.length)) } catch { case _: ArrayIndexOutOfBoundsException => None } + def can_search_text(buffer: JEditBuffer, range: Text.Range, regex: Regex): Boolean = + try { regex.findFirstIn(buffer.getSegment(range.start, range.length)).nonEmpty } + catch { case _: ArrayIndexOutOfBoundsException => false } + def search_text(buffer: JEditBuffer, range: Text.Range, regex: Regex): List[Text.Range] = List.from( for { @@ -335,26 +339,23 @@ { (range: Text.Range) => val stop = range.stop + try { + val p = text_area.offsetToXY(range.start) + val (q, r) = + if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) { + (text_area.offsetToXY(stop - 1), char_width) + } + else if (stop >= end) { + (text_area.offsetToXY(end), char_width * (stop - end)) + } + else (text_area.offsetToXY(stop), 0) - val (p, q, r) = - try { - val p = text_area.offsetToXY(range.start) - val (q, r) = - if (get_text(buffer, Text.Range(stop - 1, stop)).contains("\n")) { - (text_area.offsetToXY(stop - 1), char_width) - } - else if (stop >= end) { - (text_area.offsetToXY(end), char_width * (stop - end)) - } - else (text_area.offsetToXY(stop), 0) - (p, q, r) + if (p != null && q != null && p.x < q.x + r && p.y == q.y) { + Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) } - catch { case _: ArrayIndexOutOfBoundsException => (null, null, 0) } - - if (p != null && q != null && p.x < q.x + r && p.y == q.y) { - Some(Gfx_Range(p.x, p.y, q.x + r - p.x)) + else None } - else None + catch { case _: ArrayIndexOutOfBoundsException => None } } } diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/output_area.scala --- a/src/Tools/jEdit/src/output_area.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/output_area.scala Fri Nov 22 20:21:36 2024 +0100 @@ -13,26 +13,47 @@ import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent, MouseEvent, MouseAdapter} import javax.swing.JComponent +import javax.swing.event.{TreeSelectionListener, TreeSelectionEvent} +import scala.util.matching.Regex import scala.swing.{Component, ScrollPane, SplitPane, Orientation} import scala.swing.event.ButtonClicked import org.gjt.sp.jedit.View -class Output_Area(view: View, root_name: String = "Overview") { +class Output_Area(view: View, root_name: String = "Search results") { + output_area => + GUI_Thread.require {} /* tree view */ + val tree_cell_renderer: Tree_View.Cell_Renderer = new Tree_View.Cell_Renderer + val tree: Tree_View = new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true) + def handle_search(search: Pretty_Text_Area.Search_Results): Unit = { + tree.init_model { for (result <- search.results) tree.root.add(Tree_View.Node(result)) } + tree.revalidate() + } + + def handle_tree_selection(e: TreeSelectionEvent): Unit = + for (result <- tree.get_selection({ case x: Pretty_Text_Area.Search_Result => x })) { + pretty_text_area.setCaretPosition(result.line_range.start) + JEdit_Lib.scroll_to_caret(pretty_text_area) + } + /* text area */ - val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view) + val pretty_text_area: Pretty_Text_Area = + new Pretty_Text_Area(view) { + override def handle_search(search: Pretty_Text_Area.Search_Results): Unit = + output_area.handle_search(search) + } def handle_resize(): Unit = pretty_text_area.zoom() def handle_update(): Unit = () @@ -69,6 +90,11 @@ } } + private lazy val tree_selection_listener = + new TreeSelectionListener { + def valueChanged(e: TreeSelectionEvent): Unit = handle_tree_selection(e) + } + /* GUI components */ @@ -89,13 +115,18 @@ rightComponent = text_pane } - def init_gui(parent: JComponent, split: Boolean = false): Unit = { + def setup(parent: JComponent): Unit = { parent.addComponentListener(component_listener) parent.addFocusListener(focus_listener) tree.addMouseListener(mouse_listener) - parent match { - case dockable: Dockable => dockable.set_content(if (split) split_pane else text_pane) - case _ => - } + tree.addTreeSelectionListener(tree_selection_listener) + tree.setCellRenderer(tree_cell_renderer) } + + def init(): Unit = { + handle_update() + handle_resize() + } + + def exit(): Unit = delay_resize.revoke() } diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/output_dockable.scala --- a/src/Tools/jEdit/src/output_dockable.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/output_dockable.scala Fri Nov 22 20:21:36 2024 +0100 @@ -16,23 +16,24 @@ class Output_Dockable(view: View, position: String) extends Dockable(view, position) { + dockable => + + /* component state -- owned by GUI thread */ private var do_update = true private var current_output: List[XML.Elem] = Nil - /* pretty text area */ + /* output area */ - val pretty_text_area = new Pretty_Text_Area(view) - set_content(pretty_text_area) + private val output: Output_Area = + new Output_Area(view) { override def handle_update(): Unit = dockable.handle_update(true) } - override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation - + override def detach_operation: Option[() => Unit] = + output.pretty_text_area.detach_operation - private def handle_resize(): Unit = pretty_text_area.zoom() - - private def handle_update(follow: Boolean, restriction: Option[Set[Command]]): Unit = { + private def handle_update(follow: Boolean, restriction: Option[Set[Command]] = None): Unit = { GUI_Thread.require {} for { @@ -51,12 +52,15 @@ else current_output if (current_output != new_output) { - pretty_text_area.update(snapshot, results, new_output) + output.pretty_text_area.update(snapshot, results, new_output) current_output = new_output } } } + output.setup(dockable) + dockable.set_content(output.split_pane) + /* controls */ @@ -68,19 +72,19 @@ tooltip = "Indicate automatic update following cursor movement" override def clicked(state: Boolean): Unit = { do_update = state - handle_update(do_update, None) + handle_update(do_update) } } private val update_button = new GUI.Button("Update") { tooltip = "Update display according to the command at cursor position" - override def clicked(): Unit = handle_update(true, None) + override def clicked(): Unit = handle_update(true) } private val controls = Wrap_Panel( List(output_state_button, auto_hovering_button, auto_update_button, update_button) ::: - pretty_text_area.search_zoom_components) + output.pretty_text_area.search_zoom_components) add(controls.peer, BorderLayout.NORTH) @@ -91,42 +95,31 @@ Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => GUI_Thread.later { - handle_resize() + output.handle_resize() output_state_button.load() auto_hovering_button.load() - handle_update(do_update, None) + handle_update(do_update) } case changed: Session.Commands_Changed => val restriction = if (changed.assignment) None else Some(changed.commands) - GUI_Thread.later { handle_update(do_update, restriction) } + GUI_Thread.later { handle_update(do_update, restriction = restriction) } case Session.Caret_Focus => - GUI_Thread.later { handle_update(do_update, None) } + GUI_Thread.later { handle_update(do_update) } } override def init(): Unit = { PIDE.session.global_options += main PIDE.session.commands_changed += main PIDE.session.caret_focus += main - handle_update(true, None) + output.init() } override def exit(): Unit = { PIDE.session.global_options -= main PIDE.session.commands_changed -= main PIDE.session.caret_focus -= main - delay_resize.revoke() + output.exit() } - - - /* resize */ - - private val delay_resize = - Delay.first(PIDE.session.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 -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/pretty_text_area.scala --- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/pretty_text_area.scala Fri Nov 22 20:21:36 2024 +0100 @@ -20,12 +20,85 @@ import scala.util.matching.Regex import org.gjt.sp.jedit.{jEdit, View, Registers, JEditBeanShellAction} +import org.gjt.sp.jedit.buffer.JEditBuffer import org.gjt.sp.jedit.input.{DefaultInputHandlerProvider, TextAreaInputHandler} import org.gjt.sp.jedit.textarea.JEditEmbeddedTextArea +import org.gjt.sp.jedit.search.HyperSearchResults import org.gjt.sp.jedit.syntax.SyntaxStyle import org.gjt.sp.jedit.gui.KeyEventTranslator -import org.gjt.sp.util.{SyntaxUtilities, Log} +import org.gjt.sp.util.{SyntaxUtilities, Log, HtmlUtilities} + +object Pretty_Text_Area { + def make_highlight_style(): String = + HtmlUtilities.style2html(jEdit.getProperty(HyperSearchResults.HIGHLIGHT_PROP), + Font_Metric.default_font) + + sealed case class Search_Result( + buffer: JEditBuffer, + highlight_style: String, + regex: Regex, + line: Int, + line_range: Text.Range + ) { + lazy val line_text: String = + Library.trim_line(JEdit_Lib.get_text(buffer, line_range).getOrElse("")) + + lazy val gui_text: String = { + // see also HyperSearchResults.highlightString + val s = new StringBuilder(line_range.length * 2) + s ++= "" + s ++= line.toString + s ++= ": " + val line_start = line_range.start + val search_range = Text.Range(line_start, line_start + line_text.length) + var last = 0 + for (range <- JEdit_Lib.search_text(buffer, search_range, regex)) { + val next = range.start - line_start + if (last < next) s ++= line_text.substring(last, next) + s ++= "" + s ++= line_text.substring(next, next + range.length) + s ++= "" + last = range.stop - line_start + } + if (last < line_text.length) s ++= line_text.substring(last) + s ++= "" + s.toString + } + override def toString: String = gui_text + } + + sealed case class Search_Results( + buffer: JEditBuffer, + highlight_style: String, + pattern: Option[Regex] = None, + results: List[Search_Result] = Nil + ) { + val length: Int = results.length + + def update(start_offset: Int): (Int, Search_Results) = + pattern match { + case None => (length, this) + case Some(regex) => + val start_line = buffer.getLineOfOffset(start_offset) + val results1 = results.takeWhile(result => result.line < start_line) + val results2 = + List.from( + for { + line <- (start_line until buffer.getLineCount).iterator + line_range = JEdit_Lib.line_range(buffer, line) + if JEdit_Lib.can_search_text(buffer, line_range, regex) + } yield Search_Result(buffer, highlight_style, regex, line, line_range)) + (results1.length, copy(results = results1 ::: results2)) + } + + def update_pattern(new_pattern: Option[Regex]): Option[Search_Results] = + if (pattern == new_pattern) None + else Some(copy(pattern = new_pattern, results = Nil).update(0)._2) + } +} class Pretty_Text_Area( view: View, @@ -55,8 +128,11 @@ new Rich_Text_Area(view, pretty_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 } + private var current_search_results = + Pretty_Text_Area.Search_Results(getBuffer, Pretty_Text_Area.make_highlight_style()) + + def get_search_pattern(): Option[Regex] = GUI_Thread.require { current_search_results.pattern } + def handle_search(search: Pretty_Text_Area.Search_Results): Unit = () def get_background(): Option[Color] = None @@ -130,6 +206,14 @@ else if (scroll_start < update_start) scroll_start else 0) JEdit_Lib.scroll_to_caret(pretty_text_area) + + val (search_update_start, search_results) = + current_search_results.update(update_start) + if (current_search_results != search_results) { + current_search_results = search_results + handle_search(search_results) + pretty_text_area.getPainter.repaint() + } } } }) @@ -195,13 +279,14 @@ val re = Library.make_regex(s) (re, re.isDefined) } - if (current_search_pattern != pattern) { - current_search_pattern = pattern - pretty_text_area.getPainter.repaint() - } text_field.setForeground( if (ok) search_field_foreground else current_rendering.color(Rendering.Color.error)) + for (search_results <- current_search_results.update_pattern(pattern)) { + current_search_results = search_results + handle_search(search_results) + refresh() + } } diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Fri Nov 22 20:21:36 2024 +0100 @@ -18,6 +18,8 @@ class Simplifier_Trace_Dockable(view: View, position: String) extends Dockable(view, position) { + dockable => + GUI_Thread.require {} @@ -30,8 +32,10 @@ private var do_update = true - private val pretty_text_area = new Pretty_Text_Area(view) - set_content(pretty_text_area) + private val output: Output_Area = new Output_Area(view) + + output.setup(dockable) + set_content(output.text_pane) private def update_contents(): Unit = { val snapshot = current_snapshot @@ -41,8 +45,8 @@ context.questions.values.toList match { case q :: _ => val data = q.data - val output = List(Pretty.block(XML.Text(data.text) :: data.content, indent = 0)) - pretty_text_area.update(snapshot, Command.Results.empty, output) + output.pretty_text_area.update(snapshot, Command.Results.empty, + List(Pretty.block(XML.Text(data.text) :: data.content, indent = 0))) q.answers.foreach { answer => answers.contents += new GUI.Button(answer.string) { override def clicked(): Unit = @@ -50,10 +54,10 @@ } } case Nil => - pretty_text_area.update(snapshot, Command.Results.empty, Nil) + output.pretty_text_area.update(snapshot, Command.Results.empty, Nil) } - handle_resize() + output.handle_resize() } private def show_trace(): Unit = { @@ -61,8 +65,6 @@ new Simplifier_Trace_Window(view, current_snapshot, trace) } - private def handle_resize(): Unit = pretty_text_area.zoom() - private def handle_update(follow: Boolean): Unit = { val (new_snapshot, new_command, new_results, new_id) = PIDE.editor.current_node_snapshot(view) match { @@ -92,7 +94,7 @@ private val main = Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => - GUI_Thread.later { handle_resize() } + GUI_Thread.later { output.handle_resize() } case changed: Session.Commands_Changed => GUI_Thread.later { handle_update(do_update) } @@ -109,6 +111,7 @@ PIDE.session.commands_changed += main PIDE.session.caret_focus += main PIDE.session.trace_events += main + output.init() handle_update(true) } @@ -117,21 +120,10 @@ PIDE.session.commands_changed -= main PIDE.session.caret_focus -= main PIDE.session.trace_events -= main - delay_resize.revoke() + output.exit() } - /* resize */ - - private val delay_resize = - Delay.first(PIDE.session.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() - }) - - /* controls */ private val controls = diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/sledgehammer_dockable.scala --- a/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/sledgehammer_dockable.scala Fri Nov 22 20:21:36 2024 +0100 @@ -19,15 +19,19 @@ class Sledgehammer_Dockable(view: View, position: String) extends Dockable(view, position) { + dockable => + GUI_Thread.require {} - /* text area */ + /* output text area */ + + private val output: Output_Area = new Output_Area(view) - val pretty_text_area = new Pretty_Text_Area(view) - set_content(pretty_text_area) + override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation - override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation + output.setup(dockable) + set_content(output.text_pane) /* query operation */ @@ -46,20 +50,8 @@ } private val sledgehammer = - new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status, pretty_text_area.update) - - - /* resize */ - - private val delay_resize = - Delay.first(PIDE.session.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 = pretty_text_area.zoom() + new Query_Operation(PIDE.editor, view, "sledgehammer", consume_status, + output.pretty_text_area.update) /* controls */ @@ -123,7 +115,7 @@ Wrap_Panel( List(provers_label, Component.wrap(provers), isar_proofs, try0, process_indicator.component, apply_query, cancel_query, locate_query, - pretty_text_area.zoom_component)) + output.pretty_text_area.zoom_component)) add(controls.peer, BorderLayout.NORTH) @@ -134,19 +126,20 @@ private val main = Session.Consumer[Session.Global_Options](getClass.getName) { - case _: Session.Global_Options => GUI_Thread.later { update_provers(); handle_resize() } + case _: Session.Global_Options => + GUI_Thread.later { update_provers(); output.handle_resize() } } override def init(): Unit = { PIDE.session.global_options += main update_provers() - handle_resize() + output.init() sledgehammer.activate() } override def exit(): Unit = { sledgehammer.deactivate() PIDE.session.global_options -= main - delay_resize.revoke() + output.exit() } } diff -r 53e61087bc6f -r 60696404b40a src/Tools/jEdit/src/state_dockable.scala --- a/src/Tools/jEdit/src/state_dockable.scala Fri Nov 22 16:05:42 2024 +0000 +++ b/src/Tools/jEdit/src/state_dockable.scala Fri Nov 22 20:21:36 2024 +0100 @@ -16,31 +16,22 @@ class State_Dockable(view: View, position: String) extends Dockable(view, position) { + dockable => + GUI_Thread.require {} - /* text area */ + /* output text area */ - val pretty_text_area = new Pretty_Text_Area(view) - set_content(pretty_text_area) + private val output: Output_Area = new Output_Area(view) - override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation + override def detach_operation: Option[() => Unit] = output.pretty_text_area.detach_operation private val print_state = - new Query_Operation(PIDE.editor, view, "print_state", _ => (), pretty_text_area.update) - - - /* resize */ + new Query_Operation(PIDE.editor, view, "print_state", _ => (), output.pretty_text_area.update) - private val delay_resize = - Delay.first(PIDE.session.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 = pretty_text_area.zoom() + output.setup(dockable) + set_content(output.split_pane) /* update */ @@ -93,7 +84,7 @@ private val controls = Wrap_Panel( List(auto_update_button, update_button, locate_button) ::: - pretty_text_area.search_zoom_components) + output.pretty_text_area.search_zoom_components) add(controls.peer, BorderLayout.NORTH) @@ -103,7 +94,7 @@ private val main = Session.Consumer[Any](getClass.getName) { case _: Session.Global_Options => - GUI_Thread.later { handle_resize() } + GUI_Thread.later { output.handle_resize() } case changed: Session.Commands_Changed => if (changed.assignment) GUI_Thread.later { auto_update() } @@ -116,7 +107,7 @@ PIDE.session.global_options += main PIDE.session.commands_changed += main PIDE.session.caret_focus += main - handle_resize() + output.init() print_state.activate() auto_update() } @@ -126,6 +117,6 @@ PIDE.session.caret_focus -= main PIDE.session.global_options -= main PIDE.session.commands_changed -= main - delay_resize.revoke() + output.exit() } }