Fix for PeerComponent text selection

Convex-Dev · Feb 21, 2024 · 71c7462 · 71c7462
1 parent 749b014
commit 71c7462
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/convex-gui/src/main/java/convex/gui/components/PeerComponent.java b/convex-gui/src/main/java/convex/gui/components/PeerComponent.java
@@ -155,7 +155,11 @@ public PeerComponent(PeerGUI manager, Convex value) {
 		}
 
 		manager.tickState.addPropertyChangeListener(e->{
+			// Set text while maintaining selection
+			int ss=description.getSelectionStart();
+			int se=description.getSelectionEnd();
 			description.setText(getPeerDescription());
+			description.select(ss, se);
 		});
 
 	}