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

@@ -20,7 +20,7 @@
 ///
 /// 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;
 /// }
 /// ```
@@ -49,13 +49,19 @@ public ScriptCommandAst(String commandName, Map<String, Object> namedArgs,
         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)
@@ -64,7 +70,7 @@ public String asCommandLine() {
                         : ";");
     }
 
-    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;