try to fix the formatting

Author: wadoon

key.format/README.md

@@ -5,7 +5,7 @@ This module provide a pretty-printer / formatting utility for KeY files.
 Usage: 
 
 ```
-./gradlew :key.format:format
+./gradlew :key.format:formatKey
 ```
 
 which formats the rule base of KeY. 

key.format/build.gradle

@@ -29,4 +29,11 @@ tasks.register('formatKey', JavaExec) {
     workingDir(rootDir)
     classpath = sourceSets.main.runtimeClasspath
     args("format", "key.core/src/main/resources/de/uka/ilkd/key/proof/rules")
+}
+
+tasks.register('formatKeyCheck', JavaExec) {
+    mainClass = mainClassName
+    workingDir(rootDir)
+    classpath = sourceSets.main.runtimeClasspath
+    args("check", "key.core/src/main/resources/de/uka/ilkd/key/proof/rules")
 }

key.format/src/main/java/de/uka/ilkd/key/nparser/format/ExpressionVisitor.java

@@ -120,7 +120,9 @@ public Void visitTerminal(TerminalNode node) {
                 token == KeYLexer.AVOID ||
                 token == KeYLexer.EXISTS ||
                 token == KeYLexer.FORALL ||
-                token == KeYLexer.SEMI)) {
+                token == KeYLexer.SEMI)
+                || token==KeYLexer.IFEX
+                || token==KeYLexer.IDENT) {
             output.spaceBeforeNext();
         }
 

key.format/src/main/java/de/uka/ilkd/key/nparser/format/KeyFileFormatter.java

@@ -383,7 +383,7 @@ public Void visitTerminal(TerminalNode node) {
         if (token == KeYLexer.DOC_COMMENT) {
             processIndentationInMLComment(text, output);
         } else {
-            output.token(text);
+            output.token(node.getSymbol());
         }
 
         if (isLBrace) {
@@ -412,12 +412,9 @@ private static int countNLs(String text) {
      */
     public static String format(CharStream stream) {
         // weigl: Not necessary is handled within the lexer
-        // var in = CharStreams.fromString(text.replaceAll("\\r\\n?", "\n"));
+        //var in = CharStreams.fromString(text.replaceAll("\\r\\n?", "\n"));
 
         var lexer = ParsingFacade.createLexer(stream);
-        // weigl: Should not be necessary
-        // lexer.setTokenFactory(new CommonTokenFactory(true));
-
         CommonTokenStream tokens = new CommonTokenStream(lexer);
         tokens.fill();
 

key.format/src/main/java/de/uka/ilkd/key/nparser/format/KeyFormatFacade.java

@@ -11,10 +11,12 @@
 import java.io.IOException;
 import java.nio.file.Files;
 import java.nio.file.Path;
+import java.sql.SQLOutput;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.concurrent.Callable;
 
+import de.uka.ilkd.key.util.KeYConstants;
 import de.uka.ilkd.key.util.parsing.SyntaxErrorReporter;
 
 import org.antlr.v4.runtime.CharStreams;
@@ -51,7 +53,7 @@ public class KeyFormatFacade {
     public static boolean checkFile(Path file) throws IOException {
         var formatted = format(CharStreams.fromPath(file));
         var content = Files.readString(file);
-        return !content.equals(formatted);
+        return content.equals(formatted);
     }
 
 
@@ -97,10 +99,12 @@ private static class Format implements Callable<Integer> {
 
         @Override
         public Integer call() throws IOException {
+            System.out.println("Formatting ...");
             var files = expandPaths(paths);
 
             for (var file : files) {
                 try {
+                    System.out.printf("Formatting %s\n",file);
                     formatSingleFileTo(file);
                 } catch (SyntaxErrorReporter.ParserException e) {
                     LOGGER.error("{} | Parser error", file, e);
@@ -131,13 +135,19 @@ private static class Check implements Callable<Integer> {
 
         @Override
         public Integer call() throws IOException {
+            System.out.println("Checking ... ");
             var valid = true;
             var files = expandPaths(paths);
             for (Path file : files) {
                 try {
-                    if (checkFile(file)) {
-                        valid = false;
-                        LOGGER.warn("{} | File is not formatted properly", file);
+                    System.out.printf("Checking file %s", file);
+                    final var b = checkFile(file);
+                    valid &= b;
+                    if (b) {
+                        System.out.printf("  ... ok\n");
+                    } else {
+                        System.out.printf(" ... not ok\n");
+                        formatSingleFile(file, file.getParent().resolve(file.getFileName().toString() + ".formatted"));
                     }
                 } catch (SyntaxErrorReporter.ParserException e) {
                     LOGGER.error("{} | Syntax errors in file", file, e);
@@ -152,6 +162,7 @@ private static class Cmd {
     }
 
     public static void main(String[] args) {
+        System.out.println("KeY formatter. " + KeYConstants.VERSION);
         int exitCode = new CommandLine(new Cmd())
                 .addSubcommand(new Format())
                 .addSubcommand(new Check())

key.format/src/main/java/de/uka/ilkd/key/nparser/format/Output.java

@@ -3,9 +3,12 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.nparser.format;
 
+import de.uka.ilkd.key.nparser.KeYLexer;
+import org.antlr.v4.runtime.Token;
+
 /**
  * Output class for managing formatted output with indentation.
- *
+ * <p>
  * This class provides methods to manage and format output with proper
  * indentation and spacing. It supports adding tokens, characters, and
  * handling new lines and indentation levels.
@@ -63,26 +66,29 @@ public void noSpaceBeforeNext() {
         this.spaceBeforeNextToken = false;
     }
 
-    /**
-     * Add a token to the output. Respects whitespace before token.
-     *
-     * @param value a string value
-     */
-    public void token(String value) {
+
+    public void token(Token value) {
         checkBeforeToken();
-        output.append(value);
+        if (lastTokenId == KeYLexer.IDENT && value.getType() == KeYLexer.IDENT) {
+            spaceBeforeNext();
+        }
+        output.append(value.getText());
+        lastTokenId = value.getType();
     }
 
     /**
-     * Add a character to the output. Respects whitespace before token.
+     * Add a token to the output. Respects whitespace before token.
      *
-     * @param value a char value
+     * @param text a string value
      */
-    public void token(char value) {
+    public void token(String text) {
         checkBeforeToken();
-        output.append(value);
+        output.append(text);
+        lastTokenId = 0;
     }
 
+    private int lastTokenId;
+
     /**
      * Increases the indentation level.
      */