Fix loading of taclet proof obligations (issue #3477) (#3481)

KeYProject · Jun 14, 2024 · 19f83d3 · 19f83d3
2 parents 1ef5c70 + 3e8b37b
commit 19f83d3
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 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
@@ -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<PositionedString> 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
@@ -233,6 +233,8 @@ public void doStopped(ProofAggregate p, ImmutableSet<Taclet> taclets,
                     getMediator().startInterface(true);
                     if (p != null) {
                         mainWindow.getUserInterface().registerProofAggregate(p);
+                        mainWindow.getMediator().getSelectionModel()
+                                .setSelectedProof(p.getFirstProof());
                     }
                 }