Undo in InteractiveMode

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/ProofScriptDebugger.java

@@ -52,6 +52,7 @@ public class ProofScriptDebugger extends Application {
                     getClass().getResource("debugger-ui.css").toExternalForm(),
                     DockNode.class.getResource("default.css").toExternalForm()
             );
+            System.out.println(getClass().getResource("debugger-ui.css").toExternalForm());
 
             primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION);
             primaryStage.setScene(scene);

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

@@ -132,6 +132,9 @@ public class DebuggerMain implements Initializable {
     @FXML
     private ToggleButton btnInteractiveMode;
 
+    @FXML
+    private Button interactive_undo;
+
     private JavaArea javaArea = new JavaArea();
 
     private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
@@ -861,6 +864,22 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+    public void undo(ActionEvent actionEvent) {
+        LOGGER.debug("DebuggerMain.undo");
+        interactiveModeController.undo(actionEvent);
+
+
+
+        /*
+        try {
+            model.getDebuggerFramework().execute(new UndoCommand<>());
+        } catch (DebuggerException e) {
+            Utils.showExceptionDialog("", "", "", e);
+            LOGGER.error(e);
+        }
+        */
+    }
+
     public void stopDebugMode(ActionEvent actionEvent) {
         scriptController.getDebugPositionHighlighter().remove();
         Button stop = (Button) actionEvent.getSource();
@@ -884,10 +903,15 @@ public class DebuggerMain implements Initializable {
     @FXML
     public void interactiveMode(ActionEvent actionEvent) {
         if (btnInteractiveMode.isSelected()) {
+            assert model.getDebuggerFramework() != null;
+            interactiveModeController.setDebuggerFramework(model.getDebuggerFramework());
             interactiveModeController.setActivated(true);
             interactiveModeController.start(getFacade().getProof(), getInspectionViewsController().getActiveInspectionViewTab().getModel());
+
+            interactive_undo.setDisable(false);
         } else {
             interactiveModeController.stop();
+            interactive_undo.setDisable(true);
         }
     }
 

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/InteractiveModeController.java

@@ -17,6 +17,8 @@ import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
+import edu.kit.iti.formal.psdbg.interpreter.dbg.DebuggerFramework;
+import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
 import edu.kit.iti.formal.psdbg.interpreter.exceptions.ScriptCommandNotApplicableException;
 import edu.kit.iti.formal.psdbg.parser.PrettyPrinter;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
@@ -30,7 +32,10 @@ import lombok.val;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.key_project.util.collection.ImmutableList;
+import recoder.util.Debug;
 
+import java.awt.event.ActionEvent;
+import java.util.ArrayList;
 import java.util.HashMap;
 import java.util.List;
 import java.util.Map;
@@ -52,16 +57,71 @@ public class InteractiveModeController {
 
     private InspectionModel model;
 
+    private DebuggerFramework<KeyData> debuggerFramework;
+    private PTreeNode<KeyData> nodeAtInteractionStart;
+
+    //needed for Undo-Operation
+    private ArrayList<CallStatement> savepointsstatement;
+    private ArrayList<Node> savepointslist;
+
+    private Proof currentProof;
 
     public void start(Proof currentProof, InspectionModel model) {
         Events.register(this);
         cases.clear();
+        this.currentProof = currentProof;
         currentProof.getSubtreeGoals(currentProof.root()).forEach(goal -> {
             cases.put(goal.node(), new Statements());
         });
         this.scriptArea = scriptController.newScript();
         this.model = model;
 
+        savepointslist = new ArrayList<>();
+        savepointsstatement = new ArrayList<>();
+        nodeAtInteractionStart = debuggerFramework.getStatePointer();
+
+    }
+
+
+    /**
+     * Undo the application of the last rule
+     */
+    public void undo(javafx.event.ActionEvent actionEvent) {
+        if(savepointslist.isEmpty()) {
+            Debug.log("Kein vorheriger Zustand."); //TODO: events fire
+            return;
+        }
+
+        val pruneNode = savepointslist.get(savepointslist.size()-1);
+        savepointslist.remove(pruneNode);
+        ImmutableList<Goal> goalsbeforePrune = currentProof.getSubtreeGoals(pruneNode);
+
+        currentProof.pruneProof(pruneNode);
+        ImmutableList<Goal> goalsafterPrune = currentProof.getSubtreeGoals(pruneNode);
+
+        ObservableList<GoalNode<KeyData>> goals = model.getGoals();
+        List<GoalNode<KeyData>> prunedChildren = goals.stream()
+                .filter(keyDataGoalNode -> goalsbeforePrune.contains(keyDataGoalNode.getData().getGoal()))
+                .collect(Collectors.toList());
+
+        KeyData kd = prunedChildren.get(0).getData();
+        goals.removeAll(prunedChildren);
+        GoalNode<KeyData> lastGoalNode = null;
+        for (Goal newGoalNode : goalsafterPrune) {
+            KeyData kdn = new KeyData(kd, newGoalNode.node());
+            goals.add(
+                    lastGoalNode = new GoalNode<>(prunedChildren.get(0).getParent().getParent(), kdn, kdn.getNode().isClosed()));
+        }
+
+        model.setSelectedGoalNodeToShow(lastGoalNode );
+
+        //TODO: undo: map.foreach(k,v) -> v.remove().last
+        val pruneStatement = savepointsstatement.get(savepointsstatement.size()-1);
+        cases.forEach((k,v) -> v.remove(pruneStatement));
+
+        String c = getCasesAsString();
+        scriptArea.setText("" +
+                "//Preview \n" + c);
     }
 
     public void stop() {
@@ -129,6 +189,9 @@ public class InteractiveModeController {
     }
 
     private void applyRule(CallStatement call, Goal g) {
+        savepointslist.add(g.node());
+        savepointsstatement.add(call);
+
         ObservableList<GoalNode<KeyData>> goals = model.getGoals();
         GoalNode<KeyData> expandedNode;
         List<GoalNode<KeyData>> collect = goals.stream().filter(keyDataGoalNode -> keyDataGoalNode.getData().getGoal().equals(g)).collect(Collectors.toList());
@@ -172,6 +235,8 @@ public class InteractiveModeController {
 
     }
 
+
+
     public boolean isActivated() {
         return activated.get();
     }
@@ -183,4 +248,4 @@ public class InteractiveModeController {
     public BooleanProperty activatedProperty() {
         return activated;
     }
-}
+}
\ No newline at end of file

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml

@@ -286,6 +286,16 @@
                             </tooltip>
                         </ToggleButton>
 
+                        <Button fx:id="interactive_undo" onAction="#undo" disable="true">
+                            <graphic>
+                                <MaterialDesignIconView glyphName="UNDO" size="24.0"/>
+                            </graphic>
+                            <tooltip>
+                                <Tooltip text="Undo"/>
+                            </tooltip>
+                        </Button>
+
+
                         <Pane HBox.hgrow="ALWAYS"/>
                         <Label text="Windows:"/>
                         <ToggleButton fx:id="togBtnCodeDock" onAction="#showCodeDock">