repair branch after rewriting

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/control/KeYEnvironment.java

@@ -24,6 +24,7 @@
 import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
+import de.uka.ilkd.key.rule.Rule;
 import de.uka.ilkd.key.speclang.Contract;
 import de.uka.ilkd.key.util.KeYTypeUtil;
 

key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java

@@ -16,10 +16,7 @@
 import de.uka.ilkd.key.proof.mgt.RuleJustification;
 import de.uka.ilkd.key.proof.proofevent.NodeChangeJournal;
 import de.uka.ilkd.key.proof.proofevent.RuleAppInfo;
-import de.uka.ilkd.key.rule.AbstractExternalSolverRuleApp;
-import de.uka.ilkd.key.rule.IBuiltInRuleApp;
-import de.uka.ilkd.key.rule.NoPosTacletApp;
-import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.rule.*;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.rule.merge.MergeRule;
 import de.uka.ilkd.key.strategy.QueueRuleApplicationManager;

key.ui/src/main/java/de/uka/ilkd/key/core/Main.java

@@ -464,25 +464,27 @@ private AbstractMediatorUserInterfaceControl createUserInterface(List<Path> file
     }
 
     public static void ensureExamplesAvailable() {
-        File examplesDir = getExamplesDir() == null ? ExampleChooser.lookForExamples()
-                : new File(getExamplesDir());
-        if (!examplesDir.exists()) {
+        Path examplesDir =
+            getExamplesDir() == null ? ExampleChooser.lookForExamples() : getExamplesDir();
+        if (!Files.exists(examplesDir)) {
             examplesDir = setupExamples();
         }
-        setExamplesDir(examplesDir.getAbsolutePath());
+        if (examplesDir == null) {
+            setExamplesDir(examplesDir.toAbsolutePath());
+        }
     }
 
-    private static File setupExamples() {
+    private static @Nullable Path setupExamples() {
         try {
             URL examplesURL = Main.class.getResource("/examples.zip");
             if (examplesURL == null) {
                 throw new IOException("Missing examples.zip in resources");
             }
 
-            File tempDir = createTempDirectory();
+            Path tempDir = Files.createTempDirectory("key-examples");
 
             if (tempDir != null) {
-                IOUtil.extractZip(examplesURL.openStream(), tempDir.toPath());
+                IOUtil.extractZip(examplesURL.openStream(), tempDir);
             }
             return tempDir;
         } catch (IOException e) {
@@ -555,9 +557,9 @@ private void preProcessInput()
         }
     }
 
-    private static String EXAMPLE_DIR = null;
+    private static Path EXAMPLE_DIR = null;
 
-    public static @Nullable String getExamplesDir() {
+    public static @Nullable Path getExamplesDir() {
         return EXAMPLE_DIR;
     }
 
@@ -568,7 +570,7 @@ private void preProcessInput()
      *
      * @param newExamplesDir The new examples directory to use.
      */
-    public static void setExamplesDir(String newExamplesDir) {
+    public static void setExamplesDir(Path newExamplesDir) {
         EXAMPLE_DIR = newExamplesDir;
     }
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java

@@ -4,7 +4,7 @@
 package de.uka.ilkd.key.gui.actions;
 
 import java.awt.event.ActionEvent;
-import java.io.File;
+import java.nio.file.Path;
 
 import de.uka.ilkd.key.core.Main;
 import de.uka.ilkd.key.gui.ExampleChooser;
@@ -30,10 +30,10 @@ public OpenExampleAction(MainWindow mainWindow) {
     }
 
     public void actionPerformed(ActionEvent e) {
-        File file = ExampleChooser.showInstance(Main.getExamplesDir());
+        Path file = ExampleChooser.showInstance(Main.getExamplesDir());
         if (file != null) {
-            KeYFileChooser.getFileChooser("Select file to load").setSelectedFile(file);
-            mainWindow.loadProblem(file.toPath());
+            KeYFileChooser.getFileChooser("Select file to load").setSelectedFile(file.toFile());
+            mainWindow.loadProblem(file);
         }
     }
 }

key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java

@@ -100,7 +100,7 @@ public RunAllProofsAction(MainWindow mainWindow) {
         super(mainWindow);
 
         Main.ensureExamplesAvailable();
-        exampleDir = Paths.get(Main.getExamplesDir());
+        exampleDir = Main.getExamplesDir();
 
         try {
             files = loadFiles();

keyext.api.doc/src/main/java/PyGen.java

@@ -32,12 +32,8 @@
  * @author Alexander Weigl
  * @version 1 (14.10.23)
  */
-@NullMarked
-@CommandLine.Command(name = "gendoc",
-    mixinStandardHelpOptions = true,
-    version = "gendoc 1.0",
-    description = "Generates the documentation for key.api")
-public class ExtractMetaData implements Callable<Integer> {
+
+public class ExtractMetaData implements Runnable {
     private final List<Metamodel.Endpoint> endpoints = new LinkedList<>();
     private final Map<Class<?>, Metamodel.Type> types = new HashMap<>();
     private final Map<String, HelpText> segDocumentation = new TreeMap<>();
@@ -48,18 +44,7 @@ public ExtractMetaData() {
     }
 
     @Override
-    public Integer call() throws IOException {
-        if (source != null) {
-            ParserConfiguration config = new ParserConfiguration();
-            config.setLanguageLevel(ParserConfiguration.LanguageLevel.JAVA_21);
-            config.setAttributeComments(true);
-            config.setLexicalPreservationEnabled(false);
-            config.setStoreTokens(false);
-            config.setIgnoreAnnotationsWhenAttributingComments(true);
-            config.setDoNotAssignCommentsPrecedingEmptyLines(true);
-            sourceRoot = new SourceRoot(source, config);
-        }
-
+    public void run() {
         for (Method method : KeyApi.class.getMethods()) {
             addServerEndpoint(method);
         }
@@ -284,7 +269,7 @@ private static HelpText printFieldDocumentation(FieldJavadoc javadoc) {
 
     private void addClientEndpoint(Method method) {
         var jsonSegment = method.getDeclaringClass().getAnnotation(JsonSegment.class);
-        var segment = jsonSegment.value();
+        var segment = jsonSegment == null ? "" : jsonSegment.value();
 
         var req = method.getAnnotation(JsonRequest.class);
         var resp = method.getAnnotation(JsonNotification.class);
@@ -429,4 +414,8 @@ else if (type == CompletableFuture.class) {
 
         return null;
     }
+
+    public Metamodel.KeyApi getApi() {
+        return keyApi;
+    }
 }

keyext.api.doc/src/main/java/org/key_project/key/api/doc/ExtractMetaData.java

@@ -1,12 +1,7 @@
 /* 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 */
-package org.key_project.key.api.doc;/*
-                                     * 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
-                                     */
+package org.key_project.key.api.doc;
 
 import java.util.List;
 import java.util.Map;
@@ -15,10 +10,11 @@
 import org.jspecify.annotations.Nullable;
 import org.keyproject.key.api.data.DataExamples;
 
-/**
- * @author Alexander Weigl
- * @version 1 (29.10.23)
- */
+/// Metamodel of the API. This class contains classes which represents the functionality and
+/// interfaces of the API.
+///
+/// @author Alexander Weigl
+/// @version 1 (29.10.23)
 @NullMarked
 public class Metamodel {
 
@@ -51,9 +47,10 @@ public sealed interface Endpoint {
         HelpText documentation();
 
         default String kind() {
-            return getClass().getSimpleName();
+            return getClass().getName();
         }
 
+        /// a list of its arguments
         List<Argument> args();
 
         ///
@@ -76,6 +73,10 @@ default boolean isAsync() {
         }
     }
 
+    /// A [Argument] of an endpoint
+    ///
+    /// @param name the argument name
+    /// @param type the argument type
     public record Argument(String name, String type) {
     }
 
@@ -115,10 +116,8 @@ public record Field(String name, /* Type */ String type, @Nullable HelpText docu
         }
     }
 
-    public sealed
-
-
-    interface Type {
+    /// A data type
+    public sealed interface Type {
         default String kind() {
             return getClass().getName();
         }
@@ -127,8 +126,10 @@ default String kind() {
         @Nullable
         HelpText documentation();
 
+        /// name of the data type
         String name();
 
+        ///
         String identifier();
     }