Try to achieve a better parser error message

[wadoon]

This PR removes the LL(*) fallback from the ParsingFacade to achieve better error message.

[codecov[bot]]

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Comparison is base (1064b30) 37.72% compared to head (d9de961) 37.72%.

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #3406 +/- ## ============================================ - Coverage 37.72% 37.72% -0.01% Complexity 17017 17017 ============================================ Files 2076 2076 Lines 126944 126939 -5 Branches 21379 21379 ============================================ - Hits 47891 47886 -5 Misses 73155 73155 Partials 5898 5898 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

[wadoon]

In your example the totally unclear SLL error message is still shown. Why? If the other is the "real" error message, can we restrict ourselves to it?

It is not final as I did not understand much of ANTLR internals.

Error messages are now caught up in the ErrorStrategy, so e.g., I lose have the ANTLR error messages not available anymore.

[wadoon]

The main question is: Is the KeY grammar within SLL? The internet says:

Strong LL Grammar (SLL):SLL grammars are a subset of LL(k) grammars, which are a more powerful class of grammars than CFGs.LL(k) grammars are capable of describing languages that are not context-free, as they can consider a limited amount of lookahead tokens (k tokens) to make parsing decisions based on context.SLL grammars are a strict subset of LL(k) grammars that are characterized by having a unique alternative for each production when the parser looks at the first k tokens of input.SLL parsers can be more efficient than general LL(k) parsers, but they are more restricted in the grammars they can parse.

I would guess so.

[mattulbrich]

Rosenkrantz,Stearns: Properties of deterministic top-down grammars

[wadoon]

SLL is sufficient for the KeY taclet base.

Should we just drop LL mode?

[wadoon]

KaKeY decision: Fallback to LL(*) will be removed.

[wadoon]

    @Override
    public Token recoverInline(Parser recognizer) throws RecognitionException {
        InputMismatchException e = new InputMismatchException(recognizer);
        for (ParserRuleContext context = recognizer.getContext(); context != null; context = context.getParent()) {
            context.exception = e;
        }
        var tok = e.getOffendingToken();

        var message = "I got offended by the token '%s'. Expected tokens are: %s".formatted(tok,
                e.getExpectedTokens().toString(recognizer.getVocabulary()));

        syntaxError(recognizer, e.getOffendingToken(),
                tok.getLine(), tok.getCharPositionInLine(), message, e);
        throw new ParseCancellationException(e);
    }

    @Override
    public void recover(Parser recognizer, RecognitionException e) throws RecognitionException {
        for (ParserRuleContext context = recognizer.getContext(); context != null; context = context.getParent()) {
            context.exception = e;
        }
        var tok = e.getOffendingToken();
        final var parseCancellationException = new ParseCancellationException(e);

        syntaxError(recognizer, e.getOffendingToken(),
                tok.getLine(), tok.getCharPositionInLine(), parseCancellationException.getMessage(), e);

        throw parseCancellationException;
    }

[wadoon]

closed in favor of hekeython2 approaches.