Skip to content

Commit 382f4ce

Browse files
committed
fixing a bug regarding proof script application
1 parent 5d3fcc1 commit 382f4ce

1 file changed

Lines changed: 7 additions & 4 deletions

File tree

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

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -23,6 +23,7 @@
2323
import de.uka.ilkd.key.scripts.ProofScriptEngine;
2424
import de.uka.ilkd.key.scripts.ScriptException;
2525

26+
import org.checkerframework.checker.nullness.qual.MonotonicNonNull;
2627
import org.jspecify.annotations.NullMarked;
2728
import org.jspecify.annotations.Nullable;
2829
import org.slf4j.Logger;
@@ -47,7 +48,8 @@ public class ProofScriptWorker extends SwingWorker<@Nullable Object, ProofScript
4748
/**
4849
* The proof script engine.
4950
*/
50-
private final ProofScriptEngine engine;
51+
private @MonotonicNonNull ProofScriptEngine engine;
52+
5153
private final JDialog monitor = new JDialog(MainWindow.getInstance(),
5254
"Running Script ...", ModalityType.MODELESS);
5355
private final JTextArea logArea = new JTextArea();
@@ -76,13 +78,13 @@ public ProofScriptWorker(KeYMediator mediator, KeyAst.ProofScript script,
7678
this.mediator = mediator;
7779
this.script = script;
7880
this.initiallySelectedGoal = initiallySelectedGoal;
79-
engine = new ProofScriptEngine(initiallySelectedGoal.proof());
80-
engine.setInitiallySelectedGoal(initiallySelectedGoal);
8181
}
8282

8383
@Override
8484
protected @Nullable Object doInBackground() throws Exception {
8585
try {
86+
engine = new ProofScriptEngine(mediator.getSelectedProof());
87+
engine.setInitiallySelectedGoal(initiallySelectedGoal);
8688
engine.setCommandMonitor(observer);
8789
engine.execute(mediator.getUI(), script);
8890
} catch (InterruptedException ex) {
@@ -173,7 +175,8 @@ public void done() {
173175

174176
private void selectGoalOrNode() {
175177
final KeYSelectionModel selectionModel = mediator.getSelectionModel();
176-
if (!mediator.getSelectedProof().closed()) {
178+
final Proof proof = mediator.getSelectedProof();
179+
if (proof != null && !proof.closed() && engine != null) {
177180
try {
178181
selectionModel
179182
.setSelectedGoal(engine.getStateMap().getFirstOpenAutomaticGoal());

0 commit comments

Comments
 (0)