compute a proper problem header including also the taclets

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java

@@ -378,9 +378,7 @@ public final String name() {
     /**
      * Creates declarations necessary to save/load proof in textual form (helper for createProof()).
      */
-    private void createProofHeader(
-            JavaModel model, Services services) {
-
+    private void createProofHeader(JavaModel model, Services services) {
         if (header != null) {
             return;
         }
@@ -418,8 +416,7 @@ protected Proof createProof(String proofName, JTerm poTerm, InitConfig proofConf
         if (proofConfig == null) {
             proofConfig = environmentConfig.deepCopy();
         }
-        final JavaModel javaModel = proofConfig.getServices().getJavaModel();
-        createProofHeader(javaModel, proofConfig.getServices());
+        header = proofConfig.getProblemHeader();
 
         final Proof proof = createProofObject(proofName, header, poTerm, proofConfig);
 

key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java

@@ -34,6 +34,7 @@
 import org.key_project.util.collection.ImmutableSet;
 
 import org.jspecify.annotations.NonNull;
+import org.jspecify.annotations.Nullable;
 
 /**
  * an instance of this class describes the initial configuration of the prover. This includes sorts,
@@ -79,10 +80,12 @@ public class InitConfig {
     /** the fileRepo which is responsible for consistency between source code and proof */
     private FileRepo fileRepo;
 
+    // weigl this field is never set
     private String originalKeYFileName;
 
     private ProofSettings settings;
 
+    private @Nullable String header;
 
 
     // -------------------------------------------------------------------------
@@ -437,6 +440,7 @@ public InitConfig copyWithServices(Services services) {
             (HashMap<Taclet, TacletBuilder<? extends Taclet>>) taclet2Builder.clone());
         ic.taclets = taclets;
         ic.originalKeYFileName = originalKeYFileName;
+        ic.header = header;
         ic.justifInfo = justifInfo.copy();
         ic.fileRepo = fileRepo; // TODO: copy instead? delete via dispose method?
         return ic;
@@ -466,4 +470,12 @@ public void activateChoice(Choice choice) {
                     .collect(ImmutableSet.collector())
                     .add(choice));
     }
+
+    public @Nullable String getProblemHeader() {
+        return header;
+    }
+
+    public void setHeader(@Nullable String header) {
+        this.header = header;
+    }
 }

key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java

@@ -254,6 +254,12 @@ private Profile readProfileFromFile() {
         }
     }
 
+
+    ///
+    public @Nullable String getProblemHeader() {
+        return getParseContext().getProblemHeader();
+    }
+
     /**
      * Returns the default {@link Profile} which was defined by a constructor.
      *

key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java

@@ -459,6 +459,11 @@ public InitConfig prepare(EnvInput envInput) throws ProofInputException {
             if (Debug.ENABLE_DEBUG) {
                 print(ic);
             }
+
+            if (envInput instanceof KeYUserProblemFile uf) {
+                ic.setHeader(uf.getProblemHeader());
+            }
+
             return ic;
         }
     }

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

@@ -21,6 +21,7 @@
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.init.IPersistablePO;
+import de.uka.ilkd.key.proof.init.KeYUserProblemFile;
 import de.uka.ilkd.key.proof.init.Profile;
 import de.uka.ilkd.key.proof.init.ProofOblInput;
 import de.uka.ilkd.key.proof.io.IProofFileParser.ProofElementID;
@@ -230,18 +231,26 @@ public void save(OutputStream out) throws IOException {
         }
     }
 
-    /**
-     * Searches in the header for absolute paths to Java files and tries to replace them by paths
-     * relative to the proof file to be saved.
-     *
-     * TODO weigl: if someone finds time, this function is a string manipulation mess.
-     * You should rather parse the header using the {@link de.uka.ilkd.key.nparser.ParsingFacade}
-     * and
-     * use the {@link de.uka.ilkd.key.nparser.builder.ProblemFinder} to extract the field.
-     *
-     * Better would be to get rid of the header, and using an AST.
-     */
-    private String makePathsRelative(String header) {
+    /// Searches in the header for absolute paths to Java files and tries to replace them by paths
+    /// relative to the proof file to be saved.
+    /// If the given `header` is null, an empty string is returned. This is the case for proofs,
+    /// that are non-KeY-file not crated by KeY-files.
+    ///
+    /// @param header a string created a proper KeY-file content.
+    ///
+    ///
+    /// TODO weigl: If someone finds time, this function is a string manipulation mess.
+    /// You should rather parse the header using the [de.uka.ilkd.key.nparser.ParsingFacade]
+    /// and use the [de.uka.ilkd.key.nparser.builder.ProblemFinder] to extract the field.
+    /// Better would be to get rid of the header, and using an AST.
+    ///
+    ///
+    /// @see KeYUserProblemFile#getProblemHeader()
+    /// @see de.uka.ilkd.key.proof.init.InitConfig#getProblemHeader()
+    private String makePathsRelative(@Nullable String header) {
+        if (header == null) {
+            return "";
+        }
         final String[] search =
             { "\\javaSource", "\\bootclasspath", "\\classpath", "\\include" };
         final String basePath;