Further improvements on error message reporting#3859
Merged
Conversation
Improve the messages produced by the proof loading/replay framework so they
state the actual problem instead of leaking internal objects or surfacing only
the first of several failures.
- PosInOccurrence: add a human-readable toString ("term at <pos> of formula
<f> in the antecedent/succedent"). Previously the default Object form
(PosInOccurrence@<hash>) leaked into replay error dialogs.
- IntermediateProofReplayer: actionable text for the two "Wrong position
information" cases; include the node serial in the otherwise context-free
catch-all; drop a whole-namespace dump from a parse-value error; downgrade the
tolerated "not in uninsts" inconsistency to a clear warn (with a comment on why
it is tolerated); grammar fix.
- ProblemLoaderException can now bundle several sub-problems, and
ExceptionTools.getMessages expands them so every failed rule application is
reported (summary + one entry each) instead of only the first;
WindowUserInterfaceControl throws the bundle on a partial replay.
- IntermediatePresentationProofFileParser: wrap a ClassNotFoundException with the
offending type name.
- IssueDialog.showExceptionDialog: neutral "Error" title instead of the
misleading "Parser Error" (the method has ~27 mostly non-parser callers).
…y errors - TestPosInOcc#testToStringIsReadable guards against the default Object representation (PosInOccurrence@<hash>) leaking into user-facing messages. - ExceptionToolsTest#getMessagesExpandsBundledProblemLoaderException: every bundled sub-problem (e.g. all failed rule applications) is reported, not just the first.
…jargon
- JavaService.simplifyJavaParserMessage: collapse the (possibly multi-line)
offending token to a single line and shorten it if very long; drop JavaCard /
schema-internal alternatives ("#abortJavaCardTransaction", ...) from the
"expected one of" list so the relevant alternatives are shown.
- New JavaService.humanizeJavaParserJargon: rewrite "Unsolved symbol : X" into the
user-facing wording KeY already uses ("Cannot resolve 'X'. No variable, field,
or type with this name is in scope here (check for typos)."). Applied in
simplifyJavaParserMessage and to the reason of a failed Java block in
ExpressionBuilder, where the type-resolution path previously leaked the raw
jargon.
…nizing - JavaServiceMessageTest: dropping JavaCard/schema alternatives, collapsing a multi-line offending token, and humanizing "Unsolved symbol". - TestJavaDLASTExtensions: assert the user-facing "Cannot resolve" wording for an unresolved type in a Java block (cause chain unchanged).
…e first ParsingFacade.parseFile keeps the fast SLL+bail pass for the common case; when it fails it now re-parses with LL and ANTLR's default error recovery, which collects all syntax errors. To avoid regressing the polished single-error message and position, the bail-path exception is kept when recovery finds exactly one error; the full list is reported only when there are several (zero errors means SLL was merely insufficient and the LL parse actually succeeded). - SyntaxErrorReporter: expose errorCount(), ParserException.getErrors(), and per-error SyntaxError.getMessage()/getLocation(). - ExceptionTools.getMessages: expand a multi-error ParserException into one located message per error, so the dialog lists them separately and the console prints each (via the unified extraction, both get this for free).
MultiSyntaxErrorTest: two independent errors are both reported (each with its own line); a single error keeps the one-message bail path (regression guard).
- IssueDialog: the location field ("URL: ...") is now a clickable link (hand
cursor, link colour) that opens the source file at the selected issue; the
"Edit File" action is rebound to the selected issue in updatePreview so it
jumps to that issue's location rather than always the first one reported
(relevant now that several issues can be listed).
- EditSourceFileAction: add a constructor taking an explicit (Location, message)
so the editor can open at a specific issue; the existing Throwable constructor
is unchanged. The "no positional information" guard now also covers a location
without a file URI.
…sages cleanFoundToken matched "unexpected \"" with a single space, but JavaParser emits "Found \"...\"" (two spaces) - so the offending multi-line token in real messages (e.g. the top-level entry for a broken \javaSource file) was not collapsed; only the hand-built single-space test input was. Match one-or-more spaces, and use the realistic two-space form in the test.
unp1
added
the
Error Reporting
auto-merge was automatically disabled
June 23, 2026 08:31
Pull request was converted to draft
…rst open updatePreview's scroll-to-error ran via invokeLater during construction, before the source preview was laid out, so modelToView2D returned null and the scroll was skipped on the initial show - the selected issue's line became visible only after clicking another issue and back. Remember the offset and re-run the scroll from componentShown (when the pane is finally laid out).
… insertion point In the multi-error path the recovered syntax errors were located at the next, unexpected token instead of the insertion point of the missing ';'/')'/... (the single-error/bail path already does this). LL recovery yields a broader expected set than SLL, so the strict "only a closing token is expected" check never fired. - ExceptionTools: extract insertionPointFor(ime, onlyClosing); the single-error path keeps the strict (only-closing) check (unchanged positions), while the multi-error path accepts a closing token being among the expected ones. - SyntaxErrorReporter: for an InputMismatch, redirect the reported position to that insertion point. - MultiSyntaxErrorTest now asserts the two errors mark lines 2 and 4 (the missing ';'), not 3 and 5.
unp1
force-pushed
the
improveErrorMessages2
branch
2 times, most recently
from
a0ce881 to
e553154
Compare
wadoon
approved these changes
Jun 23, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Follow-up round of error-reporting improvements, focused on KeY's file-loading and proof-replay framework: clearer messages, all errors reported (not just the first), and clickable error locations.
KeY_error_report_round2.pdf with a short before/after comparison on what changed.
Intended Change
This continues the error-reporting work (round 1 is already on
main) and targets the loading and proof-replay path:PosInOccurrenceobject (…@<hash>) into the dialog.PosInOccurrencenow has a readabletoString, and the replay messages are actionable. A partially-replayable proof now reports every failed rule application instead of only the first (ProblemLoaderExceptioncan bundle them;ExceptionTools.getMessagesexpands them, so the console benefits too).Unsolved symbol : Xis rewritten to the sameCannot resolve 'X'. …wording KeY already uses elsewhere..keyparsing keeps the fast SLL+bail pass for a single error (so the polished single-error message and position are unchanged — no regression), but on failure re-parses with LL + recovery and reports every independent syntax error, each with its own location.Type of pull request
Ensuring quality
PosInOccurrence.toString, bundled replay errors, JavaParser message tidy-up, multi syntax-error reporting); existing suites stay green (e.g.KeYParserExceptionTest, save/load round-trips); compiled with-DENABLE_NULLNESS=true; spotless-clean; and reviewed via the attached before/after report (real screenshots atorigin/mainvs this branch). Full RAP regression runs on CI.Additional information and contact(s)
Each change is a reviewable code-then-tests commit. Behaviour-affecting parser/replay messages are covered by tests, and the single-error
.keypath is intentionally left untouched (verified no regression).PR created with support of AI tooling.
The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.