--- a/etc/build.props Mon Nov 04 12:22:24 2024 +0100
+++ b/etc/build.props Mon Nov 04 12:58:05 2024 +0100
@@ -304,6 +304,7 @@
src/Tools/jEdit/src/keymap_merge.scala \
src/Tools/jEdit/src/main_plugin.scala \
src/Tools/jEdit/src/monitor_dockable.scala \
+ src/Tools/jEdit/src/output_area.scala \
src/Tools/jEdit/src/output_dockable.scala \
src/Tools/jEdit/src/pide_docking_framework.scala \
src/Tools/jEdit/src/pretty_text_area.scala \
@@ -327,8 +328,7 @@
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/tree_text_area.scala
+ src/Tools/jEdit/src/token_markup.scala
services = \
isabelle.Bash$Handler \
isabelle.Bibtex$File_Format \
--- a/src/Tools/jEdit/src/debugger_dockable.scala Mon Nov 04 12:22:24 2024 +0100
+++ b/src/Tools/jEdit/src/debugger_dockable.scala Mon Nov 04 12:58:05 2024 +0100
@@ -66,8 +66,8 @@
/* pretty text area */
- private val output: Tree_Text_Area =
- new Tree_Text_Area(view, root_name = "Threads") {
+ private val output: Output_Area =
+ new Output_Area(view, root_name = "Threads") {
override def handle_tree_selection(e: TreeSelectionEvent): Unit = {
update_focus()
update_vals()
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/output_area.scala Mon Nov 04 12:58:05 2024 +0100
@@ -0,0 +1,90 @@
+/* Title: Tools/jEdit/src/output_area.scala
+ Author: Makarius
+
+GUI component for structured output.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Dimension
+import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
+ MouseEvent, MouseAdapter}
+import javax.swing.JComponent
+import javax.swing.event.TreeSelectionEvent
+
+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") {
+ GUI_Thread.require {}
+
+
+ /* tree view */
+
+ val tree: Tree_View =
+ new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
+
+ def handle_tree_selection(e: TreeSelectionEvent): Unit = ()
+ tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))
+
+
+ /* text area */
+
+ val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view)
+
+ def handle_resize(): Unit = ()
+ def handle_update(): Unit = ()
+
+ lazy val delay_resize: Delay =
+ Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
+
+
+ /* 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)
+ }
+
+
+ /* GUI component */
+
+ def handle_focus(): Unit = ()
+
+ def init_gui(parent: JComponent): Unit = {
+ parent.addComponentListener(
+ new ComponentAdapter {
+ override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
+ override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
+ })
+ parent.addFocusListener(
+ new FocusAdapter {
+ override def focusGained(e: FocusEvent): Unit = handle_focus()
+ })
+
+ tree.addMouseListener(
+ new MouseAdapter {
+ override def mouseClicked(e: MouseEvent): Unit = {
+ val click = tree.getPathForLocation(e.getX, e.getY)
+ if (click != null && e.getClickCount == 1) handle_focus()
+ }
+ })
+
+ parent match {
+ case dockable: Dockable => dockable.set_content(main_pane)
+ case _ =>
+ }
+ }
+}
--- a/src/Tools/jEdit/src/tree_text_area.scala Mon Nov 04 12:22:24 2024 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,90 +0,0 @@
-/* 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.Dimension
-import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
- MouseEvent, MouseAdapter}
-import javax.swing.JComponent
-import javax.swing.event.TreeSelectionEvent
-
-import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
-import scala.swing.event.ButtonClicked
-
-import org.gjt.sp.jedit.View
-
-
-class Tree_Text_Area(view: View, root_name: String = "Overview") {
- GUI_Thread.require {}
-
-
- /* tree view */
-
- val tree: Tree_View =
- new Tree_View(root = Tree_View.Node(root_name), single_selection_mode = true)
-
- def handle_tree_selection(e: TreeSelectionEvent): Unit = ()
- tree.addTreeSelectionListener((e: TreeSelectionEvent) => handle_tree_selection(e))
-
-
- /* text area */
-
- val pretty_text_area: Pretty_Text_Area = new Pretty_Text_Area(view)
-
- def handle_resize(): Unit = ()
- def handle_update(): Unit = ()
-
- lazy val delay_resize: Delay =
- Delay.first(PIDE.session.update_delay, gui = true) { handle_resize() }
-
-
- /* 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)
- }
-
-
- /* GUI component */
-
- def handle_focus(): Unit = ()
-
- def init_gui(parent: JComponent): Unit = {
- parent.addComponentListener(
- new ComponentAdapter {
- override def componentResized(e: ComponentEvent): Unit = delay_resize.invoke()
- override def componentShown(e: ComponentEvent): Unit = delay_resize.invoke()
- })
- parent.addFocusListener(
- new FocusAdapter {
- override def focusGained(e: FocusEvent): Unit = handle_focus()
- })
-
- tree.addMouseListener(
- new MouseAdapter {
- override def mouseClicked(e: MouseEvent): Unit = {
- val click = tree.getPathForLocation(e.getX, e.getY)
- if (click != null && e.getClickCount == 1) handle_focus()
- }
- })
-
- parent match {
- case dockable: Dockable => dockable.set_content(main_pane)
- case _ =>
- }
- }
-}