Fix fast-click auto-mode crash: overlapping runs + proof breaking proof listeners

[unp1]

Intended Change

Rapidly clicking the auto-mode / apply-strategy toolbar button can crash the proof with a stray
exception on a SwingWorker thread. The crash turned out to be layered — two independent
causes, both fixed here.

Layer 1 — overlapping auto-mode/macro runs

Starting the automatic proof search (auto mode or a proof macro) while a previous run on the same
proof is still winding down runs two provers on one Proof concurrently and corrupts shared proof
state. The symptom is a stray exception on a SwingWorker thread — e.g. NullPointerException in
NamespaceSet.copy (from Goal.adaptNamespacesNewGoals), AssertionFailure: Expected an empty leaf node, or a null SemisequentTacletAppIndex.succIndex.

Root cause: MediatorProofControl guards re-entry only through the mediator's inAutoMode flag,
which ProofMacroWorker.done() clears. But SwingWorker.done() fires on cancellation, while the
cooperative doInBackground is still applying rules — so the flag drops while the run is still
winding down and the next click starts a second, overlapping run.

This PR adds an explicit re-entrancy guard (AtomicBoolean autoModeActive) in
MediatorProofControl: startAutoMode/runMacro claim it on entry and it is released only when
the worker's background task has truly finished (doInBackground's finally, with a backstop for
the cancelled-before-start case). A new run is refused while one is active or winding down, so two
runs can never prove the same proof at once. It also hardens the analogous guard in
DefaultProofControl (volatile autoModeThread, synchronized runMacro); that control already
released at true completion and the CLI runs blocking, so this is defence-in-depth only.

Layer 2 — a listener must not be able to break the proof

Proofnotifies allRuleAppListeners and ProofTreeListeners with bare dispatch loops, so *any* observer (now or in the future) could break the proof. Rather than have each listener guard itself, this PR isolates them at the firing site: a new Proof.notifyListenershelper wraps every callback — a listener that throws is logged and **unregistered**, and the remaining listeners are still notified.fireRuleAppliedand thefireProof*` dispatches all route through it, so no listener can corrupt the proof.

The problem appeared in this case (but it is not specific to the DependencyTracker) with the slicing extension's always track setting on, DependencyTracker is registered as a RuleAppListener, so its ruleApplied(..) runs inside Goal.apply (via Proof.fireRuleApplied), after the proof tree and namespaces have already been updated for the step.
When tracking failed there — e.g. IllegalStateException: found formula that was not produced by any rule! on a loop-scope invariant while auto mode re-applied the loop-scope rule — the exception
propagated out of Goal.apply, aborting the run mid-application and leaving the proof inconsistent.
That broken state is what then produced the NullPointerException in Goal.adaptNamespacesNewGoals
on the next step.

DependencyTracker additionally records, on a tracking failure, that its dependency graph became
incomplete, so a later analyze() returns no slice rather than one built from a partial graph.

The deeper reason the tracker can miss a loop-scope formula on a re-run is a separate
slicing-correctness question (the naming part was addressed by the #3834 fix already on main); this
PR makes any listener fail safe rather than fatally.

Type of pull request

• Bug fix (non-breaking change which fixes an issue)
• There are changes to the (Java) code

Ensuring quality

• I made sure that introduced/changed code is well documented (javadoc and inline comments).
• I have tested the feature as follows:
  • Layer 1: reproduced the corruption headlessly (two concurrent auto-mode runs on one proof
    corrupt it reliably; interrupting a single run and waiting does not), confirmed that the GUI
    genuinely runs two auto-mode workers on one proof when fast-clicking, and verified that the guard
    prevents the overlap. Final check: fast-clicking the auto button in the GUI no longer crashes.
  • Layer 2: added ProofListenerIsolationTest — a RuleAppListener that always throws neither
    stops the proof from closing nor keeps firing (it is unregistered after its first failure).
    Verified it fails without the guard.
• I have checked that runtime performance has not deteriorated: the re-entrancy guard is a single
  atomic CAS per run start; listener isolation only wraps the existing dispatch in a try/catch — no
  effect on the proof-search hot path.

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

Additional Information and contact(s)

Created with AI tooling support

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.