Pfeifer/proof mgmt includes fix

keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java

@@ -433,7 +433,18 @@ public static void ensureSourceLoaded(CheckerData data) throws ProofManagementEx
 
             Profile profile = AbstractProfile.getDefaultProfile();
 
-            SLEnvInput slenv = new SLEnvInput(src, cp, bcp, profile, null);
+            /*
+             * We need to respect included .key files from project.key (for dl_ escapes). The
+             * easiest way to do this is to add the top-level project.key as include and let
+             * SLEnvInput take care about the includes from there.
+             */
+            List<Path> includePaths = List.of();
+            Path projectFile = pbh.getTopLevelProjectFile();
+            if (projectFile != null) {
+                includePaths = List.of(projectFile);
+            }
+
+            SLEnvInput slenv = new SLEnvInput(src, cp, bcp, profile, includePaths);
             data.setSlenv(slenv);
             data.setSrcLoadingState(CheckerData.LoadingState.SUCCESS);
             data.print(LogLevel.DEBUG, "Java sources successfully loaded!");

keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/DirectoryProofBundleHandler.java

@@ -106,6 +106,15 @@ public Path getBootclasspath() throws IOException {
         return null;
     }
 
+    @Override
+    public Path getTopLevelProjectFile() {
+        Path projectFile = rootPath.resolve(Paths.get("project.key"));
+        if (Files.isRegularFile(projectFile)) {
+            return projectFile;
+        }
+        return null;
+    }
+
     @Override
     public PathNode getFileTree() throws IOException {
         PathNode root = new PathNode(null, rootPath);

keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ProofBundleHandler.java

@@ -117,6 +117,14 @@ public abstract class ProofBundleHandler implements Closeable {
      */
     public abstract Path getBootclasspath() throws IOException;
 
+    /**
+     * Returns the path to the top-level `project.key` file in the bundle, if existing, otherwise
+     * null.
+     *
+     * @return the path to the top-level project file or null
+     */
+    public abstract Path getTopLevelProjectFile();
+
     /**
      * Returns a tree of the complete file hierarchy inside the bundle.
      *

keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/io/ZipProofBundleHandler.java

@@ -111,6 +111,11 @@ public Path getBootclasspath() throws IOException {
         return dbh.getBootclasspath();
     }
 
+    @Override
+    public Path getTopLevelProjectFile() {
+        return dbh.getTopLevelProjectFile();
+    }
+
     @Override
     public PathNode getFileTree() throws IOException {
         // Path rootPath = fs.getPath("/");