StepInto for Atomic Calls!

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/CommandHandler.java

@@ -28,7 +28,7 @@ public interface CommandHandler<T> {
                   VariableAssignment params);
 
     default boolean isAtomic() {
-        return false;
+        return true;
     }
 
     /**

rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/ProofScriptHandler.java

@@ -98,7 +98,7 @@ public class ProofScriptHandler implements CommandHandler {
 
     @Override
     public boolean isAtomic() {
-        return true;
+        return false;
     }
 
     public void addScripts(List<ProofScript> ast) {

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

@@ -6,6 +6,9 @@ import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.api.ProofApi;
+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.init.ProofInputException;
 import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.speclang.Contract;
@@ -40,6 +43,7 @@ import javafx.scene.web.WebEngine;
 import javafx.scene.web.WebView;
 import javafx.stage.FileChooser;
 import lombok.Getter;
+import lombok.RequiredArgsConstructor;
 import org.antlr.v4.runtime.RecognitionException;
 import org.apache.commons.io.FileUtils;
 import org.apache.logging.log4j.LogManager;
@@ -63,6 +67,7 @@ import java.util.Optional;
 import java.util.ResourceBundle;
 import java.util.Set;
 import java.util.concurrent.*;
+import java.util.stream.Collectors;
 
 /**
  * Controller for the Debugger MainWindow
@@ -787,6 +792,10 @@ public class DebuggerMain implements Initializable {
     public void stepInto(ActionEvent actionEvent) {
         LOGGER.debug("DebuggerMain.stepOver");
         try {
+            if (model.getDebuggerFramework().getStatePointer().isAtomic()) {
+                model.getDebuggerFramework().getStatePointerListener()
+                        .add(new StepIntoHandler(model.getStatePointer()));
+            }
             model.getDebuggerFramework().execute(new StepIntoCommand<>());
         } catch (DebuggerException e) {
             Utils.showExceptionDialog("", "", "", e);
@@ -794,6 +803,11 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+    private void handleStepInto(PTreeNode<KeyData> newState) {
+
+
+    }
+
     /**
      * Perform a step back
      *
@@ -931,6 +945,38 @@ public class DebuggerMain implements Initializable {
             return FACADE.getContractsForJavaFileTask(model.getJavaFile());
         }
     }
+
+    @RequiredArgsConstructor
+    private class StepIntoHandler implements java.util.function.Consumer<PTreeNode<KeyData>> {
+        private final PTreeNode<KeyData> original;
+
+        @Override
+        public void accept(PTreeNode<KeyData> keyDataPTreeNode) {
+            Platform.runLater(this::acceptUI);
+        }
+
+        public void acceptUI() {
+            model.getDebuggerFramework().getStatePointerListener().remove(this);
+            GoalNode<KeyData> beforeNode = original.getStateBeforeStmt().getSelectedGoalNode();
+            ProofTree ptree = new ProofTree();
+            Proof proof = beforeNode.getData().getProof();
+            Node pnode = beforeNode.getData().getNode();
+
+            ptree.setProof(proof);
+            ptree.setRoot(pnode);
+            ptree.setDeactivateRefresh(true);
+
+            Set<Node> sentinels = proof.getSubtreeGoals(pnode)
+                    .stream()
+                    .map(Goal::node)
+                    .collect(Collectors.toSet());
+            ptree.getSentinels().addAll(sentinels);
+            DockNode node = new DockNode(ptree, "Proof Tree for Step Into: " +
+                    original.getStatement().accept(new ShortCommandPrinter())
+            );
+            node.dock(dockStation, DockPos.CENTER, getActiveInspectorDock());
+        }
+    }
 //endregion
 }
 //deprecated

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

@@ -11,11 +11,9 @@ import de.uka.ilkd.key.proof.ProofTreeListener;
 import edu.kit.iti.formal.psdbg.LabelFactory;
 import edu.kit.iti.formal.psdbg.gui.controller.Events;
 import javafx.application.Platform;
-import javafx.beans.property.MapProperty;
-import javafx.beans.property.ObjectProperty;
-import javafx.beans.property.SimpleMapProperty;
-import javafx.beans.property.SimpleObjectProperty;
+import javafx.beans.property.*;
 import javafx.collections.FXCollections;
+import javafx.collections.ObservableSet;
 import javafx.fxml.FXML;
 import javafx.scene.control.*;
 import javafx.scene.control.cell.TextFieldTreeCell;
@@ -40,11 +38,21 @@ public class ProofTree extends BorderPane {
 
     private ObjectProperty<Node> root = new SimpleObjectProperty<>();
 
+    private SetProperty<Node> sentinels = new SimpleSetProperty<>(FXCollections.observableSet());
+
+
     private MapProperty colorOfNodes = new SimpleMapProperty<>(FXCollections.observableHashMap());
 
     @FXML
     private TreeView<TreeNode> treeProof;
 
+    private ContextMenu contextMenu;
+
+    @Getter @Setter
+    private Services services;// = DebuggerMain.FACADE.getService();
+
+    private BooleanProperty deactivateRefresh = new SimpleBooleanProperty();
+
     private ProofTreeListener proofTreeListener = new ProofTreeListener() {
         @Override
         public void proofExpanded(ProofTreeEvent proofTreeEvent) {
@@ -97,11 +105,6 @@ public class ProofTree extends BorderPane {
         }
     };
 
-    private ContextMenu contextMenu;
-
-    @Getter @Setter
-    private Services services;// = DebuggerMain.FACADE.getService();
-
     public ProofTree() {
         Utils.createWithFXML(this);
         treeProof.setCellFactory(this::cellFactory);
@@ -259,18 +262,26 @@ public class ProofTree extends BorderPane {
     }
 
     private void init() {
+        if (deactivateRefresh.get())
+            return;
+
         if (root.get() != null) {
             TreeItem<TreeNode> item = populate("Proof", root.get());
             treeProof.setRoot(item);
         }
+
         treeProof.refresh();
     }
 
     private TreeItem<TreeNode> populate(String label, Node n) {
-
         val treeNode = new TreeNode(label, n);
-
         TreeItem<TreeNode> ti = new TreeItem<>(treeNode);
+
+        // abort the traversing iff we have reached a sentinel!
+        if (sentinels.contains(n)) {
+            return ti;
+        }
+
         if (n.childrenCount() == 0) {
             ti.getChildren().add(new TreeItem<>(new TreeNode(
                     n.isClosed() ? "CLOSED GOAL" : "OPEN GOAL", null)));
@@ -386,6 +397,30 @@ public class ProofTree extends BorderPane {
         return proof;
     }
 
+    public ObservableSet<Node> getSentinels() {
+        return sentinels.get();
+    }
+
+    public void setSentinels(ObservableSet<Node> sentinels) {
+        this.sentinels.set(sentinels);
+    }
+
+    public SetProperty<Node> sentinelsProperty() {
+        return sentinels;
+    }
+
+    public boolean isDeactivateRefresh() {
+        return deactivateRefresh.get();
+    }
+
+    public void setDeactivateRefresh(boolean deactivateRefresh) {
+        this.deactivateRefresh.set(deactivateRefresh);
+    }
+
+    public BooleanProperty deactivateRefreshProperty() {
+        return deactivateRefresh;
+    }
+
     @AllArgsConstructor
     private static class TreeNode {
         String label;