Small feature: go to node with given serial number

[WolframPfeifer]

This PR adds a small feature: An entry "Go to Node..." to the proof tree settings menu (gear symbol) and the proof menu which prompts the user jumps to the proof node with the given serial number (if it exists in the proof).

This is particularly useful with the slicing and caching extensions (but also with proof replay), when you receive an error message with a node number.

Note that one could also use the "Search in Proof Tree" as a workaround (which I noticed only after implementing the feature), but this is less precise: If you search for "100" for instance, also the nodes "1001", "1002", ..., "1100", etc. are found.

Type of pull request

• New feature (non-breaking change which adds functionality)
• 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: Manually via the GUI

Additional information and contact(s)

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

[mattulbrich]

Nice feature! Thanks!
I have added a bit of functionality which should be self-explanatory by trying it out.
[curated ChatGPT code]

[mattulbrich]

Like it! thanks!

@WolframPfeifer please check the changes are improvements.

[wadoon]

Reviewed PR #3963 ("Small feature: go to node with given serial number") — full diff plus surrounding code at the PR head (0f4ce623), including KeYSelectionModel, MainWindow, KeyStrokeSettings, SearchModeChangeAction, NodeInfo and its callers.

---

Medium severity

1. Ctrl+G accelerators conflict with an existing action

key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java + key.ui/.../actions/SearchModeChangeAction.java

defineDefault(GotoNodeAction.class, KeyEvent.VK_G, SHORTCUT_KEY_MASK);

But SearchModeChangeAction (for SearchMode.REGROUP, added to the same proof menu in MainWindow) already binds Ctrl+G:

} else if (mode == SequentViewSearchBar.SearchMode.REGROUP) {
    setAcceleratorLetter(KeyEvent.VK_G);
}

Both menu items are present simultaneously in the proof menu (GotoNodeAction directly, the Search Mode items in the "Search Mode" submenu), so the two Ctrl+G bindings shadow each other; depending on Swing registration order, one of them silently stops working. The KeyStrokeSettings comment explicitly says defaults are centralized "to detect and prevent possible duplicates" — this hard-coded binding bypasses that. Suggest using a different combination for the new action (e.g. Ctrl+Shift+G, which is unassigned) or moving the SearchModeChangeAction accelerator into KeyStrokeSettings so conflicts are visible.

2. setSelectedNodeBySerialNr does the selection twice and fires a misleading duplicate event

key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java

goalIsValid = false;
selectedNode = node;
selectedSequent = selectedNode.sequent();
selectedRuleApp = selectedNode.getAppliedRuleApp();
setSelectedNode(node);                     // sets the same fields again and fires an event
fireSelectedNodeChanged(previousSelectedNode);  // and fires again

setSelectedNode(node) already performs all four assignments and fires selectedNodeChanged itself. Because selectedNode was already set to node, the inner call fires a first event whose previous-selected node equals the new one (a semantically wrong "changed" event where old == new), and then the outer method fires a second, correct event. Every KeYSelectionListener (ProofTreeView, GoalList, TaskTree, MainWindow, SelectionHistory) is therefore notified twice per goto; SelectionHistory happens to deduplicate, but the other listeners do redundant work, and the first event is wrong regardless.

The method can simply be:

if (proof == null) return false;
Node node = proof.findAny(n -> n.serialNr() == serialNr);
if (node == null) return false;
setSelectedNode(node);
return true;

3. showGotoNodeDialog NPEs when no proof is loaded

key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java

final var currentProof = mediator != null ? mediator.getSelectedProof() : null;
...
for (Iterator<Node> it = currentProof.root().subtreeIterator(); ...

mediator is effectively never null (there is an assert m != null in setMediator), but getSelectedProof() can be null — the codebase guards against exactly this elsewhere in the same class (autoModeStopped returns early if mediator.getSelectedProof() == null). The new dialog dereferences currentProof unconditionally. The GotoNodeAction menu entry is guarded by enableWhenProofLoaded, but the gear-menu button added in ProofTreeSettingsMenuFactory is not, so when the proof tree is shown with no selected proof (e.g. fresh start or after closing the last proof), that entry NPEs inside the dialog instead of doing nothing. Add a currentProof == null early return.

Low severity / informational

4. Notes dialog behavior change (ProofTreePopupFactory)

The item was renamed "Edit Notes..." → "Set bookmark/Annotate ...", and an empty/blank note now prefills with "Bookmark %d". Intended (it feeds the new bookmarks list in the dialog), but note the semantic change: pressing OK on an empty note now silently stores a note where previously nothing (or an empty string) was written — a script or user relying on note-free nodes would see different behavior. Fine if deliberate.

5. Performance on very large proofs

showGotoNodeDialog iterates the entire proof (subtreeIterator) on every dialog opening to collect noted nodes, even when the user just wants to type a number. The PR's stated use case (slicing/caching, large proofs) is exactly where an O(n) full-tree scan per dialog open is most noticeable. Consider bounding the scan (e.g. stop after N noted nodes) or collecting lazily.

6. NodeInfo nullability annotations — correct

Making notes/setNotes/getNotes @Nullable matches reality: setNotes(null) is already called by the delete-notes path, OutputStreamProofSaver.notes2Proof and the ProofTreeView renderers already null-check. Good cleanup, no issue.

---

Summary

The feature is small and mostly clean, but before merge: resolve the Ctrl+G conflict (finding 1), simplify setSelectedNodeBySerialNr to avoid the duplicated selection and double/misleading events (finding 2), and add the missing null-proof guard in the dialog (finding 3). No automated tests cover the new selection-model path — given it's GUI code that's acceptable, but the double-event is the kind of thing a quick unit test of setSelectedNodeBySerialNr would have caught.