From a49cf56be7b6c0f369d1e95aab172e99f20e3ac3 Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 14 Jun 2024 09:40:26 +0200 Subject: [PATCH] Fix loading of taclet proof obligations (issue #3477) * This commit fixes an NPE when loading * This commit fixes missing or inconsistent selection of loaded proof obligation --- .../uka/ilkd/key/taclettranslation/lemma/EmptyEnvInput.java | 4 ++-- .../de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/EmptyEnvInput.java b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/EmptyEnvInput.java index 74338e792e6..2c2d47deed2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/EmptyEnvInput.java +++ b/key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/EmptyEnvInput.java @@ -11,6 +11,7 @@ import de.uka.ilkd.key.proof.io.AbstractEnvInput; import de.uka.ilkd.key.speclang.PositionedString; +import org.key_project.util.collection.DefaultImmutableSet; import org.key_project.util.collection.ImmutableSet; public class EmptyEnvInput extends AbstractEnvInput { @@ -21,8 +22,7 @@ public EmptyEnvInput(Profile profile) { @Override public ImmutableSet read() throws ProofInputException { - // nothing to to do - return null; + return DefaultImmutableSet.nil(); } @Override diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java index cf1fc6ae46b..a47a606203b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LemmaGenerationAction.java @@ -233,6 +233,7 @@ public void doStopped(ProofAggregate p, ImmutableSet taclets, getMediator().startInterface(true); if (p != null) { mainWindow.getUserInterface().registerProofAggregate(p); + mainWindow.getMediator().getSelectionModel().setSelectedProof(p.getFirstProof()); } }