more operations, specifically for FlatLaf;
authorwenzelm
Mon, 16 Dec 2024 22:53:31 +0100
changeset 81614 afd27db5a15b
parent 81608 a38e80897c34
child 81615 ebf954ceb4d1
more operations, specifically for FlatLaf;
src/Tools/jEdit/src/output_area.scala
--- a/src/Tools/jEdit/src/output_area.scala	Mon Dec 16 19:22:54 2024 +0100
+++ b/src/Tools/jEdit/src/output_area.scala	Mon Dec 16 22:53:31 2024 +0100
@@ -12,13 +12,15 @@
 import java.awt.Dimension
 import java.awt.event.{ComponentEvent, ComponentAdapter, FocusAdapter, FocusEvent,
   MouseEvent, MouseAdapter}
-import javax.swing.JComponent
+import javax.swing.{JComponent, JButton}
 import javax.swing.event.{TreeSelectionListener, TreeSelectionEvent}
 
 import scala.util.matching.Regex
 import scala.swing.{Component, ScrollPane, SplitPane, Orientation}
 import scala.swing.event.ButtonClicked
 
+import com.formdev.flatlaf.ui.FlatSplitPaneUI
+
 import org.gjt.sp.jedit.View
 
 
@@ -115,6 +117,37 @@
       rightComponent = text_pane
     }
 
+  def split_pane_layout(open: Boolean = false): Unit = {
+    split_pane.peer.getUI match {
+      case ui: FlatSplitPaneUI =>
+        val div = ui.getDivider
+
+        // operations from protected FlatSplitPaneUI.FlatSplitPaneDivider
+        val left_collapsed =
+          Untyped.the_method(div.getClass, "isLeftCollapsed").invoke(div) == java.lang.Boolean.TRUE
+        val right_collapsed =
+          Untyped.the_method(div.getClass, "isRightCollapsed").invoke(div) == java.lang.Boolean.TRUE
+
+        def click(i: Int): Unit = {
+          val comp =
+            try { div.getComponent(i) }
+            catch { case _: ArrayIndexOutOfBoundsException => null }
+          comp match {
+            case button: JButton => button.doClick()
+            case _ =>
+          }
+        }
+
+        if (open && left_collapsed) click(1)
+        else if (open && right_collapsed || !open && !left_collapsed) click(0)
+        else if (!open && right_collapsed) {
+          click(0)
+          GUI_Thread.later { click(0) }  // FIXME!?
+        }
+      case _ =>
+    }
+  }
+
   def setup(parent: JComponent): Unit = {
     parent.addComponentListener(component_listener)
     parent.addFocusListener(focus_listener)