Skip to content

Commit 70df98b

Browse files
committed
When switching panels in a split pane using the keyboard, focus on the output web view if the input text area is hidden. Make synchronised scrolling relative to the maximum scroll distance, i.e. the content height minus the window height.
1 parent 8afe642 commit 70df98b

2 files changed

Lines changed: 17 additions & 6 deletions

File tree

src/fjwright/runreduce/REDUCEPanel.java

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ public class REDUCEPanel extends BorderPane {
4343
@FXML
4444
private Label outputLabel, inputLabel;
4545
@FXML
46-
private ToggleButton hideEditorToggleButton;
46+
ToggleButton hideEditorToggleButton;
4747
@FXML
4848
Label activeLabel;
4949
@FXML
@@ -61,8 +61,8 @@ public class REDUCEPanel extends BorderPane {
6161

6262
final WebEngine webEngine;
6363
HTMLDocument doc;
64-
private HTMLElement html, head, inputPre;
65-
HTMLElement body;
64+
HTMLElement html, body;
65+
private HTMLElement head, inputPre;
6666
private JSObject katex, katexMacros;
6767
JSObject window;
6868

src/fjwright/runreduce/RunREDUCE.java

Lines changed: 14 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -29,6 +29,7 @@
2929
import javafx.scene.text.Font;
3030
import javafx.stage.Screen;
3131
import javafx.stage.Stage;
32+
import netscape.javascript.JSObject;
3233
import org.w3c.dom.events.EventListener;
3334
import org.w3c.dom.events.EventTarget;
3435

@@ -165,14 +166,24 @@ private static void splitPaneKeyPressed(KeyEvent event) {
165166
reducePanel2 = tmp;
166167
reducePanel.setSelected(true); // new panel
167168
reducePanel.updateMenus();
168-
reducePanel.inputTextArea.requestFocus();
169+
if (reducePanel.hideEditorToggleButton.isSelected())
170+
reducePanel.outputWebView.requestFocus();
171+
else
172+
reducePanel.inputTextArea.requestFocus();
169173
}
170174
}
171175

172176
static final EventListener scrollListener = new EventListener() {
173177
public void handleEvent(org.w3c.dom.events.Event ev) {
174-
int scrollY = (int) reducePanel.window.getMember("scrollY");
175-
reducePanel2.window.call("scrollTo", 0, scrollY);
178+
// int scrollY = (int) reducePanel.window.getMember("scrollY");
179+
// reducePanel2.window.call("scrollTo", 0, scrollY);
180+
// Relative scrolling:
181+
int windowHeight = (int) reducePanel.window.getMember("innerHeight");
182+
float thisScrollYMax = (int) ((JSObject) reducePanel.html).getMember("scrollHeight") - windowHeight;
183+
float thatScrollYMax = (int) ((JSObject) reducePanel2.html).getMember("scrollHeight") - windowHeight;
184+
int thisScrollY = (int) reducePanel.window.getMember("scrollY");
185+
int thatScrollY = (int) (thisScrollY / thisScrollYMax * thatScrollYMax);
186+
reducePanel2.window.call("scrollTo", 0, thatScrollY);
176187
}
177188
};
178189

0 commit comments

Comments
 (0)