Better Scrolling behaviour for Peer panels

Convex-Dev · Aug 21, 2023 · 5262d30 · 5262d30
1 parent db8e3f3
commit 5262d30
Show file tree

Hide file tree

Showing 3 changed files with 29 additions and 8 deletions.
diff --git a/convex-gui/src/main/java/convex/gui/components/NonUpdatingCaret.java b/convex-gui/src/main/java/convex/gui/components/NonUpdatingCaret.java
@@ -0,0 +1,13 @@
+package convex.gui.components;
+
+import java.awt.Rectangle;
+
+import javax.swing.text.DefaultCaret;
+
+@SuppressWarnings("serial")
+public class NonUpdatingCaret extends DefaultCaret {
+    @Override
+    protected void adjustVisibility(Rectangle nloc) {
+
+    }
+}
diff --git a/convex-gui/src/main/java/convex/gui/manager/windows/peer/PeerInfoPanel.java b/convex-gui/src/main/java/convex/gui/manager/windows/peer/PeerInfoPanel.java
@@ -8,12 +8,14 @@
 
 import javax.swing.JButton;
 import javax.swing.JPanel;
+import javax.swing.JScrollPane;
 import javax.swing.JTextArea;
 import javax.swing.Timer;
 
 import convex.api.Convex;
 import convex.core.util.Text;
 import convex.gui.components.ActionPanel;
+import convex.gui.components.NonUpdatingCaret;
 import convex.gui.utils.Toolkit;
 import convex.peer.AThreadedComponent;
 import convex.peer.Server;
@@ -32,15 +34,18 @@ public PeerInfoPanel(Convex p) {
 		JButton refreshButton = new JButton("Refresh");
 		panel.add(refreshButton);
 
-		JPanel panel_1 = new JPanel();
-		add(panel_1, BorderLayout.CENTER);
-		panel_1.setLayout(new BorderLayout(0, 0));
-
 		textArea = new JTextArea();
 		textArea.setEditable(false);
 		textArea.setBackground(null);
+		textArea.setCaret(new NonUpdatingCaret());
+		textArea.setColumns(100);
 		textArea.setFont(Toolkit.SMALL_MONO_FONT);
 
+		JPanel panel1=new JPanel();
+		panel1.add(textArea);
+		JScrollPane jsp1=new JScrollPane(panel1);
+		add(jsp1, BorderLayout.CENTER);
+
 		// Set up periodic refresh
 		int INTERVAL = 500;
 		Timer timer = new Timer(INTERVAL,new ActionListener() {
@@ -60,7 +65,6 @@ public void componentShown(ComponentEvent ce) {
 		    }
 		});
 
-		panel_1.add(textArea);
 		refreshButton.addActionListener(e -> {
 			updateState(p);
 		});

diff --git a/convex-gui/src/main/java/convex/gui/manager/windows/peer/PeerWindow.java b/convex-gui/src/main/java/convex/gui/manager/windows/peer/PeerWindow.java
@@ -2,6 +2,8 @@
 
 import java.awt.BorderLayout;
 
+import javax.swing.JLabel;
+import javax.swing.JScrollPane;
 import javax.swing.JTabbedPane;
 
 import org.slf4j.Logger;
@@ -37,16 +39,18 @@ public PeerWindow(PeerGUI manager, Convex peer) {
 				Convex convex = Convex.connect(server.getHostAddress(), server.getPeerController(),server.getKeyPair());
 				tabbedPane.addTab("REPL", null, new REPLPanel(convex), null);
 			} catch (Throwable t) {
-				log.warn("Unable to create Peer Controller Window");
+				String msg=("Failed to connect to Peer: "+t);
+				log.warn(msg);
+				tabbedPane.addTab("REPL Error", null, new JLabel(msg), null);
+				return;
 			}
-			tabbedPane.addTab("Observation", null, new ObserverPanel(server), null);
+			tabbedPane.addTab("Observation", null, new JScrollPane(new ObserverPanel(server)), null);
 		}
 		tabbedPane.addTab("Stress", null, new StressPanel(peer), null);
 		tabbedPane.addTab("Info", null, new PeerInfoPanel(peer), null);
 
 		PeerComponent pcom = new PeerComponent(manager, peer);
 		add(pcom, BorderLayout.NORTH);
-
 	}
 
 	@Override