Edits for REPL keys, hopefully more mac friendly

Convex-Dev · Aug 18, 2023 · 9d79d88 · 9d79d88
1 parent f009c5c
commit 9d79d88
Showing 1 changed file with 4 additions and 2 deletions.
diff --git a/convex-gui/src/main/java/convex/gui/manager/windows/peer/REPLPanel.java b/convex-gui/src/main/java/convex/gui/manager/windows/peer/REPLPanel.java
@@ -236,6 +236,8 @@ public void insertUpdate(DocumentEvent e) {
 			int len = e.getLength();
 			int off = e.getOffset();
 			String s = inputArea.getText();
+
+			// Detect Enter at end of form
 			if ((len == 1) && (len + off == s.length()) && (s.charAt(off) == '\n')) {
 				sendMessage(s.trim());
 			}
@@ -258,8 +260,8 @@ public void keyTyped(KeyEvent e) {
 
 		@Override
 		public void keyPressed(KeyEvent e) {
-			// System.out.println(e);
-			if (e.isControlDown()) {
+			// CTRL or Shift scrolls through history
+			if (e.isControlDown()||e.isShiftDown()) {
 				int code = e.getKeyCode();
 				int hSize=history.size();
 				if (code==KeyEvent.VK_UP) {