# HG changeset patch # User wenzelm # Date 1730555930 -3600 # Node ID ccdbe1b538fcf9dda6a86b38d18a0f6042636e5b # Parent c5d1354b7e879c1c2c3d919d18da0ef4a35d4ae9 clarified modules: more re-usable; diff -r c5d1354b7e87 -r ccdbe1b538fc etc/build.props --- a/etc/build.props Sat Nov 02 14:56:13 2024 +0100 +++ b/etc/build.props Sat Nov 02 14:58:50 2024 +0100 @@ -326,7 +326,8 @@ src/Tools/jEdit/src/theories_dockable.scala \ src/Tools/jEdit/src/theories_status.scala \ src/Tools/jEdit/src/timing_dockable.scala \ - src/Tools/jEdit/src/token_markup.scala + src/Tools/jEdit/src/token_markup.scala \ + src/Tools/jEdit/src/tree_text_area.scala services = \ isabelle.Bash$Handler \ isabelle.Bibtex$File_Format \ diff -r c5d1354b7e87 -r ccdbe1b538fc src/Tools/jEdit/src/debugger_dockable.scala --- a/src/Tools/jEdit/src/debugger_dockable.scala Sat Nov 02 14:56:13 2024 +0100 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Sat Nov 02 14:58:50 2024 +0100 @@ -69,38 +69,38 @@ /* pretty text area */ - val pretty_text_area = new Pretty_Text_Area(view) + private val tree_text_area: Tree_Text_Area = + new Tree_Text_Area(view, root_name = "Threads") { + override def handle_resize(): Unit = + GUI_Thread.require { pretty_text_area.zoom(zoom) } - override def detach_operation: Option[() => Unit] = pretty_text_area.detach_operation + override def handle_update(): Unit = { + GUI_Thread.require {} - private def handle_resize(): Unit = - GUI_Thread.require { pretty_text_area.zoom(zoom) } + val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) + val (new_threads, new_output) = debugger.status(tree_selection()) - private def handle_update(): Unit = { - GUI_Thread.require {} + if (new_threads != current_threads) update_tree(new_threads) - val new_snapshot = PIDE.editor.current_node_snapshot(view).getOrElse(current_snapshot) - val (new_threads, new_output) = debugger.status(tree_selection()) + if (new_output != current_output) { + pretty_text_area.update(new_snapshot, Command.Results.empty, Pretty.separate(new_output)) + } - 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 + } } - current_snapshot = new_snapshot - current_threads = new_threads - current_output = new_output - } + override def detach_operation: Option[() => Unit] = + tree_text_area.pretty_text_area.detach_operation + + set_content(tree_text_area.main_pane) /* 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: JTree = tree_text_area.tree def tree_selection(): Option[Debugger.Context] = tree.getLastSelectedPathComponent match { @@ -127,17 +127,16 @@ case _ => thread_contexts.headOption } - tree.clearSelection() - root.removeAllChildren() + tree_text_area.clear() for (thread <- thread_contexts) { val thread_node = new DefaultMutableTreeNode(thread) for ((_, i) <- thread.debug_states.zipWithIndex) thread_node.add(new DefaultMutableTreeNode(thread.select(i))) - root.add(thread_node) + tree_text_area.root.add(thread_node) } - tree.getModel.asInstanceOf[DefaultTreeModel].reload(root) + tree_text_area.reload() tree.expandRow(0) for (i <- Range.inclusive(tree.getRowCount - 1, 1, -1)) tree.expandRow(i) @@ -176,11 +175,6 @@ } }) - 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 */ @@ -262,7 +256,8 @@ tooltip = "Official Standard ML instead of Isabelle/ML" } - private val zoom = new Font_Info.Zoom { override def changed(): Unit = handle_resize() } + private val zoom = + new Font_Info.Zoom { override def changed(): Unit = tree_text_area.handle_resize() } private val controls = Wrap_Panel( @@ -270,7 +265,8 @@ 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)) + tree_text_area.pretty_text_area.search_label, + tree_text_area.pretty_text_area.search_field, zoom)) add(controls.peer, BorderLayout.NORTH) @@ -295,27 +291,17 @@ } - /* 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() } + GUI_Thread.later { tree_text_area.handle_resize() } case Debugger.Update => GUI_Thread.later { break_button.selected = debugger.is_break() - handle_update() + tree_text_area.handle_update() } } @@ -323,7 +309,7 @@ PIDE.session.global_options += main PIDE.session.debugger_updates += main debugger.init(dockable) - handle_update() + tree_text_area.handle_update() jEdit.propertiesChanged() } @@ -339,7 +325,7 @@ /* resize */ private val delay_resize = - Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() } + Delay.first(PIDE.session.update_delay, gui = true) { tree_text_area.handle_resize() } addComponentListener(new ComponentAdapter { override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke() diff -r c5d1354b7e87 -r ccdbe1b538fc src/Tools/jEdit/src/tree_text_area.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/tree_text_area.scala Sat Nov 02 14:58:50 2024 +0100 @@ -0,0 +1,69 @@ +/* Title: Tools/jEdit/src/tree_text_area.scala + Author: Makarius + +GUI component for tree view with pretty-printed text area. +*/ + +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, 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 + + +class Tree_Text_Area(view: View, root_name: String = "Overview") { + GUI_Thread.require {} + + + /* tree view */ + + val root: DefaultMutableTreeNode = new DefaultMutableTreeNode(root_name) + + val tree: JTree = new JTree(root) + tree.setRowHeight(0) + tree.getSelectionModel.setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION) + + def clear(): Unit = { + tree.clearSelection() + root.removeAllChildren() + } + + def reload(): Unit = + tree.getModel.asInstanceOf[DefaultTreeModel].reload(root) + + + /* text area */ + + val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view) + + def handle_resize(): Unit = () + def handle_update(): Unit = () + + + /* main pane */ + + val tree_pane: ScrollPane = new ScrollPane(Component.wrap(tree)) + tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always + tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always + tree_pane.minimumSize = new Dimension(200, 100) + + val main_pane: SplitPane = new SplitPane(Orientation.Vertical) { + oneTouchExpandable = true + leftComponent = tree_pane + rightComponent = Component.wrap(pretty_text_area) + } +}