Taclet match dialog: readable \assumes candidates and smarter window placement

key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/AssumesSelectionPanel.java

@@ -45,7 +45,7 @@ public class AssumesSelectionPanel extends JPanel {
     private static final long serialVersionUID = 1L;
 
     /** abbreviate candidate text longer than this in the list (full text on hover) */
-    private static final int ABBREV_LIMIT = 100;
+    private static final int ABBREV_LIMIT = 200;
 
     private static final Color OK_COLOR = new Color(0x1D9E75);
     private static final Color WARN_COLOR = new Color(0xBA7517);
@@ -445,7 +445,9 @@ public Component getListCellRendererComponent(JList<?> l, Object value, int inde
                 boolean isSelected, boolean cellHasFocus) {
             JLabel c = (JLabel) super.getListCellRendererComponent(l, value, index, isSelected,
                 cellHasFocus);
-            c.setText(TmText.truncateFirstLine(text((AssumesFormulaInstantiation) value),
+            // flatten a possibly multi-line, wrapped formula to one line so the whole thing shows
+            // (up to the abbreviation limit) instead of just its first wrapped segment
+            c.setText(TmText.collapseToLine(text((AssumesFormulaInstantiation) value),
                 ABBREV_LIMIT));
             c.setFont(TmStyle.mono(c));
             return c;

key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TacletMatchDialog.java

@@ -80,10 +80,74 @@ public TacletMatchDialog(MainWindow parent, TacletInstantiationModel[] model, Go
         pack();
 
         mainWindow.loadPreferences(this);
-        setLocationRelativeTo(parent);
+        positionDialog(parent);
         setVisible(true);
     }
 
+    /**
+     * where the dialog was last closed, remembered for this session only (deliberately not
+     * persisted: on a restart the main window may sit elsewhere, so a stale absolute position would
+     * be worse than a fresh placement beside the sequent).
+     */
+    private static Point sessionLocation;
+
+    /**
+     * Places the dialog so it does not sit on top of the sequent view. The user frequently needs to
+     * read a variable name off the sequent, or drag a sub-term from it onto a field, so covering it
+     * is exactly what to avoid. Within a session the last position the user moved it to is reused;
+     * otherwise the dialog is put in the free space beside the sequent view, falling back to the
+     * screen edge that leaves the most of the sequent visible. Either way it ends up fully on
+     * screen.
+     */
+    private void positionDialog(MainWindow parent) {
+        Rectangle screen = usableScreen(parent);
+        Point target = sessionLocation != null ? sessionLocation : besideSequent(parent, screen);
+        // keep the window fully on screen (the remembered spot may be off a since-changed screen)
+        int x = Math.max(screen.x, Math.min(target.x, screen.x + screen.width - getWidth()));
+        int y = Math.max(screen.y, Math.min(target.y, screen.y + screen.height - getHeight()));
+        setLocation(x, y);
+    }
+
+    /** a spot beside the sequent view (right, else left, else the roomier screen edge). */
+    private Point besideSequent(MainWindow parent, Rectangle screen) {
+        Rectangle avoid = sequentBoundsOnScreen(parent);
+        int gap = 8;
+        int w = getWidth();
+        int rightX = avoid.x + avoid.width + gap;
+        int leftX = avoid.x - gap - w;
+        int x;
+        if (rightX + w <= screen.x + screen.width) {
+            x = rightX; // free space to the right of the sequent
+        } else if (leftX >= screen.x) {
+            x = leftX; // free space to the left of the sequent
+        } else {
+            // the sequent leaves no room beside it: dock to the edge with more space, so at least
+            // that much of the sequent stays visible
+            int roomRight = screen.x + screen.width - (avoid.x + avoid.width);
+            int roomLeft = avoid.x - screen.x;
+            x = roomRight >= roomLeft ? screen.x + screen.width - w : screen.x;
+        }
+        return new Point(x, avoid.y); // align with the top of the sequent (caller clamps to screen)
+    }
+
+    /** the sequent view's rectangle on screen, or the whole main window if it is not showing. */
+    private Rectangle sequentBoundsOnScreen(MainWindow parent) {
+        Component seq = parent.getGoalView();
+        if (seq != null && seq.isShowing()) {
+            return new Rectangle(seq.getLocationOnScreen(), seq.getSize());
+        }
+        return parent.getBounds();
+    }
+
+    /** the usable bounds (minus taskbar/menubar insets) of the screen the main window is on. */
+    private static Rectangle usableScreen(Window on) {
+        GraphicsConfiguration gc = on.getGraphicsConfiguration();
+        Rectangle b = gc.getBounds();
+        Insets in = Toolkit.getDefaultToolkit().getScreenInsets(gc);
+        return new Rectangle(b.x + in.left, b.y + in.top,
+            b.width - in.left - in.right, b.height - in.top - in.bottom);
+    }
+
     private void layoutDialog() {
         getContentPane().setLayout(new BorderLayout());
         getContentPane().add(createInstantiationPanel(), BorderLayout.CENTER);
@@ -275,6 +339,8 @@ protected void pushAllInputToModel() {
 
     @Override
     protected void closeDlg() {
+        // remember the position for the rest of this session; savePreferences persists the size
+        sessionLocation = getLocation();
         if (mainWindow != null) {
             mainWindow.savePreferences(this);
         }

key.ui/src/main/java/de/uka/ilkd/key/gui/tacletmatch/TmText.java

@@ -24,20 +24,14 @@ static String firstLine(String s) {
     }
 
     /**
-     * the first line of {@code s}, truncated to {@code limit} characters with an ellipsis appended
-     * when it was longer.
-     */
-    static String truncateFirstLine(String s, int limit) {
-        String line = firstLine(s);
-        return line.length() > limit ? line.substring(0, limit) + " …" : line;
-    }
-
-    /**
-     * {@code s} flattened to a single line (newlines become spaces), truncated to {@code limit}
-     * characters with an ellipsis appended when it was longer.
+     * {@code s} flattened to a single line and truncated to {@code limit} characters with an
+     * ellipsis appended when it was longer. Every run of whitespace (the newlines and the alignment
+     * indentation the pretty-printer inserts when it wraps a term) collapses to a single space, so
+     * a
+     * multi-line formula reads as one continuous line instead of a stub followed by blank gaps.
      */
     static String collapseToLine(String s, int limit) {
-        String oneLine = (s == null ? "" : s).replace('\n', ' ');
+        String oneLine = (s == null ? "" : s).replaceAll("\\s+", " ").trim();
         return oneLine.length() > limit ? oneLine.substring(0, limit) + " …" : oneLine;
     }
 

key.ui/src/test/java/de/uka/ilkd/key/gui/tacletmatch/TmTextTest.java

@@ -23,22 +23,16 @@ public void firstLine() {
         assertEquals("a", TmText.firstLine("a\n"), "a trailing newline keeps the content line");
     }
 
-    @Test
-    public void truncateFirstLine() {
-        assertEquals("abc", TmText.truncateFirstLine("abc", 10), "short text is unchanged");
-        assertEquals("abc", TmText.truncateFirstLine("abc", 3), "length exactly at the limit");
-        assertEquals("abc …", TmText.truncateFirstLine("abcd", 3), "longer than the limit");
-        assertEquals("ab", TmText.truncateFirstLine("ab\nlong second line", 10),
-            "only the first line is considered");
-        assertEquals("", TmText.truncateFirstLine(null, 5));
-    }
-
     @Test
     public void collapseToLine() {
         assertEquals("a b c", TmText.collapseToLine("a\nb\nc", 80), "newlines become spaces");
         assertEquals("abc", TmText.collapseToLine("abc", 3), "length exactly at the limit");
         assertEquals("a b …", TmText.collapseToLine("a\nb\nc", 3),
             "flattened first, then truncated by character count");
+        assertEquals("a & b", TmText.collapseToLine("a\n        &   b", 80),
+            "wrapped-formula indentation collapses to a single space");
+        assertEquals("x", TmText.collapseToLine("\n  x\n  ", 80),
+            "leading and trailing whitespace is trimmed");
         assertEquals("", TmText.collapseToLine(null, 5));
     }