# HG changeset patch
# User wenzelm
# Date 1731936948 -3600
# Node ID 085393ed204a9bee6779357207ba9d831cfe5246
# Parent  dd657c4bc2696b2492ccdff39a64b0659d8a5731
handle tree selection;

diff -r dd657c4bc269 -r 085393ed204a src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Mon Nov 18 12:36:56 2024 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Mon Nov 18 14:35:48 2024 +0100
@@ -11,6 +11,7 @@
 
 import java.awt.BorderLayout
 import java.awt.event.{ComponentEvent, ComponentAdapter}
+import javax.swing.event.TreeSelectionEvent
 
 import org.gjt.sp.jedit.View
 
@@ -67,6 +68,19 @@
     }
   }
 
+
+  /* tree view */
+
+  private def tree_selection(): Option[Pretty_Text_Area.Search_Result] =
+    output.tree.get_selection({ case x: Pretty_Text_Area.Search_Result => x })
+
+  output.tree.addTreeSelectionListener({ (e: TreeSelectionEvent) =>
+    for (result <- tree_selection()) {
+      output.pretty_text_area.setCaretPosition(result.line_range.start)
+      JEdit_Lib.scroll_to_caret(output.pretty_text_area)
+    }
+  })
+
   output.init_gui(dockable, split = true)