address reviewer comments

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java

@@ -50,7 +50,7 @@ private ParsingFacade() {
      * <b>The use of this method is discouraged and should be avoided in all high level
      * scenarios.</b>
      *
-     * @param ast a key ast object
+     * @param ast a {@link KeyAst} object
      * @param <T> parse tree type
      * @return the {@link ParserRuleContext} inside the given ast object.
      */

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

@@ -3,37 +3,37 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.scripts;
 
-import java.util.Collections;
-import java.util.List;
-import java.util.Map;
-import java.util.Objects;
-
 import de.uka.ilkd.key.parser.Location;
-
+import org.antlr.v4.runtime.CharStream;
 import org.antlr.v4.runtime.ParserRuleContext;
 import org.jspecify.annotations.NullMarked;
 import org.jspecify.annotations.Nullable;
 
+import java.util.Collections;
+import java.util.List;
+import java.util.Map;
+import java.util.Objects;
+
 import static java.util.stream.Collectors.joining;
 
 /// This class represents is the AST of a proof script command.
 ///
 /// It is an abstraction to the commands of following structure:
 /// ```
-/// <commandName> key_1=value_1 ... key_m=value_m positionalArgs_1 ... positionalArgs_n {
+/// <commandName> key_1:value_1 ... key_m:value_m positionalArgs_1 ... positionalArgs_n {
 /// commands_0; ...; commands_k;
-/// }
-/// ```
+///}
+///```
 ///
-/// @param commandName the name of the command, e.g., "macro" for `macro auto;`
-/// @param namedArgs a map of the given named arguments and values.
-/// If a named argument is not given, the entry should be missing in the map. Null-values are not
-/// allowed.
+/// @param commandName    the name of the command, e.g., "macro" for `macro auto;`
+/// @param namedArgs      a map of the given named arguments and values.
+///                       If a named argument is not given, the entry should be missing in the map. Null-values are not
+///                       allowed.
 /// @param positionalArgs the list of given positional arguments
-/// @param commands a nullable block of proof script arguments (represents "higher-order proof
-/// scripts").
-/// If null, the block was omitted syntactically in contrast to an empty list.
-/// @param location the location of this command for error reporting.
+/// @param commands       a nullable block of proof script arguments (represents "higher-order proof
+///                       scripts").
+///                       If null, the block was omitted syntactically in contrast to an empty list.
+/// @param location       the location of this command for error reporting.
 /// @author Alexander Weigl
 /// @version 1 (14.03.25)
 @NullMarked
@@ -45,26 +45,30 @@ public record ScriptCommandAst(
         @Nullable Location location) {
 
     public ScriptCommandAst(String commandName, Map<String, Object> namedArgs,
-            List<Object> positionalArgs) {
+                            List<Object> positionalArgs) {
         this(commandName, namedArgs, positionalArgs, Collections.emptyList(), null);
     }
 
+    /// Renders this command a parsable string representation. The order of the arguments is as follows:
+    /// key-value arguments, positional arguments and the additional script block.
+    ///
+    /// @see de.uka.ilkd.key.nparser.ParsingFacade#parseScript(CharStream)
     public String asCommandLine() {
         return commandName + ' ' +
                 namedArgs.entrySet().stream()
-                        .map(it -> it.getKey() + ": " + humanString(it.getValue()))
+                        .map(it -> it.getKey() + ": " + asReadableString(it.getValue()))
                         .collect(joining(" "))
                 + ' '
-                + positionalArgs.stream().map(ScriptCommandAst::humanString).collect(joining(" "))
+                + positionalArgs.stream().map(ScriptCommandAst::asReadableString).collect(joining(" "))
                 + (commands != null
-                        ? " {"
-                            + commands.stream().map(ScriptCommandAst::asCommandLine)
-                                    .collect(joining("\n"))
-                            + "\n}"
-                        : ";");
+                ? " {"
+                + commands.stream().map(ScriptCommandAst::asCommandLine)
+                .collect(joining("\n"))
+                + "\n}"
+                : ";");
     }
 
-    public static String humanString(Object value) {
+    public static String asReadableString(Object value) {
         if (value instanceof ParserRuleContext ctx) {
             return ctx.getText();
         }

key.core/tacletProofs/seqPerm2/Taclet_schiffl_thm_1.proof

@@ -47,75 +47,74 @@
 
 \proofScript {
 macro "split-prop";
-rule schiffl_lemma_2 formula: (seqPerm(f_s,f_t));
-instantiate hide var: x with: (f_x);
-instantiate hide var: y with: (f_y);
+rule schiffl_lemma_2 formula=(seqPerm(f_s,f_t));
+instantiate hide var=x with=(f_x);
+instantiate hide var=y with=(f_y);
 rule impLeft;
 tryclose branch;
 rule exLeft;
 macro "split-prop";
-rule seqPermDef occ: 1;
+rule seqPermDef occ=1;
 rule andRight;
 tryclose branch;
-instantiate hide var: s with: (r_0);
+instantiate hide var=s with=(r_0);
 rule andRight;
 tryclose branch;
 rule allRight;
 rule impRight;
-instantiate hide var: iv with: (iv_0);
+instantiate hide var=iv with=(iv_0);
 rule impLeft;
 tryclose branch;
 rule andLeft;
 rule seqNPermRange;
-instantiate hide var: iv with: (iv_0);
+instantiate hide var=iv with=(iv_0);
 rule impLeft;
 tryclose branch;
 rule andLeft;
 rule andLeft;
 rule seqNPermRange;
-instantiate hide var: iv with: (f_x);
+instantiate hide var=iv with=(f_x);
 rule impLeft;
 tryclose branch;
-// Wrong branch is selected here. Goal 1 instead of Goal 2
 rule andLeft;
 rule andLeft;
 rule seqNPermRange;
-instantiate hide var: iv with: (f_y);
+instantiate hide var=iv with=(f_y);
 rule impLeft;
 tryclose branch;
 rule andLeft;
 rule andLeft;
-rule getOfSeqDef occ: 0;
+rule getOfSeqDef occ=0;
 rule getOfSeqDef;
-rule ifthenelse_split occ: 0;
-rule andLeft occ: 0;
-rule sub_zero_2 occ: 0;
-rule ifthenelse_split occ: 2;
+rule ifthenelse_split occ=0;
+rule andLeft occ=0;
+rule sub_zero_2 occ=0;
+rule ifthenelse_split occ=2;
 rule andLeft;
-rule sub_zero_2 occ: 0;
-rule add_zero_right occ: 0;
-rule add_zero_right occ: 0;
-rule add_zero_right occ: 0;
-rule add_zero_right occ: 0;
-rule add_zero_right occ: 0;
-rule add_zero_right occ: 0;
-rule ifthenelse_split occ: 0;
-rule ifthenelse_split occ: 0;
+rule sub_zero_2 occ=0;
+rule add_zero_right occ=0;
+rule add_zero_right occ=0;
+rule add_zero_right occ=0;
+rule add_zero_right occ=0;
+rule add_zero_right occ=0;
+rule add_zero_right occ=0;
+rule ifthenelse_split occ=0;
+rule ifthenelse_split occ=0;
 tryclose branch;
 tryclose branch;
-rule ifthenelse_split occ: 0;
+rule ifthenelse_split occ=0;
 tryclose branch;
-rule ifthenelse_split occ: 0;
+rule ifthenelse_split occ=0;
 rule seqNPermInjective;
-instantiate hide var: iv with: (iv_0);
-instantiate hide var: jv with: (f_y);
+instantiate hide var=iv with=(iv_0);
+instantiate hide var=jv with=(f_y);
 rule impLeft;
 tryclose branch;
 tryclose branch;
-rule ifthenelse_split occ: 0;
+rule ifthenelse_split occ=0;
 rule seqNPermInjective;
-instantiate hide var: iv with: (iv_0);
-instantiate hide var: jv with: (f_x);
+instantiate hide var=iv with=(iv_0);
+instantiate hide var=jv with=(f_x);
 rule impLeft;
 tryclose branch;
 tryclose branch;