diff --git a/convex-gui/src/main/java/convex/gui/components/NonUpdatingCaret.java b/convex-gui/src/main/java/convex/gui/components/NonUpdatingCaret.java new file mode 100644 index 000000000..6b3701d69 --- /dev/null +++ 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 index 0e2649560..432f6f946 100644 --- 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 index 841d9c129..8f90f61cd 100644 --- 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