--- 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)