fix Taclet options activation

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java

@@ -292,7 +292,6 @@ private Vertex getVertexFor(Pair<Sort, IObserverFunction> vertexCore, ClassAxiom
      */
     private void registerClassAxiomTaclets(KeYJavaType selfKJT, InitConfig proofConfig) {
         final ImmutableSet<ClassAxiom> axioms = selectClassAxioms(selfKJT);
-        var choices = Collections.unmodifiableSet(proofConfig.getActivatedChoices().toSet());
         for (ClassAxiom axiom : axioms) {
             final Vertex node = getVertexFor(axiom.getKJT().getSort(), axiom.getTarget(), axiom);
             if (node.index == -1) {
@@ -305,9 +304,9 @@ private void registerClassAxiomTaclets(KeYJavaType selfKJT, InitConfig proofConf
                 proofConfig.getServices())) {
                 assert axiomTaclet != null : "class axiom returned null taclet: " + axiom.getName();
                 // only include if choices are appropriate
-                if (axiomTaclet.getChoices().eval(choices)) {
-                    register(axiomTaclet, proofConfig);
-                }
+                // weigl: register always! choices are evaluated as late as possible.
+                // This would technically allow to change Taclet options after loading.
+                register(axiomTaclet, proofConfig);
             }
         }
 

key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java

@@ -78,7 +78,7 @@ public class InitConfig {
     private Map<Taclet, TacletBuilder<? extends Taclet>> taclet2Builder = new LinkedHashMap<>();
 
     /** HashMap for quick lookups taclet name->taclet */
-    private Map<Name, Taclet> activatedTacletCache = null;
+    private @Nullable Map<Name, Taclet> activatedTacletCache = null;
 
     /** the fileRepo which is responsible for consistency between source code and proof */
     private FileRepo fileRepo;
@@ -134,7 +134,7 @@ public Profile getProfile() {
     public void addCategory2DefaultChoices(@NonNull Map<String, String> init) {
         boolean changed = false;
         for (final Map.Entry<String, String> entry : init.entrySet()) {
-            final Choice c = choiceNS().lookup(new Name(entry.getKey()));
+            final Choice c = choiceNS().lookup(new Name(entry.getValue()));
             if (c != null && !category2DefaultChoice.containsKey(c.category())) {
                 changed = true;
                 category2DefaultChoice.put(c.category(), c);

key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java

@@ -153,14 +153,21 @@ private void loadProof(Proof selectedProof) throws RuntimeException {
             lblStatus.setText("Javac runs");
             lblStatus.setIcon(ICON_WAIT.get(16));
 
-            CompletableFuture<List<PositionedIssueString>> task =
-                JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath);
+
             try {
-                task.thenAccept(it -> SwingUtilities.invokeLater(() -> {
-                    lblStatus.setText("Javac finished");
-                    data.issues = it;
-                    updateLabel(data);
-                })).get();
+                try {
+                    CompletableFuture<List<PositionedIssueString>> task =
+                        JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath,
+                            javaPath);
+
+                    task.thenAccept(it -> SwingUtilities.invokeLater(() -> {
+                        lblStatus.setText("Javac finished");
+                        data.issues = it;
+                        updateLabel(data);
+                    })).get();
+                } catch (IllegalArgumentException iae) {
+                    LOGGER.error("Javac check failed {}", iae.getMessage());
+                }
             } catch (InterruptedException | ExecutionException ex) {
                 throw new RuntimeException(ex);
             }