From 638e108adf86b66bd7a05e9ed24307ef25f9eead Mon Sep 17 00:00:00 2001 From: Richard Bubel Date: Fri, 27 Oct 2023 11:32:00 +0200 Subject: [PATCH] Feature: If possible save the last selected node in the proof, to reselect it upon loading (issue #3297). --- .../AbstractSymbolicExecutionTestCase.java | 2 +- .../java/de/uka/ilkd/key/proof/Proof.java | 4 +- .../key/proof/io/AbstractProblemLoader.java | 16 +++--- .../de/uka/ilkd/key/proof/io/AutoSaver.java | 2 +- .../uka/ilkd/key/proof/io/GZipProofSaver.java | 7 ++- .../ilkd/key/proof/io/IProofFileParser.java | 2 +- ...termediatePresentationProofFileParser.java | 25 +++++++++ .../proof/io/IntermediateProofReplayer.java | 52 +++++++++---------- .../key/proof/io/OutputStreamProofSaver.java | 32 ++++++++---- .../ilkd/key/proof/io/ProofBundleSaver.java | 6 ++- .../de/uka/ilkd/key/proof/io/ProofSaver.java | 22 ++++---- .../io/intermediate/AppNodeIntermediate.java | 23 ++++++++ .../ilkd/key/proof/io/TestZipProofSaving.java | 2 +- .../io/consistency/TestProofBundleIO.java | 2 +- .../key/smt/newsmt2/ProveSMTLemmasTest.java | 2 +- .../key/gui/WindowUserInterfaceControl.java | 14 +++-- .../ilkd/key/gui/actions/QuickSaveAction.java | 6 ++- .../ilkd/key/gui/actions/SaveFileAction.java | 4 +- .../key/gui/actions/SendFeedbackAction.java | 3 +- .../key/gui/actions/ShowProofStatistics.java | 3 +- .../gui/lemmatagenerator/LemmataHandler.java | 2 +- .../ilkd/key/gui/prooftree/ProofTreeView.java | 17 +++++- .../AbstractMediatorUserInterfaceControl.java | 2 +- .../proofmanagement/check/KeYFacade.java | 10 ++-- 24 files changed, 176 insertions(+), 84 deletions(-) diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java index 95c6da8fe33..d887e1d13a8 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java @@ -1678,7 +1678,7 @@ protected void assertSaveAndReload(File baseDir, String javaPathInBaseDir, KeYEnvironment reloadedEnv = null; SymbolicExecutionTreeBuilder reloadedBuilder = null; try { - ProofSaver saver = new ProofSaver(env.getProof(), tempFile.getAbsolutePath(), + ProofSaver saver = new ProofSaver(env.getProof(), null, tempFile.getAbsolutePath(), KeYConstants.INTERNAL_VERSION); assertNull(saver.save()); // Load proof from saved *.proof file diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java index 6b97d88d82d..b223dee0696 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java @@ -1344,7 +1344,7 @@ public void setProofFile(File proofFile) { } public void saveToFile(File file) throws IOException { - ProofSaver saver = new ProofSaver(this, file); + ProofSaver saver = new ProofSaver(this, null, file); saver.save(); } @@ -1356,7 +1356,7 @@ public void saveToFile(File file) throws IOException { * @throws IOException on any I/O error */ public void saveProofObligationToFile(File file) throws IOException { - ProofSaver saver = new ProofSaver(this, file, false); + ProofSaver saver = new ProofSaver(this, null, file, false); saver.save(); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index ae83793a678..cd7398ca2f1 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -740,15 +740,17 @@ private ReplayResult replayProof(Proof proof) { replayResult = replayer.replay(problemInitializer.getListener(), problemInitializer.getProgMon()); - lastTouchedNode = replayResult.getLastSelectedGoal() != null - ? replayResult.getLastSelectedGoal().node() - : proof.root(); + lastTouchedNode = + replayResult.savedSelectedNode() != null ? replayResult.savedSelectedNode() + : replayResult.lastSelectedGoal() != null + ? replayResult.lastSelectedGoal().node() + : proof.root(); } catch (Exception e) { if (parserResult == null || parserResult.errors() == null || parserResult.errors().isEmpty() || replayer == null - || replayResult == null || replayResult.getErrors() == null - || replayResult.getErrors().isEmpty()) { + || replayResult == null || replayResult.errors() == null + || replayResult.errors().isEmpty()) { // this exception was something unexpected errors.add(e); } @@ -758,10 +760,10 @@ private ReplayResult replayProof(Proof proof) { errors.addAll(parserResult.errors()); } status += (status.isEmpty() ? "Proof replayed successfully." : "\n\n") - + (replayResult != null ? replayResult.getStatus() + + (replayResult != null ? replayResult.status() : "Error while loading proof."); if (replayResult != null) { - errors.addAll(replayResult.getErrors()); + errors.addAll(replayResult.errors()); } StrategyProperties newProps = diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java index 8d7ce122077..f87329128dd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java @@ -147,7 +147,7 @@ private void save(final String filename, final Proof proof) { // there may be concurrent changes to the proof... whatever final Runnable r = () -> { try { - new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION).save(); + new ProofSaver(proof, null, filename, KeYConstants.INTERNAL_VERSION).save(); LOGGER.info("File saved: {}", filename); } catch (Exception e) { LOGGER.error("Autosaving file {} failed.", filename, e); diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java index 6747ec7e9a6..7cc1f49e7c6 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipProofSaver.java @@ -8,6 +8,7 @@ import java.io.IOException; import java.util.zip.GZIPOutputStream; +import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; /** @@ -22,11 +23,13 @@ public class GZipProofSaver extends ProofSaver { * Instantiates a new proof saver. * * @param proof the non-null proof to save + * @param selectedNode the Node selected at time of saving or null if no + * information available * @param fileName the name of the file to write to * @param internalVersion the internal version */ - public GZipProofSaver(Proof proof, String fileName, String internalVersion) { - super(proof, fileName, internalVersion); + public GZipProofSaver(Proof proof, Node selectedNode, String fileName, String internalVersion) { + super(proof, selectedNode, fileName, internalVersion); } /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java index aa958b4efe6..b42c1e1e11f 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IProofFileParser.java @@ -34,7 +34,7 @@ enum ProofElementID { USER_INTERACTION("userinteraction"), PROOF_SCRIPT("proofscript"), NEW_NAMES("newnames"), AUTOMODE_TIME("autoModeTime"), KeY_LOG("keyLog"), KeY_USER("keyUser"), KeY_VERSION("keyVersion"), KeY_SETTINGS("keySettings"), OPEN_GOAL("opengoal"), - NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality"); + NOTES("notes"), SOLVERTYPE("solverType"), MODALITY("modality"), SELECTED_NODE("selected"); private final String rawName; diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java index 4e5b2ad248c..844f2f1d06a 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java @@ -74,6 +74,7 @@ public class IntermediatePresentationProofFileParser implements IProofFileParser private BranchNodeIntermediate root = null; // the "dummy ID" branch private NodeIntermediate currNode; private final LinkedList errors = new LinkedList<>(); + private boolean parsingOpenGoal = false; /** * @param proof Proof object for storing meta information about the parsed proof. @@ -220,6 +221,9 @@ public void beginExpr(ProofElementID eid, String str) { } } case SOLVERTYPE -> ((BuiltinRuleInformation) ruleInfo).solver = str; + case OPEN_GOAL -> { + parsingOpenGoal = true; + } default -> { } } @@ -235,6 +239,24 @@ public void endExpr(ProofElementID eid, int lineNr) { ((AppNodeIntermediate) currNode).setInteractiveRuleApplication(true); } } + case SELECTED_NODE -> { + int openGoalChildSelected = -1; + if (parsingOpenGoal) { + if (currNode instanceof BranchNodeIntermediate branchNode) { + if (!stack.isEmpty()) { + if (stack.peek() instanceof AppNodeIntermediate parentAppNode) { + openGoalChildSelected = parentAppNode.getChildren().size() - 1; + parentAppNode.setSelectedNode(true, openGoalChildSelected); + } + } + } else { + openGoalChildSelected = 0; + } + } + if (currNode != null && currNode instanceof AppNodeIntermediate appNode) { + appNode.setSelectedNode(true, openGoalChildSelected); + } + } case PROOF_SCRIPT -> { if (currNode != null) { ((AppNodeIntermediate) currNode).setScriptRuleApplication(true); @@ -254,6 +276,9 @@ public void endExpr(ProofElementID eid, int lineNr) { builtinInfo.builtinIfInsts.append(new Pair<>( builtinInfo.currIfInstFormula, builtinInfo.currIfInstPosInTerm)); } + case OPEN_GOAL -> { + parsingOpenGoal = false; + } default -> { } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java index fc3895e7b0c..6c1b78bb184 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java @@ -116,12 +116,15 @@ public class IntermediateProofReplayer { /** The current open goal */ private Goal currGoal = null; + /** the node selected at time of saving, or null if information is not available */ + private Node savedSelectedNode = null; + /** * Constructs a new {@link IntermediateProofReplayer}. * - * @param loader The problem loader, for reporting errors. - * @param proof The proof object into which to load the replayed proof. - * @param parserResult the result of the proof file parser to be replayed + * @param loader the problem loader, for reporting errors. + * @param proof the proof object into which to load the replayed proof. + * @param parserResult the result of the intermediate parser to be replayed */ public IntermediateProofReplayer(AbstractProblemLoader loader, Proof proof, IntermediatePresentationProofFileParser.Result parserResult) { @@ -223,6 +226,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener, proof.getServices().getNameRecorder() .setProposals(currInterm.getIntermediateRuleApp().getNewNames()); + if (currInterm.getIntermediateRuleApp() instanceof TacletAppIntermediate) { TacletAppIntermediate appInterm = (TacletAppIntermediate) currInterm.getIntermediateRuleApp(); @@ -358,6 +362,21 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener, } } } + // set information if this node was the last selected node at the time of saving + // the + // proof + if (currInterm.getSelectedNode()) { + // check whether the node itself was selected or a child that is an open + // goal + int openChildSelected = currInterm.getOpenChildSelected(); + if (openChildSelected < 0 + || openChildSelected >= currNode.childrenCount()) { + savedSelectedNode = currNode; + } else { + savedSelectedNode = currNode.child(openChildSelected); + } + } + } } catch (Throwable throwable) { // Default exception catcher -- proof should not stop loading @@ -374,7 +393,7 @@ public Result replay(ProblemInitializer.ProblemInitializerListener listener, progressMonitor.setProgress(max); } LOGGER.debug("Proof replay took " + PerfScope.formatTime(System.nanoTime() - time)); - return new Result(status, errors, currGoal); + return new Result(status, errors, currGoal, savedSelectedNode); } /** @@ -1057,27 +1076,6 @@ static class SkipSMTRuleException extends Exception { * * @author Dominic Scheurer */ - public static class Result { - private final String status; - private final List errors; - private Goal lastSelectedGoal = null; - - public Result(String status, List errors, Goal lastSelectedGoal) { - this.status = status; - this.errors = errors; - this.lastSelectedGoal = lastSelectedGoal; - } - - public String getStatus() { - return status; - } - - public List getErrors() { - return errors; - } - - public Goal getLastSelectedGoal() { - return lastSelectedGoal; - } - } + public record Result(String status, List errors, Goal lastSelectedGoal, + Node savedSelectedNode) {} } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java index 536cfb5ec79..9504a056432 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java @@ -74,6 +74,10 @@ public class OutputStreamProofSaver { */ protected final boolean saveProofSteps; + /** + * The currently selected node if available, otherwise null + */ + protected final Node selectedNode; /** * Extracts java source directory from {@link Proof#header()}, if it exists. @@ -95,27 +99,28 @@ public static File getJavaSourceLocation(Proof proof) { return null; } - public OutputStreamProofSaver(Proof proof) { - this(proof, KeYConstants.INTERNAL_VERSION); + public OutputStreamProofSaver(Proof proof, Node selectedNode) { + this(proof, selectedNode, KeYConstants.INTERNAL_VERSION); } - public OutputStreamProofSaver(Proof proof, String internalVersion) { - this.proof = proof; - this.internalVersion = internalVersion; - this.saveProofSteps = true; + public OutputStreamProofSaver(Proof proof, Node selectedNode, String internalVersion) { + this(proof, selectedNode, internalVersion, true); } /** * Create a new OutputStreamProofSaver. * * @param proof the proof to save + * @param selectedNode the Node selected at time of saving or null if no information available * @param internalVersion currently running KeY version * @param saveProofSteps whether to save the performed proof steps */ - public OutputStreamProofSaver(Proof proof, String internalVersion, boolean saveProofSteps) { + public OutputStreamProofSaver(Proof proof, Node selectedNode, String internalVersion, + boolean saveProofSteps) { this.proof = proof; this.internalVersion = internalVersion; this.saveProofSteps = saveProofSteps; + this.selectedNode = selectedNode; } /** @@ -589,7 +594,11 @@ private void printSingleNode(Node node, String prefix, Appendable output) throws printer.printSequent(node.sequent()); output.append(escapeCharacters(printer.result().replace('\n', ' '))); - output.append("\")\n"); + output.append("\""); + if (node == selectedNode) { + output.append(" (" + ProofElementID.SELECTED_NODE.getRawName() + ")"); + } + output.append(")\n"); return; } @@ -653,10 +662,13 @@ private void collectProof(Node node, String prefix, Appendable output) throws IO */ private void userInteraction2Proof(Node node, Appendable output) throws IOException { if (node.getNodeInfo().getInteractiveRuleApplication()) { - output.append(" (userinteraction)"); + output.append(" (" + ProofElementID.USER_INTERACTION.getRawName() + ")"); + } + if (node == selectedNode) { + output.append(" (" + ProofElementID.SELECTED_NODE.getRawName() + ")"); } if (node.getNodeInfo().getScriptRuleApplication()) { - output.append(" (proofscript)"); + output.append(" (" + ProofElementID.PROOF_SCRIPT.getRawName() + ")"); } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java index 32e54ea77ba..db5b3dec3af 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java @@ -7,6 +7,7 @@ import java.io.IOException; import java.nio.file.Paths; +import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.consistency.AbstractFileRepo; import de.uka.ilkd.key.proof.io.consistency.FileRepo; @@ -30,10 +31,11 @@ public class ProofBundleSaver extends ProofSaver { * Creates a new ProofBundleSaver. * * @param proof the proof to save + * @param selectedNode the Node selected at time of saving or null if no information available * @param saveFile the target filename */ - public ProofBundleSaver(Proof proof, File saveFile) { - super(proof, saveFile); + public ProofBundleSaver(Proof proof, Node selectedNode, File saveFile) { + super(proof, selectedNode, saveFile); } @Override diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java index 8cfcae13817..ab9d9eebc91 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofSaver.java @@ -9,6 +9,7 @@ import java.util.LinkedList; import java.util.List; +import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.event.ProofSaverEvent; import de.uka.ilkd.key.proof.io.event.ProofSaverListener; @@ -37,16 +38,16 @@ public class ProofSaver extends OutputStreamProofSaver { */ private static final List listeners = new LinkedList<>(); - public ProofSaver(Proof proof, String fileName, String internalVersion) { - this(proof, new File(fileName), internalVersion); + public ProofSaver(Proof proof, Node selectedNdode, String fileName, String internalVersion) { + this(proof, selectedNdode, new File(fileName), internalVersion); } - public ProofSaver(Proof proof, File file) { - this(proof, file, KeYConstants.INTERNAL_VERSION); + public ProofSaver(Proof proof, Node selectedNode, File file) { + this(proof, selectedNode, file, KeYConstants.INTERNAL_VERSION); } - public ProofSaver(Proof proof, File file, String internalVersion) { - super(proof, internalVersion); + public ProofSaver(Proof proof, Node selectedNode, File file, String internalVersion) { + super(proof, selectedNode, internalVersion); this.file = file; } @@ -57,8 +58,8 @@ public ProofSaver(Proof proof, File file, String internalVersion) { * @param file file to save proof into * @param saveProofSteps whether to save proof steps (false -> only proof obligation) */ - public ProofSaver(Proof proof, File file, boolean saveProofSteps) { - this(proof, file, KeYConstants.INTERNAL_VERSION, saveProofSteps); + public ProofSaver(Proof proof, Node selectedNode, File file, boolean saveProofSteps) { + this(proof, selectedNode, file, KeYConstants.INTERNAL_VERSION, saveProofSteps); } /** @@ -69,8 +70,9 @@ public ProofSaver(Proof proof, File file, boolean saveProofSteps) { * @param internalVersion version of KeY to add to the proof log * @param saveProofSteps whether to save proof steps (false -> only proof obligation) */ - public ProofSaver(Proof proof, File file, String internalVersion, boolean saveProofSteps) { - super(proof, internalVersion, saveProofSteps); + public ProofSaver(Proof proof, Node selectedNode, File file, String internalVersion, + boolean saveProofSteps) { + super(proof, selectedNode, internalVersion, saveProofSteps); this.file = file; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/AppNodeIntermediate.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/AppNodeIntermediate.java index 63133b7f6f3..7c1506d95be 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/AppNodeIntermediate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/AppNodeIntermediate.java @@ -16,6 +16,9 @@ public class AppNodeIntermediate extends NodeIntermediate { private boolean scriptRuleApplication = false; /** user-provided notes for the node */ private String notes = null; + /** true if this node was the one selected at the time of saving the proof */ + private boolean selectedNode; + private int openGoalChildSelected = -1; public AppIntermediate getIntermediateRuleApp() { return ruleApp; @@ -41,6 +44,26 @@ public void setScriptRuleApplication(boolean scriptRuleApplication) { this.scriptRuleApplication = scriptRuleApplication; } + public void setSelectedNode(boolean selectedNode, int openGoalChildSelected) { + this.selectedNode = selectedNode; + this.openGoalChildSelected = openGoalChildSelected; + } + + public boolean getSelectedNode() { + return selectedNode; + } + + /** + * return the index of a selected child that is an open goal + * if the node itself is selected -1 is returned + * + * @return the index of an open child (if a goal was selected when saving), -1 if the node + * itself is selected + */ + public int getOpenChildSelected() { + return openGoalChildSelected; + } + public void setNotes(String notes) { this.notes = notes; } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/io/TestZipProofSaving.java b/key.core/src/test/java/de/uka/ilkd/key/proof/io/TestZipProofSaving.java index 57ad2025a7e..9a882060139 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/io/TestZipProofSaving.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/io/TestZipProofSaving.java @@ -37,7 +37,7 @@ private void proveAndSaveZip(Path file, Path fileTarget) KeYEnvironment env = KeYEnvironment.load(file.toFile()); env.getProofControl().startAndWaitForAutoMode(env.getLoadedProof()); GZipProofSaver proofSaver = - new GZipProofSaver(env.getLoadedProof(), fileTarget.toString(), "n/a"); + new GZipProofSaver(env.getLoadedProof(), null, fileTarget.toString(), "n/a"); proofSaver.save(); } diff --git a/key.core/src/test/java/de/uka/ilkd/key/proof/io/consistency/TestProofBundleIO.java b/key.core/src/test/java/de/uka/ilkd/key/proof/io/consistency/TestProofBundleIO.java index 1f05b1ae87f..0a494ab8a4c 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/proof/io/consistency/TestProofBundleIO.java +++ b/key.core/src/test/java/de/uka/ilkd/key/proof/io/consistency/TestProofBundleIO.java @@ -216,7 +216,7 @@ private Path testBundleGeneration(String dirName, long expectedSize) throws Exce // save (closed) proof as a bundle Path target = testDir.resolve(dirName).resolve("test.zproof"); - ProofBundleSaver saver = new ProofBundleSaver(proof, target.toFile()); + ProofBundleSaver saver = new ProofBundleSaver(proof, null, target.toFile()); saver.save(); // check if target file exists and has minimum size diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java index 4021eeebf0d..afab8708d0d 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java @@ -78,7 +78,7 @@ public void testSMTLemmaSoundness(String name, String lemmaString) throws Except env.getProofControl().startAndWaitForAutoMode(loadedProof); if (!loadedProof.closed()) { File saveFile = new File(file.getAbsoluteFile() + ".proof"); - ProofSaver saver = new ProofSaver(loadedProof, saveFile); + ProofSaver saver = new ProofSaver(loadedProof, null, saveFile); saver.save(); Assertions.fail("Proof does not close. See " + file + " and " + saveFile); } else { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index 88d8f7c46ba..6147d7854c5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -26,6 +26,7 @@ import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; @@ -387,7 +388,8 @@ public AbstractProblemLoader load(Profile profile, File file, List classPa * @param fileExtension the respective file extension * @return the saved proof as a file */ - public File saveProof(Proof proof, String fileExtension) { + + public File saveProof(Proof proof, Node selectedNode, String fileExtension) { final MainWindow mainWindow = MainWindow.getInstance(); final KeYFileChooser fc = KeYFileChooser.getFileChooser("Choose filename to save proof"); fc.setFileFilter(KeYFileChooser.DEFAULT_FILTER); @@ -400,9 +402,11 @@ public File saveProof(Proof proof, String fileExtension) { final String filename = file.getAbsolutePath(); ProofSaver saver; if (fc.useCompression()) { - saver = new GZipProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION); + saver = new GZipProofSaver(proof, selectedNode, filename, + KeYConstants.INTERNAL_VERSION); } else { - saver = new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION); + saver = + new ProofSaver(proof, selectedNode, filename, KeYConstants.INTERNAL_VERSION); } String errorMsg; try { @@ -438,7 +442,8 @@ public void saveProofBundle(Proof proof) { final int result = fileChooser.showSaveDialog(mainWindow, f.first, f.second); if (result == JFileChooser.APPROVE_OPTION) { final File file = fileChooser.getSelectedFile(); - final ProofSaver saver = new ProofBundleSaver(proof, file); + final ProofSaver saver = + new ProofBundleSaver(proof, getMediator().getSelectedNode(), file); final String errorMsg = saver.save(); if (errorMsg != null) { @@ -538,6 +543,7 @@ public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poCo if (poContainer != null && poContainer.getProofOblInput() instanceof KeYUserProblemFile) { ((KeYUserProblemFile) poContainer.getProofOblInput()).close(); } + getMediator().getSelectionModel().setSelectedNode(result.getNode()); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java index 597cda24603..d891b3cdd02 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/QuickSaveAction.java @@ -7,6 +7,7 @@ import java.io.File; import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.ProofSaver; import de.uka.ilkd.key.util.KeYConstants; @@ -53,8 +54,9 @@ public static void quickSave(MainWindow mainWindow) { if (mainWindow.getMediator().ensureProofLoaded()) { final String filename = QUICK_SAVE_PATH; final Proof proof = mainWindow.getMediator().getSelectedProof(); - - String status = new ProofSaver(proof, filename, KeYConstants.INTERNAL_VERSION).save(); + final Node selectedNode = mainWindow.getMediator().getSelectedNode(); + String status = + new ProofSaver(proof, selectedNode, filename, KeYConstants.INTERNAL_VERSION).save(); if (status == null) { // success case diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveFileAction.java index f82b0b33195..04a5ef18b13 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveFileAction.java @@ -7,6 +7,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; /** @@ -31,7 +32,8 @@ public void actionPerformed(ActionEvent e) { if (mainWindow.getMediator().ensureProofLoaded()) { // Try to save back to file where proof was initially loaded from final Proof selectedProof = mainWindow.getMediator().getSelectedProof(); - mainWindow.getUserInterface().saveProof(selectedProof, ".proof"); + final Node selectedNode = mainWindow.getMediator().getSelectedNode(); + mainWindow.getUserInterface().saveProof(selectedProof, selectedNode, ".proof"); } else { mainWindow.popupWarning("No proof.", "Oops..."); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java index 1d87d1712ac..3e9b226e3f5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java @@ -212,7 +212,8 @@ private static class OpenProofItem extends SendFeedbackFileItem { byte[] retrieveFileData() throws IOException { KeYMediator mediator = MainWindow.getInstance().getMediator(); Proof proof = mediator.getSelectedProof(); - OutputStreamProofSaver saver = new OutputStreamProofSaver(proof); + OutputStreamProofSaver saver = + new OutputStreamProofSaver(proof, mediator.getSelectedNode()); ByteArrayOutputStream stream = new ByteArrayOutputStream(); saver.save(stream); return stream.toByteArray(); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java index f7978a92249..a0abc701ec6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java @@ -304,7 +304,8 @@ private void init(MainWindow mainWindow, String stats) { JButton saveButton = new JButton("Save proof"); saveButton.addActionListener( - e -> mainWindow.getUserInterface().saveProof(proof, ".proof")); + e -> mainWindow.getUserInterface().saveProof(proof, + mainWindow.getMediator().getSelectedNode(), ".proof")); JButton saveBundleButton = new JButton("Save proof bundle"); saveBundleButton .addActionListener(e -> mainWindow.getUserInterface().saveProofBundle(proof)); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataHandler.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataHandler.java index 3b2f4191af6..4c4fd28f7a9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataHandler.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataHandler.java @@ -152,7 +152,7 @@ private void startProofs(ProofAggregate pa) { private void saveProof(Proof p) throws IOException { ProofSaver saver = - new ProofSaver(p, options.createProofPath(p), options.getInternalVersion()); + new ProofSaver(p, null, options.createProofPath(p), options.getInternalVersion()); saver.save(); } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index ffd63a07333..ec8767650e4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -518,8 +518,21 @@ private void setProof(Proof p) { delegateView.setSelectionPath(delegateModel.getSelection()); delegateView.scrollPathToVisible(delegateModel.getSelection()); } else { - // new proof, select initial node - delegateView.setSelectionRow(1); + Node selectedNode = mediator.getSelectedNode(); + if (selectedNode == null || selectedNode.proof() != p) { + // new proof, select initial node + delegateView.setSelectionRow(1); + } else { + final GUIAbstractTreeNode guiNodeForSelectedProofNode = + delegateModel.find(selectedNode); + if (guiNodeForSelectedProofNode != null) { + delegateView.setSelectionPath( + new TreePath(guiNodeForSelectedProofNode.getPath())); + } else { + // fail safe + delegateView.setSelectionRow(1); + } + } } // Restore previous scroll position. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java index 5b547b0ca16..066fdf3c0f6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java @@ -213,7 +213,7 @@ private void saveSideProof(Proof proof) { } final File toSave = new File(proofFolder, filename); final KeYResourceManager krm = KeYResourceManager.getManager(); - final ProofSaver ps = new ProofSaver(proof, toSave.getAbsolutePath(), krm.getSHA1()); + final ProofSaver ps = new ProofSaver(proof, null, toSave.getAbsolutePath(), krm.getSHA1()); final String errorMsg = ps.save(); if (errorMsg != null) { reportException(this, null, new IOException(errorMsg)); diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java index 6d445482155..b05934e8e93 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/check/KeYFacade.java @@ -381,14 +381,14 @@ private static ReplayResult replayProof(CheckerData.ProofEntry line, EnvInput en // pass false here to keep the intermediate tree (may be needed for later checkers)! replayResult = replayer.replay(null, null, false); - Goal lastGoal = replayResult.getLastSelectedGoal(); + Goal lastGoal = replayResult.lastSelectedGoal(); lastTouchedNode = lastGoal != null ? lastGoal.node() : proof.root(); } catch (Exception e) { if (parserResult == null || parserResult.errors() == null || parserResult.errors().isEmpty() || - replayer == null || replayResult == null || replayResult.getErrors() == null - || replayResult.getErrors().isEmpty()) { + replayer == null || replayResult == null || replayResult.errors() == null + || replayResult.errors().isEmpty()) { // this exception was something unexpected errors.add(e); } @@ -399,10 +399,10 @@ private static ReplayResult replayProof(CheckerData.ProofEntry line, EnvInput en errors.addAll(parserResult.errors()); } status += - (status.isEmpty() ? "" : "\n\n") + (replayResult != null ? replayResult.getStatus() + (status.isEmpty() ? "" : "\n\n") + (replayResult != null ? replayResult.status() : "Error while loading proof."); if (replayResult != null) { - errors.addAll(replayResult.getErrors()); + errors.addAll(replayResult.errors()); } // reset OSS