Rewriter of old to new settings format.

key.core/src/main/antlr4/KeYLexer.g4

@@ -40,6 +40,10 @@ lexer grammar KeYLexer;
    }
 
     private Token tokenBackStorage = null;
+    private boolean proofIsEOF = true;
+    public void setProofIsEOF(boolean b) { proofIsEOF = b;}
+    public boolean isProofIsEOF() { return proofIsEOF;}
+
     @Override
     public void emit(Token token) {
        int MAX_K = 10;
@@ -51,7 +55,7 @@ lexer grammar KeYLexer;
                break;
            }
        }
-       if(token.getType() == PROOF) {
+       if(token.getType() == PROOF && isProofIsEOF()) {
           tokenBackStorage = super.emitEOF();
           //will later be overwritten the EOF token
        }

key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java

@@ -466,6 +466,10 @@ public ConfigurationWriter printIndent() {
         }
 
         public ConfigurationWriter printComment(String comment) {
+            if (comment == null || comment.isBlank()) {
+                return this;
+            }
+
             if (comment.contains("\n")) {
                 out.format("/* %s */\n", comment);
             } else {
@@ -509,7 +513,7 @@ public ConfigurationWriter printValue(Object value) {
         }
 
         private ConfigurationWriter printMap(Map<?, ?> value) {
-            out.format("{ ");
+            out.format("{");
             indent += 4;
             newline().printIndent();
             for (Iterator<? extends Map.Entry<?, ?>> iterator =
@@ -525,7 +529,7 @@ private ConfigurationWriter printMap(Map<?, ?> value) {
             }
             indent -= 4;
             newline().printIndent();
-            out.format(" }");
+            out.format("}");
             return this;
         }
 
@@ -536,7 +540,7 @@ private ConfigurationWriter print(String s) {
         }
 
         private ConfigurationWriter printSeq(Collection<?> value) {
-            out.format("[ ");
+            out.format("[");
             indent += 4;
             newline();
             printIndent();
@@ -555,7 +559,7 @@ private ConfigurationWriter printSeq(Collection<?> value) {
             }
             indent -= 4;
             newline().printIndent();
-            out.format(" ]");
+            out.format("]");
             return this;
         }
 

key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java

@@ -136,7 +136,7 @@ public Configuration getConfiguration() {
      * Used by saveSettings() and settingsToString()
      */
     public void settingsToStream(Writer out) {
-        getConfiguration().save(out, "Proof-Settings-Config-File");
+        getConfiguration().save(out, "");
     }
 
     /**

scripts/settings/RewriteSettings.java

@@ -0,0 +1,144 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
+
+import de.uka.ilkd.key.nparser.KeYLexer;
+import de.uka.ilkd.key.nparser.ParsingFacade;
+import de.uka.ilkd.key.settings.ProofSettings;
+import org.antlr.v4.runtime.CharStreams;
+import org.antlr.v4.runtime.Token;
+import org.antlr.v4.runtime.misc.ParseCancellationException;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import java.io.IOException;
+import java.nio.charset.Charset;
+import java.nio.file.Files;
+import java.nio.file.Path;
+import java.nio.file.Paths;
+import java.util.Collections;
+import java.util.Iterator;
+import java.util.zip.GZIPInputStream;
+import java.util.zip.GZIPOutputStream;
+
+/// This is a java program for rewriting the settings of KeY files from the old format to the new format.
+/// The old format was a string contain a properties file (`key=value`). The new format is JSON-like tree structure
+/// with the advantage of type safety and structureness.
+///
+/// ## How to run the program
+/// 1. Compile key to receive a fatjar
+/// ```sh
+/// key> gradle assemble
+///```
+///
+/// 2. Run this program using the shadow jar. Requires a rather new JDK/JRE:
+/// ```sh
+/// java -cp ../../key.ui/build/libs/key-2.12.4-dev-exe.jar RewriteSettings.java <files>
+///```
+/// (no compilation needed)
+///
+/// @author Alexander Weigl
+/// @version 1 (4/6/25)
+public class RewriteSettings {
+    private static final Logger LOGGER = LoggerFactory.getLogger(RewriteSettings.class);
+    private static boolean ERROR = false;
+    private static boolean ALWAYS_WRITE = false;
+
+    public static void main(String[] args) throws IOException {
+        if (args.length == 0) {
+            args = new String[]{
+                    "../../key.core/src/test/resources/testcase/parser/MultipleRecursion/MultipleRecursion[MultipleRecursion__a()]_JML_normal_behavior_operation_contract_0.proof"};
+        }
+
+        for (String arg : args) {
+            if ("-f".equals(arg)) {
+                ALWAYS_WRITE = true;
+            }
+
+            var path = Paths.get(arg);
+            var files = Files.isDirectory(
+                    path) ? Files.walk(path).filter(it -> Files.isRegularFile(it)
+                            && (it.getFileName().toString().endsWith(".key") ||
+                            it.getFileName().toString().endsWith(".proof")))
+                    .toList()
+                    : Collections.singletonList(path);
+            for (var file : files) {
+                rewrite(file);
+            }
+        }
+        System.exit(ERROR ? 1 : 0);
+    }
+
+    private static void rewrite(Path file) throws IOException {
+        boolean isGzip = file.getFileName().toString().endsWith(".gz");
+        LOGGER.info("Rewriting: {} (isGzip:{})", file.getFileName(), isGzip);
+        KeYLexer lex;
+        if (isGzip) {
+            var input = CharStreams.fromStream(new GZIPInputStream(Files.newInputStream(file)));
+            lex = ParsingFacade.createLexer(input);
+        } else {
+            lex = ParsingFacade.createLexer(file);
+        }
+        lex.setProofIsEOF(false);
+        var ctx = lex.getAllTokens();
+        var output = new StringBuilder();
+
+        boolean hit = false;
+        for (Iterator<? extends Token> iterator = ctx.iterator(); iterator.hasNext(); ) {
+            var token = iterator.next();
+            if (token.getType() == KeYLexer.KEYSETTINGS) {
+                output.append(token.getText());
+
+                while (iterator.hasNext() && token.getType() != KeYLexer.STRING_LITERAL) {
+                    token = iterator.next();
+                }
+
+                if (token.getType() != KeYLexer.STRING_LITERAL) {
+                    return;
+                }
+
+                hit = true;
+
+                final var text = token.getText();
+                var settings = new ProofSettings(ProofSettings.DEFAULT_SETTINGS);
+                settings.loadSettingsFromPropertyString(text.substring(1, text.length() - 1));
+                output.append(settings.settingsToString());
+
+                while (iterator.hasNext() && token.getType() != KeYLexer.RBRACE) {
+                    token = iterator.next();
+                }
+            } else {
+                output.append(token.getText());
+            }
+        }
+
+        if (!hit) {
+            LOGGER.warn("No settings in file {} found", file);
+            return;
+        }
+
+        boolean write = true;
+        try {
+            ParsingFacade.parseFile(CharStreams.fromString(output.toString()));
+        } catch (ParseCancellationException e) {
+            write = false;
+            LOGGER.error("Error parsing after rewrite file {}: {}", file, e.getMessage(), e);
+            System.err.println(output);
+        }
+
+        if (write || ALWAYS_WRITE) {
+
+            if (!isGzip) {
+                Files.writeString(file, output.toString());
+            } else {
+                try (var out = new GZIPOutputStream(Files.newOutputStream(file))) {
+                    out.write(output.toString().getBytes(Charset.defaultCharset()));
+                }
+            }
+            LOGGER.info("File translated, tested and written: {}", file);
+        } else {
+            ERROR = true;
+        }
+    }
+}
+