2929import javafx .scene .text .Font ;
3030import javafx .stage .Screen ;
3131import javafx .stage .Stage ;
32+ import org .w3c .dom .events .EventListener ;
33+ import org .w3c .dom .events .EventTarget ;
3234
3335import java .util .ArrayList ;
3436import java .util .Arrays ;
@@ -45,6 +47,7 @@ public class RunREDUCE extends Application {
4547 static int tabLabelNumber = 1 ;
4648 public static REDUCEPanel reducePanel ; // the REDUCEPanel with current focus
4749 static List <REDUCEPanel > reducePanelList = new ArrayList <>();
50+ private static REDUCEPanel reducePanel2 ; // the split pane REDUCEPanel without current focus
4851
4952 // Set the main window to 2/3 the linear dimension of the screen initially:
5053 static final Rectangle2D primaryScreenBounds = Screen .getPrimary ().getVisualBounds ();
@@ -73,12 +76,12 @@ public void start(Stage primaryStage) throws Exception {
7376 primaryStage .setMinHeight (375 );
7477 primaryStage .getIcons ().addAll (RRicon128Image );
7578
76- // REDUCE I/O requires a monospaced font:
77- // Only "system" fonts (in C:\Windows\Fonts) are found, not
78- // "user" fonts (in C:\Users\franc\AppData\Local\Microsoft\Windows\Fonts).
79- // ("DejaVu Sans Mono" is my only "user" font.)
80- // ToDo Consider bundling a font as a resource.
81- reduceFontFamilyName = REDUCEConfiguration .windowsOS ? "Consolas" : "DejaVu Sans Mono" ;
79+ // REDUCE I/O requires a monospaced font:
80+ // Only "system" fonts (in C:\Windows\Fonts) are found, not
81+ // "user" fonts (in C:\Users\franc\AppData\Local\Microsoft\Windows\Fonts).
82+ // ("DejaVu Sans Mono" is my only "user" font.)
83+ // ToDo Consider bundling a font as a resource.
84+ reduceFontFamilyName = REDUCEConfiguration .windowsOS ? "Consolas" : "DejaVu Sans Mono" ;
8285 Font reduceFont = Font .font (reduceFontFamilyName , RRPreferences .fontSize );
8386 if (!reduceFont .getFamily ().equals (reduceFontFamilyName ))
8487 alert (Alert .AlertType .WARNING , "REDUCE I/O Font" ,
@@ -107,7 +110,7 @@ public void start(Stage primaryStage) throws Exception {
107110
108111 static void useSplitPane (boolean enable , boolean startup ) {
109112 if (enable ) {
110- REDUCEPanel reducePanel2 = new REDUCEPanel ();
113+ reducePanel2 = new REDUCEPanel ();
111114 reducePanelList .add (reducePanel2 );
112115 splitPane = new SplitPane (reducePanel , reducePanel2 );
113116 splitPane .setDividerPositions (0.5 );
@@ -118,26 +121,32 @@ static void useSplitPane(boolean enable, boolean startup) {
118121 if (startup )
119122 reducePanel .setSelected (true );
120123 else {
121- reducePanel . setSelected ( false ) ; // old panel
124+ REDUCEPanel tmp = reducePanel ; // swap panels
122125 reducePanel = reducePanel2 ; // new panel
126+ reducePanel2 = tmp ;
123127 reducePanel .setSelected (true );
124128 reducePanel .updateMenus ();
125129 reducePanel .inputTextArea .requestFocus ();
126130 }
127131 } else { // Revert to single pane.
128- reducePanelList .removeIf (x -> x != reducePanel );
132+ reducePanelList .remove (reducePanel2 );
133+ reducePanel2 = null ; // release resources
129134 splitPane = null ; // release resources
130135 reducePanel .removeEventFilter (MouseEvent .MOUSE_CLICKED , RunREDUCE ::splitPaneMouseClicked );
131- // Retain the reducePanel from the selected tab:
136+ ((EventTarget ) reducePanel .doc ).removeEventListener ("scroll" , scrollListener , false );
137+ RunREDUCE .runREDUCEFrame .syncScrollCheckMenuItem .setSelected (false );
138+ // Retain the selected reducePanel:
132139 runREDUCEFrame .frame .setCenter (reducePanel );
133140 reducePanel .activeLabel .setVisible (false );
134141 }
142+ RunREDUCE .runREDUCEFrame .syncScrollCheckMenuItem .setDisable (!enable );
135143 }
136144
137145 private static void splitPaneMouseClicked (MouseEvent event ) {
138146 Node node = (Node ) event .getSource ();
139147 if (node == reducePanel ) return ;
140148 reducePanel .setSelected (false ); // other panel
149+ reducePanel2 = reducePanel ;
141150 reducePanel = (REDUCEPanel ) node ; // this panel
142151 reducePanel .setSelected (true );
143152 reducePanel .updateMenus ();
@@ -150,17 +159,32 @@ private static void splitPaneKeyPressed(KeyEvent event) {
150159 event .getCode () == KeyCode .PAGE_UP ||
151160 event .getCode () == KeyCode .PAGE_DOWN )) {
152161 reducePanel .setSelected (false ); // current panel
153- for (var rp : reducePanelList )
154- if (rp != reducePanel ) {
155- reducePanel = rp ;
156- break ;
157- }
162+ REDUCEPanel tmp = reducePanel ; // swap panels
163+ reducePanel = reducePanel2 ;
164+ reducePanel2 = tmp ;
158165 reducePanel .setSelected (true ); // new panel
159166 reducePanel .updateMenus ();
160167 reducePanel .inputTextArea .requestFocus ();
161168 }
162169 }
163170
171+ static final EventListener scrollListener = new EventListener () {
172+ public void handleEvent (org .w3c .dom .events .Event ev ) {
173+ int scrollY = (int ) reducePanel .window .getMember ("scrollY" );
174+ reducePanel2 .window .call ("scrollTo" , 0 , scrollY );
175+ }
176+ };
177+
178+ static void setUseSplitPaneSyncScroll (boolean enable ) {
179+ if (enable ) {
180+ ((EventTarget ) reducePanel .doc ).addEventListener ("scroll" , scrollListener , false );
181+ ((EventTarget ) reducePanel2 .doc ).addEventListener ("scroll" , scrollListener , false );
182+ } else {
183+ ((EventTarget ) reducePanel .doc ).removeEventListener ("scroll" , scrollListener , false );
184+ ((EventTarget ) reducePanel2 .doc ).removeEventListener ("scroll" , scrollListener , false );
185+ }
186+ }
187+
164188 static void useTabPane (boolean enable ) {
165189 if (enable ) {
166190 tabPane = new TabPane ();
0 commit comments