--- 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.
--- 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) {
--- 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()
--- 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()
}
--- 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)
}
}
--- 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()
}
}
--- 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 }
}
}
--- 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()
}
--- 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()
- })
}
--- 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 ++= "<html><b>"
+ s ++= line.toString
+ s ++= ":</b> "
+ 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 ++= "<span style=\""
+ s ++= highlight_style
+ s ++= "\">"
+ s ++= line_text.substring(next, next + range.length)
+ s ++= "</span>"
+ last = range.stop - line_start
+ }
+ if (last < line_text.length) s ++= line_text.substring(last)
+ s ++= "</html>"
+ 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()
+ }
}
--- 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 =
--- 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()
}
}
--- 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()
}
}