Fixes 255, now wrapping text and no wrapping for tables

AlloyTools · May 14, 2024 · 052abd9 · 052abd9
1 parent 52a0527
commit 052abd9
Showing 1 changed file with 6 additions and 8 deletions.
diff --git a/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java b/org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java
@@ -942,18 +942,14 @@ public final void focusLost(FocusEvent e) {
             }
             case TEXT : {
                 String textualOutput = myStates.get(statepanes - 1).getOriginalInstance().originalA4.toString(current);
-                content = getTextComponent(textualOutput);
+                content = getTextComponent(textualOutput, true);
                 break;
             }
             case TABLE : {
                 String textualOutput = myStates.get(statepanes - 1).getOriginalInstance().originalA4.format(current);
-                content = getTextComponent(textualOutput);
+                content = getTextComponent(textualOutput, false);
                 break;
             }
-            // case XML: {
-            // content=getTextComponent(xmlFileName);
-            // break;
-            // }
             default : {
                 List<VizState> numPanes = isTrace && !isMeta ? myStates : myStates.subList(statepanes - 1, statepanes);
                 if (myGraphPanel == null || numPanes.size() != myGraphPanel.numPanels()) {
@@ -1131,9 +1127,11 @@ private void addThemeHistory(String filename) {
 
     /**
      * Helper method returns a JTextArea containing the given text.
+     *
+     * @param b
      */
-    private JComponent getTextComponent(String text) {
-        final JTextArea ta = OurUtil.textarea(text, 10, 10, false, false);
+    private JComponent getTextComponent(String text, boolean wrap) {
+        final JTextArea ta = OurUtil.textarea(text, 10, 10, false, wrap);
         final JScrollPane ans = new JScrollPane(ta, ScrollPaneConstants.VERTICAL_SCROLLBAR_AS_NEEDED, ScrollPaneConstants.HORIZONTAL_SCROLLBAR_AS_NEEDED) {
 
             private static final long serialVersionUID = 0;