Nicer error message for parse errors

key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java

@@ -130,15 +130,16 @@ public static KeyAst.File parseFile(CharStream stream) {
         KeYParser p = createParser(stream);
 
         p.getInterpreter().setPredictionMode(PredictionMode.SLL);
-        // we don't want error messages or recovery during first try
         p.removeErrorListeners();
         p.setErrorHandler(new BailErrorStrategy());
         KeYParser.FileContext ctx;
         try {
             ctx = p.file();
         } catch (ParseCancellationException ex) {
             LOGGER.warn("SLL was not enough");
+            stream.seek(0);
             p = createParser(stream);
+            p.setErrorHandler(new BailErrorStrategy());
             ctx = p.file();
         }
 

key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java

@@ -3,7 +3,9 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.util;
 
+import java.io.File;
 import java.net.MalformedURLException;
+import java.nio.file.Paths;
 import java.util.Optional;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
@@ -15,6 +17,11 @@
 import de.uka.ilkd.key.parser.proofjava.TokenMgrError;
 import de.uka.ilkd.key.util.parsing.HasLocation;
 
+import org.antlr.v4.runtime.InputMismatchException;
+import org.antlr.v4.runtime.IntStream;
+import org.antlr.v4.runtime.NoViableAltException;
+import org.antlr.v4.runtime.Vocabulary;
+import org.antlr.v4.runtime.misc.IntervalSet;
 import org.jspecify.annotations.NonNull;
 import org.jspecify.annotations.Nullable;
 
@@ -38,6 +45,46 @@ public final class ExceptionTools {
     private ExceptionTools() {
     }
 
+    public static String getNiceMessage(InputMismatchException ime) {
+        return getNiceMessageInternal(ime.getInputStream(), ime.getOffendingToken(),
+            ime.getRecognizer().getVocabulary(), ime.getExpectedTokens());
+    }
+
+    public static String getNiceMessage(NoViableAltException ime) {
+        return getNiceMessageInternal(ime.getInputStream(), ime.getOffendingToken(),
+            ime.getRecognizer().getVocabulary(), ime.getExpectedTokens());
+    }
+
+    private static String getNiceMessageInternal(IntStream inputStream,
+            org.antlr.v4.runtime.Token offendingToken, Vocabulary vocabulary,
+            IntervalSet expectedTokens) {
+        StringBuilder sb = new StringBuilder();
+
+        sb.append("Syntax error in input file ");
+        var inFile = new File(inputStream.getSourceName());
+        sb.append(inFile.getName());
+        sb.append("\n");
+        sb.append("Line: ");
+        sb.append(offendingToken.getLine());
+        sb.append(" Character: ");
+        sb.append(offendingToken.getCharPositionInLine() + 1);
+
+        sb.append("\n");
+        sb.append("Found token which was not expected: ");
+        sb.append(vocabulary.getDisplayName(offendingToken.getType()));
+        sb.append("\n");
+        sb.append("Expected token type(s): ");
+        for (var interval : expectedTokens.getIntervals()) {
+            for (int i = interval.a; i <= interval.b; i++) {
+                sb.append(vocabulary.getDisplayName(i));
+                sb.append("\n");
+            }
+        }
+
+        return sb.toString();
+    }
+
+
     /**
      * Tries to resolve the location (i.e., file name, line, and column) from a parsing exception.
      * Result may be null.
@@ -56,6 +103,10 @@ public static Optional<Location> getLocation(@NonNull Throwable exc)
             return Optional.ofNullable(getLocation((ParseException) exc));
         } else if (exc instanceof TokenMgrError) {
             return Optional.ofNullable(getLocation((TokenMgrError) exc));
+        } else if (exc instanceof InputMismatchException ime) {
+            return Optional.ofNullable(getLocation(ime));
+        } else if (exc instanceof NoViableAltException nvae) {
+            return Optional.ofNullable(getLocation(nvae));
         }
 
         if (exc.getCause() != null) {
@@ -73,6 +124,26 @@ private static Location getLocation(ParseException exc) {
                 : new Location(null, Position.fromToken(token.next));
     }
 
+    private static Location getLocation(NoViableAltException exc) {
+        var token = exc.getOffendingToken();
+
+        return token == null ? null
+                : new Location(
+                    Paths.get(Paths.get("").toString(), exc.getInputStream().getSourceName())
+                            .normalize().toUri(),
+                    Position.fromToken(token));
+    }
+
+    private static Location getLocation(InputMismatchException exc) {
+        var token = exc.getOffendingToken();
+
+        return token == null ? null
+                : new Location(
+                    Paths.get(Paths.get("").toString(), exc.getInputStream().getSourceName())
+                            .normalize().toUri(),
+                    Position.fromToken(token));
+    }
+
     private static Location getLocation(TokenMgrError exc) {
         Matcher m = TOKEN_MGR_ERR_PATTERN.matcher(exc.getMessage());
         if (m.find()) {

key.core/src/test/java/de/uka/ilkd/key/util/ExceptionToolsTest.java

@@ -0,0 +1,56 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+package de.uka.ilkd.key.util;
+
+import java.io.File;
+import java.io.IOException;
+import java.net.MalformedURLException;
+import java.net.URISyntaxException;
+
+import de.uka.ilkd.key.nparser.ParsingFacade;
+import de.uka.ilkd.key.parser.Location;
+import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter;
+
+import org.key_project.util.helper.FindResources;
+
+import org.antlr.v4.runtime.InputMismatchException;
+import org.antlr.v4.runtime.misc.ParseCancellationException;
+import org.junit.jupiter.api.Test;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+class ExceptionToolsTest {
+    public static final File testCaseDirectory = FindResources.getTestCasesDirectory();
+
+    @Test
+    void missingSemicolon() throws MalformedURLException, URISyntaxException {
+        var fileToRead = testCaseDirectory.toPath();
+        fileToRead = fileToRead.resolve("parserErrorTest/missing_semicolon.key");
+        try {
+            var result = ParsingFacade.parseFile(fileToRead);
+            fail("should fail to parse");
+        } catch (IOException e) {
+            throw new RuntimeException(e);
+        } catch (ParseCancellationException exc) {
+            InputMismatchException ime = (InputMismatchException) exc.getCause();
+            String message = """
+                    Syntax error in input file missing_semicolon.key
+                    Line: 6 Character: 1
+                    Found token which was not expected: '}'
+                    Expected token type(s): ';'
+                    """;
+            String resultMessage = ExceptionTools.getNiceMessage(ime);
+            assertEquals(message, resultMessage);
+
+            Location loc = ExceptionTools.getLocation(ime).get();
+            assertEquals(6, loc.getPosition().line());
+            assertEquals(1, loc.getPosition().column());
+            assertEquals(fileToRead.toUri(), loc.fileUri());
+        } catch (SyntaxErrorReporter.ParserException exception) {
+            Location loc = ExceptionTools.getLocation(exception).get();
+            assertEquals(6, loc.getPosition().line());
+            assertEquals(1, loc.getPosition().column());
+        }
+    }
+}

key.core/src/test/resources/testcase/parserErrorTest/missing_semicolon.key

@@ -0,0 +1,10 @@
+\rules {
+   missingSemicolon {
+      \find(0=0)
+      \replacewith(1=1)
+  }
+}
+\problem {
+0=0
+}
+

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

@@ -41,6 +41,9 @@
 import org.key_project.util.java.StringUtil;
 import org.key_project.util.java.SwingUtil;
 
+import org.antlr.v4.runtime.InputMismatchException;
+import org.antlr.v4.runtime.NoViableAltException;
+import org.antlr.v4.runtime.misc.ParseCancellationException;
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
 
@@ -600,6 +603,17 @@ private static PositionedIssueString extractMessage(Throwable exception) {
             String message = exception.getMessage();
             String info = sw.toString();
 
+            if (exception instanceof ParseCancellationException) {
+                exception = exception.getCause();
+            }
+
+            if (exception instanceof InputMismatchException ime) {
+                message = ExceptionTools.getNiceMessage(ime);
+            }
+            if (exception instanceof NoViableAltException nvae) {
+                message = ExceptionTools.getNiceMessage(nvae);
+            }
+
             // also add message of the cause to the string if available
             if (exception.getCause() != null) {
                 String causeMessage = exception.getCause().getMessage();