smaller fixes in proof script treatment

Author: mattulbrich

key.core/src/main/java/de/uka/ilkd/key/macros/ApplyScriptsMacro.java

@@ -170,6 +170,8 @@ public ProofMacroFinishedInfo applyTo(UserInterfaceControl uic, Proof proof,
             pse.getStateMap().putUserData("jml.obtainVarMap", obtainMap);
             pse.getStateMap().getValueInjector().addConverter(JTerm.class, ObtainAwareTerm.class,
                     oat -> oat.resolve(obtainMap, goal.proof().getServices()));
+            pse.getStateMap().getValueInjector().addConverter(boolean.class, ObtainAwareTerm.class,
+                    oat -> Boolean.parseBoolean(oat.term.toString()));
             LOGGER.debug("---- Script");
             LOGGER.debug(renderedProof.stream().map(ScriptCommandAst::asCommandLine)
                     .collect(Collectors.joining("\n")));
@@ -335,11 +337,13 @@ private static ScriptCommandAst renderObtainCommand(ProofCmdContext ctx, Map<Par
                     value = services.getTermBuilder().apply(update, (JTerm) value);
                 }
             }
-            ObtainAwareTerm wrapped = new ObtainAwareTerm((JTerm) value);
+            if (value instanceof JTerm term) {
+                value = new ObtainAwareTerm(term);
+            }
             if (argContext.argLabel != null) {
-                named.put(argContext.argLabel.getText(), wrapped);
+                named.put(argContext.argLabel.getText(), value);
             } else {
-                positional.add(wrapped);
+                positional.add(value);
             }
         }
         return new ScriptCommandAst(ctx.cmd.getText(), named, positional,

key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java

@@ -173,6 +173,7 @@ private static Taclet getLimitedToUnlimitedTaclet(IObserverFunction limited,
                 ImmutableSLList.nil(), unlimitedTerm));
         tacletBuilder.setName(
             MiscTools.toValidTacletName("unlimit " + getUniqueNameForObserver(unlimited)));
+        //tacletBuilder.addRuleSet(new RuleSet(new Name("unlimitObserver")));
         return tacletBuilder.getTaclet();
     }
 

key.core/src/main/java/de/uka/ilkd/key/scripts/ExpandDefCommand.java

@@ -107,7 +107,7 @@ private TacletApp makeRuleApp(Parameters p, EngineState state) throws ScriptExce
 
     public static class Parameters {
         @Option(value = "on")
-        public @Nullable Term on;
+        public @Nullable JTerm on;
         @Option(value = "occ")
         public @Nullable Integer occ;
         @Option(value = "formula")

key.core/src/test/java/de/uka/ilkd/key/scripts/JmlScriptTest.java

@@ -34,7 +34,7 @@ public class JmlScriptTest {
     private static final Logger LOGGER = LoggerFactory.getLogger(JmlScriptTest.class);
 
     // Set this to a specific case to only run that case for debugging
-    private static final String ONLY_CASE = null;
+    private static final String ONLY_CASE = "ObtainFromGoal.java";
 
     static {
         URL url = JmlScriptTest.class.getResource("jml/project.key");