More REPL and GUI improvements

Convex-Dev · Sep 3, 2024 · 9ef679d · 9ef679d
1 parent a65c58f
commit 9ef679d
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 9 deletions.
diff --git a/convex-gui/src/main/java/convex/gui/panels/REPLPanel.java b/convex-gui/src/main/java/convex/gui/panels/REPLPanel.java
@@ -1,7 +1,6 @@
 package convex.gui.panels;
 
 import java.awt.Color;
-import java.awt.Component;
 import java.awt.Font;
 import java.awt.event.ComponentAdapter;
 import java.awt.event.ComponentEvent;
@@ -49,6 +48,7 @@
 import convex.gui.components.CodePane;
 import convex.gui.components.account.AccountChooserPanel;
 import convex.gui.utils.CVXHighlighter;
+import convex.gui.utils.Toolkit;
 import net.miginfocom.swing.MigLayout;
 
 /**
@@ -57,8 +57,10 @@
 @SuppressWarnings("serial")
 public class REPLPanel extends JPanel {
 
-	protected final  CodePane input;
+	protected final CodePane input;
 	protected final CodePane output;
+	protected final JScrollPane inputScrollPane;
+	protected final JScrollPane outputScrollPane;
 	private final JButton btnRun;
 	private final JButton btnClear;
 	private final JButton btnInfo;
@@ -72,8 +74,8 @@ public class REPLPanel extends JPanel {
 
 	private InputListener inputListener=new InputListener();
 
-	private Font OUTPUT_FONT=new Font("Monospaced", Font.PLAIN, 24);
-	private Font INPUT_FONT=new Font("Monospaced", Font.PLAIN, 30);
+	private Font OUTPUT_FONT=Toolkit.MONO_FONT.deriveFont(16f*Toolkit.SCALE);
+	private Font INPUT_FONT=Toolkit.MONO_FONT.deriveFont(20f*Toolkit.SCALE);
 	private Color DEFAULT_OUTPUT_COLOR=Color.LIGHT_GRAY;
 
 	private JPanel actionPanel;
@@ -170,16 +172,18 @@ public REPLPanel(Convex convex) {
 		output.setToolTipText("Output from transaction execution");
 		//DefaultCaret caret = (DefaultCaret)(outputArea.getCaret());
 		//caret.setUpdatePolicy(DefaultCaret.ALWAYS_UPDATE);
-		splitPane.setLeftComponent(wrapScrollPane(output));
+		outputScrollPane=wrapScrollPane(output);
+		splitPane.setLeftComponent(outputScrollPane);
 
 		input = new CodePane();
 		input.setFont(INPUT_FONT);
 		input.getDocument().addDocumentListener(inputListener);
 		input.addKeyListener(inputListener);
 		input.setToolTipText("Input commands here (Press Enter at the end of input to send)");
+		inputScrollPane=wrapScrollPane(input);
 		//inputArea.setForeground(Color.GREEN);
 
-		splitPane.setRightComponent(wrapScrollPane(input));
+		splitPane.setRightComponent(inputScrollPane);
 
 		// stop ctrl+arrow losing focus
 		setFocusTraversalKeysEnabled(false);
@@ -246,7 +250,7 @@ public void componentShown(ComponentEvent ce) {
 		});
 	}
 
-	private Component wrapScrollPane(CodePane codePane) {
+	private JScrollPane wrapScrollPane(CodePane codePane) {
 		JScrollPane scrollPane=new JScrollPane(codePane);
 		return scrollPane;
 	}

diff --git a/convex-gui/src/main/java/convex/gui/peer/PeerGUI.java b/convex-gui/src/main/java/convex/gui/peer/PeerGUI.java
@@ -385,7 +385,9 @@ public void launchExtraPeer() {
 		}
 	}
 
-	public void closePeers() {
+	@Override
+	public void close() {
+		updateRunning=false;
 		DefaultListModel<ConvexLocal> peerList = getPeerList();
 		int n = peerList.getSize();
 		for (int i = 0; i < n; i++) {
@@ -396,6 +398,7 @@ public void closePeers() {
 				// ignore
 			}
 		}
+		super.close();
 	}
 
 	public void addPeer(ConvexLocal cvl) {

diff --git a/convex-gui/src/main/java/convex/gui/utils/Toolkit.java b/convex-gui/src/main/java/convex/gui/utils/Toolkit.java
@@ -69,7 +69,7 @@ public class Toolkit {
 
 	public static Font DEFAULT_FONT = new Font(Font.SANS_SERIF,Font.PLAIN,(int)DEFAULT_FONT_SIZE);
 	public static Font BIG_FONT = new Font(Font.SANS_SERIF, Font.BOLD, (int)(DEFAULT_FONT_SIZE*1.8));
-	public static Font MONO_FONT = new Font(Font.MONOSPACED, Font.BOLD, (int)(DEFAULT_FONT_SIZE));
+	public static Font MONO_FONT = new Font(Font.MONOSPACED, Font.PLAIN, (int)(DEFAULT_FONT_SIZE));
 	public static Font BIG_MONO_FONT = new Font(Font.MONOSPACED, Font.BOLD, (int)(DEFAULT_FONT_SIZE*1.5));
 	public static Font SMALL_MONO_FONT = new Font(Font.MONOSPACED, Font.PLAIN, (int)(DEFAULT_FONT_SIZE*0.8));
 	public static Font BUTTON_FONT = new Font(Font.SANS_SERIF, Font.PLAIN, (int)(DEFAULT_FONT_SIZE*1.2));