# HG changeset patch
# User wenzelm
# Date 1730721485 -3600
# Node ID 40af19b10f8a1f169fd593777edc478cb140145f
# Parent  fe32eaea366cffb299ddf0af0a20e04652a32f2a
clarified modules;

diff -r fe32eaea366c -r 40af19b10f8a etc/build.props
--- 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 \
diff -r fe32eaea366c -r 40af19b10f8a src/Tools/jEdit/src/debugger_dockable.scala
--- 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()
diff -r fe32eaea366c -r 40af19b10f8a src/Tools/jEdit/src/output_area.scala
--- /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 _ =>
+    }
+  }
+}
diff -r fe32eaea366c -r 40af19b10f8a src/Tools/jEdit/src/tree_text_area.scala
--- 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 _ =>
-    }
-  }
-}