Fix construction of Javac issue dialog (#3008)

Continuation of https://git.key-project.org/key/key/-/merge_requests/637

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/java/Position.java

@@ -6,7 +6,7 @@
  * superceded.
  */
 
-public class Position {
+public class Position implements Comparable<Position> {
 
     /**
      * The line number.
@@ -93,18 +93,6 @@ public boolean equals(Object x) {
         return line == p.line && column == p.column;
     }
 
-    /**
-     * Compares this position with the given object for order. An undefined position is less than
-     * any defined position.
-     *
-     * @param x the position object to compare with.
-     * @return a negative number, zero, or a positive number, if this position is lower than, equals
-     *         to, or higher than the given one.
-     */
-    public int compareTo(Object x) {
-        return compareTo((Position) x);
-    }
-
     /**
      * Compares this position with the given object for order. An undefined position is less than
      * any defined position.
@@ -113,6 +101,7 @@ public int compareTo(Object x) {
      * @return a negative number, zero, or a positive number, if this position is lower than, equals
      *         to, or higher than the given one.
      */
+    @Override
     public int compareTo(Position p) {
         return (line == p.line) ? (column - p.column) : (line - p.line);
     }

key.core/src/main/java/de/uka/ilkd/key/proof/JavaModel.java

@@ -9,6 +9,9 @@
 
 public final class JavaModel {
 
+    /**
+     * Directory of Java source files. May be null if the proof doesn't refer to any Java code.
+     */
     private final String modelDir;
     private final String modelTag;
     private final String descr;

key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java

@@ -60,6 +60,17 @@
 public final class IssueDialog extends JDialog {
     private static final Logger LOGGER = LoggerFactory.getLogger(IssueDialog.class);
 
+    /**
+     * Default text for critical issues (runtime exceptions).
+     */
+    private static final String CRITICAL_ISSUE = "The following exception occurred:";
+    /**
+     * Default text for non-critical issues (JML specification warnings).
+     */
+    private static final String NON_CRITICAL_ISSUE = String.format(
+        "The following non-fatal problems occurred when translating your %s specifications:",
+        SLEnvInput.getLanguage());
+
     /** regex to find web urls in string messages */
     private static final Pattern HTTP_REGEX = Pattern.compile("https?://[^\\s]+");
 
@@ -129,7 +140,20 @@ public final class IssueDialog extends JDialog {
 
     public IssueDialog(Window owner, String title, Set<PositionedIssueString> issues,
             boolean critical) {
-        this(owner, title, issues, critical, null);
+        this(owner, title, critical ? CRITICAL_ISSUE : NON_CRITICAL_ISSUE, issues, critical, null);
+    }
+
+    /**
+     * Create an issue dialog with the given title and description.
+     *
+     * @param owner parent window
+     * @param title window title
+     * @param description description to show
+     * @param issues the issues
+     */
+    public IssueDialog(Window owner, String title, String description,
+            Set<PositionedIssueString> issues) {
+        this(owner, title, description, issues, false, null);
     }
 
     /**
@@ -166,8 +190,34 @@ private static List<PositionedIssueString> decorateHTML(Set<PositionedIssueStrin
         }).collect(Collectors.toList());
     }
 
+    /**
+     * Construct a new issue dialog based on the title, the warnings to show and the exception to
+     * show.
+     *
+     * @param owner parent window
+     * @param title dialog title
+     * @param warnings warnings to show
+     * @param critical whether the issue is critical
+     * @param throwable exception to show (may be null)
+     */
     IssueDialog(Window owner, String title, Set<PositionedIssueString> warnings,
             boolean critical, Throwable throwable) {
+        this(owner, title, critical ? CRITICAL_ISSUE : NON_CRITICAL_ISSUE, warnings, critical,
+            throwable);
+    }
+
+    /**
+     * Construct a new issue dialog given the title, description, warnings and exception.
+     *
+     * @param owner parent window
+     * @param title dialog title
+     * @param head description
+     * @param warnings warnings to show
+     * @param critical criticality of the issue
+     * @param throwable exception to show (may be null)
+     */
+    IssueDialog(Window owner, String title, String head, Set<PositionedIssueString> warnings,
+            boolean critical, Throwable throwable) {
         super(owner, title, ModalityType.APPLICATION_MODAL);
 
         this.throwable = throwable;
@@ -195,14 +245,6 @@ private static List<PositionedIssueString> decorateHTML(Set<PositionedIssueStrin
         // stTextArea
 
         // set descriptive text in top label
-        final String head;
-        if (critical) {
-            head = "The following exception occurred:";
-        } else {
-            head = String.format(
-                "The following non-fatal problems occurred when translating your %s specifications:",
-                SLEnvInput.getLanguage());
-        }
         JLabel label = new JLabel(head);
         label.setBorder(BorderFactory.createEmptyBorder(5, 5, 2, 5));
         add(label, BorderLayout.NORTH);
@@ -719,8 +761,11 @@ public Component getListCellRendererComponent(JList<? extends PositionedString>
                 BorderFactory.createMatteBorder(0, 0, 1, 0, Color.LIGHT_GRAY),
                 BorderFactory.createEmptyBorder(5, 5, 5, 5)));
             if (isSelected) {
-                textPane.setBackground(list.getSelectionBackground());
-                textPane.setForeground(list.getSelectionForeground());
+                // for some reason, this copy is needed to get correct colors
+                Color bg = new Color(list.getSelectionBackground().getRGB());
+                Color fg = new Color(list.getSelectionForeground().getRGB());
+                textPane.setBackground(bg);
+                textPane.setForeground(fg);
             } else {
                 textPane.setBackground(list.getBackground());
                 textPane.setForeground(list.getForeground());

key.ui/src/main/java/de/uka/ilkd/key/gui/PositionedIssueString.java

@@ -12,7 +12,8 @@
  * (text, filename, position) contains a String for additional information which can be used to
  * store a stacktrace if present.
  */
-public class PositionedIssueString extends PositionedString {
+public class PositionedIssueString extends PositionedString
+        implements Comparable<PositionedIssueString> {
 
     public enum Kind {
         ERROR, WARNING, INFO
@@ -73,4 +74,17 @@ public boolean equals(Object o) {
     public int hashCode() {
         return Objects.hash(super.hashCode(), additionalInfo, kind);
     }
+
+    @Override
+    public int compareTo(PositionedIssueString o) {
+        int compareFile = fileName.compareTo(o.fileName);
+        if (compareFile != 0) {
+            return compareFile;
+        }
+        int comparePosition = pos.compareTo(o.pos);
+        if (comparePosition != 0) {
+            return comparePosition;
+        }
+        return kind.compareTo(o.kind);
+    }
 }