diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/ShortCommandPrinter.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/ShortCommandPrinter.java
new file mode 100644
index 0000000000000000000000000000000000000000..07091f1fef4236b92c84b0f27f81e1e462dd5de1
--- /dev/null
+++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/ShortCommandPrinter.java
@@ -0,0 +1,60 @@
+package edu.kit.iti.formal.psdbg;
+
+import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
+import edu.kit.iti.formal.psdbg.parser.Facade;
+import edu.kit.iti.formal.psdbg.parser.ast.*;
+
+/**
+ * Prints every command to a single line representation.
+ *
+ * @author Alexander Weigl
+ * @version 1
+ */
+public class ShortCommandPrinter extends DefaultASTVisitor<String> {
+    @Override
+    public String defaultVisit(ASTNode node) {
+        return (Facade.prettyPrint(node));
+    }
+
+    @Override
+    public String visit(ProofScript proofScript) {
+        return String.format("script %s (%s) {%n",
+                proofScript.getName(),
+                Facade.prettyPrint(proofScript.getSignature()));
+    }
+
+    @Override
+    public String visit(CasesStatement casesStatement) {
+        return "cases {";
+    }
+
+    @Override
+    public String visit(SimpleCaseStatement caseStatement) {
+        return "case " + Facade.prettyPrint(caseStatement.getGuard());
+    }
+
+    @Override
+    public String visit(TryCase tryCase) {
+        return "try " + Facade.prettyPrint(tryCase.getBody());
+    }
+
+    @Override
+    public String visit(ClosesCase closesCase) {
+        return "closes with {" + Facade.prettyPrint(closesCase.getClosesScript()) + "}";
+    }
+
+    @Override
+    public String visit(TheOnlyStatement theOnly) {
+        return "theonly {";
+    }
+
+    @Override
+    public String visit(ForeachStatement foreach) {
+        return "foreach {";
+    }
+
+    @Override
+    public String visit(RepeatStatement repeatStatement) {
+        return ("repeat {");
+    }
+}
diff --git a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java
index 6df83d8973baaa854c1ded135b6377f11350449f..03b6cefb480af79de6f8c63ae42ce73816519b48 100644
--- a/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java
+++ b/lang/src/main/java/edu/kit/iti/formal/psdbg/parser/PrettyPrinter.java
@@ -41,12 +41,15 @@ import java.util.Map;
 public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
     private final StringBuilder s = new StringBuilder();
+
     @Getter
     @Setter
     private int maxWidth = 80;
+
     @Getter
     @Setter
     private boolean unicode = true;
+
     private int indentation = 0;
 
     @Override
@@ -187,8 +190,11 @@ public class PrettyPrinter extends DefaultASTVisitor<Void> {
 
     @Override
     public Void visit(CallStatement call) {
-        s.append(call.getCommand()).append(' ');
-        call.getParameters().accept(this);
+        s.append(call.getCommand());
+        if (call.getParameters().size() != 0) {
+            s.append(' ');
+            call.getParameters().accept(this);
+        }
         s.append(";");
         return null;
     }
diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/InteractiveCLIDebugger.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/InteractiveCLIDebugger.java
index 27fa0a503810ccab8bc9220a3d9d5ce82717e164..bb979511f0d987bd853eaaa9a7d03ecf0469888d 100644
--- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/InteractiveCLIDebugger.java
+++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/InteractiveCLIDebugger.java
@@ -9,7 +9,6 @@ import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
 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.dbg.*;
-import edu.kit.iti.formal.psdbg.parser.DefaultASTVisitor;
 import edu.kit.iti.formal.psdbg.parser.Facade;
 import edu.kit.iti.formal.psdbg.parser.ast.*;
 import org.apache.logging.log4j.LogManager;
@@ -82,7 +81,7 @@ public class InteractiveCLIDebugger {
         System.out.println("digraph G {");
         for (PTreeNode<KeyData> n : df.getStates()) {
             System.out.format("%d [label=\"%s@%s (G: %d)\"]%n", n.hashCode(),
-                    n.getStatement().accept(new CommandPrinter()),
+                    n.getStatement().accept(new ShortCommandPrinter()),
                     n.getStatement().getStartPosition().getLineNumber(),
                     n.getStateBeforeStmt().getGoals().size()
             );
@@ -154,7 +153,7 @@ public class InteractiveCLIDebugger {
     private void printNode(PTreeNode<KeyData> node) {
         System.out.format("%3d: %s%n",
                 node.getStatement().getStartPosition().getLineNumber(),
-                node.getStatement().accept(new CommandPrinter())
+                node.getStatement().accept(new ShortCommandPrinter())
         );
 
         for (GoalNode<KeyData> gn : node.getStateBeforeStmt().getGoals()) {
@@ -171,52 +170,3 @@ public class InteractiveCLIDebugger {
         //df.addBreakpoint(breakpoint);
     }
 }
-
-class CommandPrinter extends DefaultASTVisitor<String> {
-    @Override
-    public String defaultVisit(ASTNode node) {
-        return (Facade.prettyPrint(node));
-    }
-
-    @Override
-    public String visit(ProofScript proofScript) {
-        return String.format("script %s (%s) {%n",
-                proofScript.getName(),
-                Facade.prettyPrint(proofScript.getSignature()));
-    }
-
-    @Override
-    public String visit(CasesStatement casesStatement) {
-        return "cases {";
-    }
-
-    @Override
-    public String visit(SimpleCaseStatement caseStatement) {
-        return "case " + Facade.prettyPrint(caseStatement.getGuard());
-    }
-
-    @Override
-    public String visit(TryCase tryCase) {
-        return "try " + Facade.prettyPrint(tryCase.getBody());
-    }
-
-    @Override
-    public String visit(ClosesCase closesCase) {
-        return "closes with {" + Facade.prettyPrint(closesCase.getClosesScript()) + "}";
-    }
-
-    @Override
-    public String visit(TheOnlyStatement theOnly) {
-        return "theonly {";
-    }
-
-    @Override
-    public String visit(ForeachStatement foreach) {
-        return "foreach {";
-    }
-
-    @Override
-    public String visit(RepeatStatement repeatStatement) {
-        return ("repeat {");
-    }
-}
diff --git a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
index d2c4ebe3e8eb3f28791b4c209eb9a40ff5aa7287..17dc6cfcc0b95f08e38de39cc2a16cd20c063399 100644
--- a/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
+++ b/rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/KeYProofFacade.java
@@ -50,9 +50,36 @@ public class KeYProofFacade {
      * BooleanProperty inidcating whether KeY finished loading
      */
     private BooleanBinding readyToExecute = proof.isNotNull();
+
     //Workaround until api is relaxed
     private ProofManagementApi pma;
 
+    /**
+     *
+     */
+    public ProofState getProofState() {
+        Proof p = proof.get();
+        if (p == null)
+            return ProofState.EMPTY;
+
+        if (p.root().childrenCount() == 0)
+            return ProofState.VIRGIN;
+
+        return ProofState.DIRTY;
+    }
+
+    /**
+     * reload the current proof. synchronously because only the first load is slow.
+     */
+    public void reload() throws ProofInputException, ProblemLoaderException {
+        if (contract.get() != null) {// reinstante the contract
+            setProof(getEnvironment().createProof(
+                    contract.get().getProofObl(getEnvironment().getServices())));
+        } else {
+            setProof(KeYApi.loadFromKeyFile(proof.get().getProofFile()).getLoadedProof().getProof());
+        }
+    }
+
     //region loading
     public Task<ProofApi> loadKeyFileTask(File keYFile) {
         Task<ProofApi> task = new Task<ProofApi>() {
@@ -117,14 +144,13 @@ public class KeYProofFacade {
         proof.set(pa.getProof());
         contract.set(null);
     }
-    //endregion
 
     /**
      * Build the KeYInterpreter that handles the execution of the loaded key problem sourceName
      */
     public InterpreterBuilder buildInterpreter() {
         assert readyToExecute.getValue();
-
+        assert getEnvironment() != null && getProof() != null : "No proof loaded";
         InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
         interpreterBuilder
                 .proof(environment.get(), proof.get())
@@ -136,7 +162,7 @@ public class KeYProofFacade {
 
         return interpreterBuilder;
     }
-
+    //endregion
 
     /**
      * Reload all KeY structure if proof should be reloaded
@@ -202,6 +228,10 @@ public class KeYProofFacade {
         KeyData data = new KeyData(proof.get().root(), getEnvironment(), getProof());
         return Collections.singleton(new GoalNode<>(null, data, data.getNode().isClosed()));
     }
+
+    public enum ProofState {
+        EMPTY, VIRGIN, DIRTY;
+    }
     //endregion
 }
 
diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Blocker.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Blocker.java
index 18631f319bf4f33b85c028957de7e6cf20548ac1..d5380239378d23ff376f47a0a95978c71c582167 100644
--- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Blocker.java
+++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Blocker.java
@@ -9,8 +9,8 @@ import lombok.Getter;
 import lombok.RequiredArgsConstructor;
 import lombok.val;
 
+import java.util.HashSet;
 import java.util.Set;
-import java.util.TreeSet;
 import java.util.concurrent.atomic.AtomicInteger;
 import java.util.function.Predicate;
 
@@ -25,7 +25,7 @@ public abstract class Blocker {
         private final Interpreter<T> interpreter;
 
         @Getter
-        private final Set<Breakpoint> breakpoints = new TreeSet<>();
+        private final Set<Breakpoint> breakpoints = new HashSet<>();
 
         private final Breakpoint cmp = new Breakpoint(null, 0);
 
@@ -52,7 +52,7 @@ public abstract class Blocker {
                     }
                 }
             }
-            return breakpoints.contains(cmp);
+            return false;
         }
     }
 
@@ -66,8 +66,9 @@ public abstract class Blocker {
 
         @Override
         public boolean test(ASTNode astNode) {
-            if (stepUntilBlock.get() >= 0) {
-                return 0 == stepUntilBlock.decrementAndGet();
+            int value;
+            if ((value = stepUntilBlock.decrementAndGet()) >= 0) {
+                return 0 == value;
             }
             return false;
         }
diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Breakpoint.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Breakpoint.java
index 8c9a633b1c0d26b36548981e779b0831ba602ca4..c4a26c4d184523b3e70c0770e6bf7bc4420afa60 100644
--- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Breakpoint.java
+++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/Breakpoint.java
@@ -3,9 +3,11 @@ package edu.kit.iti.formal.psdbg.interpreter.dbg;
 import edu.kit.iti.formal.psdbg.parser.Facade;
 import edu.kit.iti.formal.psdbg.parser.ast.Expression;
 import lombok.Data;
+import lombok.EqualsAndHashCode;
 import org.antlr.v4.runtime.CharStreams;
 
 @Data
+@EqualsAndHashCode(of = {"sourceName", "lineNumber"})
 public class Breakpoint {
     private String sourceName;
 
diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java
index e3ab5d1012b65beff258306969a383b39851c2a6..00ab2eabcf3034b04e5dec0140f3f0c4f9ebd3d8 100644
--- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java
+++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/PTreeNode.java
@@ -1,17 +1,16 @@
 package edu.kit.iti.formal.psdbg.interpreter.dbg;
 
+import edu.kit.iti.formal.psdbg.ShortCommandPrinter;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
 import edu.kit.iti.formal.psdbg.parser.ast.CaseStatement;
-import edu.kit.iti.formal.psdbg.parser.ast.Parameters;
-import lombok.*;
+import lombok.Getter;
+import lombok.RequiredArgsConstructor;
+import lombok.Setter;
 
 import javax.annotation.Nullable;
-import java.util.Collections;
-import java.util.HashMap;
-import java.util.List;
-import java.util.Map;
+import java.util.*;
 
 /**
  * PTreeNode represents a node in the state graph.
@@ -23,29 +22,34 @@ import java.util.Map;
  */
 @Getter
 @Setter
-@ToString
 @RequiredArgsConstructor
 public class PTreeNode<T> {
     private final ASTNode statement;
 
     private Map<CaseStatement, List<GoalNode<T>>> mappingOfCaseToStates = new HashMap<>();
+
     private State<T> stateBeforeStmt;
+
     private State<T> stateAfterStmt;
+
     private ASTNode[] context;
 
     private boolean atomic;
 
     @Nullable
     private PTreeNode<T> stepInto;
+
     @Nullable
     private PTreeNode<T> stepOver;
+
     @Nullable
     private PTreeNode<T> stepInvOver;
+
     @Nullable
     private PTreeNode<T> stepInvInto;
+
     @Nullable
     private PTreeNode<T> stepReturn;
-    private Parameters goals;
 
     public void connectStepOver(PTreeNode<T> jumpOverTo) {
         setStepOver(jumpOverTo);
@@ -60,4 +64,36 @@ public class PTreeNode<T> {
     public List<GoalNode<T>> getActiveGoalsForCase(CaseStatement caseStmt) {
         return mappingOfCaseToStates.getOrDefault(caseStmt, Collections.emptyList());
     }
+
+    public List<PTreeNode<T>> getContextNodes() {
+        List<PTreeNode<T>> contextNodes = new ArrayList<>(context.length);
+        PTreeNode<T> cur = this;
+        outer : do {
+            // add the current node, and every node that can be reached by an inverse into pointer.
+            contextNodes.add(cur);
+
+            // if the current node doesn't have an inverse into pointer, then trace
+            // inverse over pointer (same context)
+            while (cur.getStepInvInto() == null) {
+                cur = cur.getStepInvOver();
+                if (cur == null) break outer; // we could reach the beginning of execution
+            }
+            cur = cur.getStepInvInto();
+        } while (cur != null);
+        return contextNodes;
+    }
+
+    public String getSingleRepresentation() {
+        if (getStatement().getStartPosition() != null)
+            return String.format("%d: %s",
+                    getStatement().getStartPosition().getLineNumber(),
+                    getStatement().accept(new ShortCommandPrinter()));
+        else
+            return (String) getStatement().accept(new ShortCommandPrinter());
+    }
+
+    @Override
+    public String toString() {
+        return getSingleRepresentation();
+    }
 }
\ No newline at end of file
diff --git a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java
index f58795243e8f66849d1edf5dd5b22aa14df69ca3..3496131597472e39bc6ee218a0379067ab0c36e1 100644
--- a/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java
+++ b/rt/src/main/java/edu/kit/iti/formal/psdbg/interpreter/dbg/ProofTreeManager.java
@@ -159,4 +159,5 @@ public class ProofTreeManager<T> {
         if (!suppressStatePointerListener)
             statePointerListener.forEach(l -> l.accept(statePointer));
     }
+
 }
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
index 9aeef553a4c0a6dca4551a0dff8fcf68b0f4cae7..dabc798d533aeba117862d9a35d9921719538d6d 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java
@@ -4,11 +4,14 @@ 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.init.ProofInputException;
+import de.uka.ilkd.key.proof.io.ProblemLoaderException;
 import de.uka.ilkd.key.speclang.Contract;
+import edu.kit.iti.formal.psdbg.StepIntoCommand;
 import edu.kit.iti.formal.psdbg.examples.Examples;
 import edu.kit.iti.formal.psdbg.gui.ProofScriptDebugger;
 import edu.kit.iti.formal.psdbg.gui.controls.*;
 import edu.kit.iti.formal.psdbg.gui.model.DebuggerMainModel;
+import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
 import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
@@ -105,19 +108,28 @@ public class DebuggerMain implements Initializable {
 
         //register the welcome dock in the center
         welcomePaneDock.dock(dockStation, DockPos.LEFT);
-        registerToolbarToStatusBar();
         //statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
         marriageJavaCode();
 
         //marriage key proof facade to proof tree
         getFacade().proofProperty().addListener(
                 (prop, o, n) -> {
-                    proofTree.setRoot(n.root());
+                    if (n == null) {
+                        proofTree.setRoot(null);
+                    } else {
+                        proofTree.setRoot(n.root());
+                        getInspectionViewsController().getActiveInspectionViewTab()
+                                .getModel().getGoals().setAll(FACADE.getPseudoGoals());
+                    }
                     proofTree.setProof(n);
-                    getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals());
                 }
         );
 
+        //
+        model.statePointerProperty().addListener((prop, o, n) -> {
+            this.handleStatePointerUI(n);
+        });
+
         //Debugging
         Utils.addDebugListener(model.javaCodeProperty());
         Utils.addDebugListener(model.executeNotPossibleProperty(), "executeNotPossible");
@@ -125,6 +137,7 @@ public class DebuggerMain implements Initializable {
         initializeExamples();
     }
 
+
     /**
      * If the mouse moves other toolbar button, the help text should display in the status bar
      */
@@ -137,7 +150,8 @@ public class DebuggerMain implements Initializable {
     }
 
     /**
-     * *Note:* This is executed in the Interpreter!
+     * <b>Note:</b> This is executed in the Interpreter Thread!
+     * You should listen to the {@link DebuggerMainModel#statePointerProperty}
      *
      * @param node
      */
@@ -145,6 +159,29 @@ public class DebuggerMain implements Initializable {
         Platform.runLater(() -> model.setStatePointer(node));
     }
 
+    /**
+     * Handling of a new state in the {@link DebuggerFramework}, now in the JavaFX Thread
+     *
+     * @see {@link #handleStatePointer(PTreeNode)}
+     */
+    private void handleStatePointerUI(PTreeNode<KeyData> node) {
+        InspectionModel im = getInspectionViewsController().getActiveInspectionViewTab().getModel();
+
+        im.getGoals().setAll(
+                node.getStateBeforeStmt().getGoals()
+        );
+        im.setSelectedGoalNodeToShow(
+                node.getStateBeforeStmt().getSelectedGoalNode());
+
+        scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
+
+        //Experimental
+        ComboBox<PTreeNode<KeyData>> frames = getInspectionViewsController().getActiveInspectionViewTab().getFrames();
+        List<PTreeNode<KeyData>> ctxn = node.getContextNodes();
+        frames.getItems().setAll(ctxn);
+        frames.getSelectionModel().select(node);
+    }
+
     private void marriageJavaCode() {
         //Listener on chosenContract from
         model.chosenContractProperty().addListener(o -> {
@@ -217,30 +254,6 @@ public class DebuggerMain implements Initializable {
         }
     }
 
-    /**
-     * Reload the KeY environment, to execute the script again
-     * TODO: reload views
-     *
-     * @param file
-     * @param keyfile
-     * @return
-     */
-    public Task<Void> reloadEnvironment(File file, boolean keyfile) {
-        Task<Void> task = new Task<Void>() {
-            @Override
-            protected Void call() throws Exception {
-                FACADE.reloadEnvironment();
-                if (keyfile) {
-                    openKeyFile(file);
-                } else {
-                    openJavaFile(file);
-                }
-                return null;
-            }
-        };
-        return task;
-    }
-
     @FXML
     public void executeScript() {
         executeScript(false);
@@ -283,32 +296,25 @@ public class DebuggerMain implements Initializable {
 
         assert model.getDebuggerFramework() == null : "There should not be any interpreter running.";
 
-        File file;
-        boolean isKeyfile = false;
-        if (model.getJavaFile() != null) {
-            file = model.getJavaFile();
-        } else {
-            isKeyfile = true;
-            file = model.getKeyFile();
+        if (FACADE.getProofState() == KeYProofFacade.ProofState.EMPTY) {
+            Alert alert = new Alert(Alert.AlertType.ERROR, "No proof loaded!", ButtonType.OK);
+            alert.showAndWait();
+            return;
         }
 
+        if (FACADE.getProofState() == KeYProofFacade.ProofState.DIRTY) {
+            try {
+                FACADE.reload();
+            } catch (ProofInputException | ProblemLoaderException e) {
+                //TODO
+                Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
+                        e
+                );
+            }
+        }
 
-        Task<Void> reloading = reloadEnvironment(file, isKeyfile);
-        reloading.setOnSucceeded(event -> {
-            statusBar.publishMessage("Cleared and Reloaded Environment");
-            executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
-        });
-
-        reloading.setOnFailed(event -> {
-            event.getSource().exceptionProperty().get();
-            Utils.showExceptionDialog("Loading Error", "Could not clear Environment", "There was an error when clearing old environment",
-                    (Throwable) event.getSource().exceptionProperty().get()
-            );
-        });
-
-        ProgressBar bar = new ProgressBar();
-        bar.progressProperty().bind(reloading.progressProperty());
-        executorService.execute(reloading);
+        // else getProofState() == VIRGIN!
+        executeScript(FACADE.buildInterpreter(), addInitBreakpoint);
     }
 
 
@@ -342,9 +348,10 @@ public class DebuggerMain implements Initializable {
             KeyInterpreter interpreter = ib.build();
             DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, ms, null);
             if (addInitBreakpoint) {
-                df.releaseUntil(new Blocker.CounterBlocker(0)); // just execute
+                df.releaseUntil(new Blocker.CounterBlocker(1)); // just execute
             }
             df.getBreakpoints().addAll(breakpoints);
+            df.getStatePointerListener().add(this::handleStatePointer);
             df.start();
 
             model.setDebuggerFramework(df);
@@ -363,7 +370,7 @@ public class DebuggerMain implements Initializable {
     public void executeToBreakpoint() {
         Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
         if (breakpoints.size() == 0) {
-            System.out.println(scriptController.mainScriptProperty().get().getLineNumber());
+            //System.out.println(scriptController.mainScriptProperty().get().getLineNumber());
             //we need to add breakpoint at end if no breakpoint exists
         }
         executeScript(false);
@@ -561,6 +568,21 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+
+    /**
+     * Perform a step into
+     * @param actionEvent
+     */
+    public void stepInto(ActionEvent actionEvent) {
+        LOGGER.debug("DebuggerMain.stepOver");
+        try {
+            model.getDebuggerFramework().execute(new StepIntoCommand<>());
+        } catch (DebuggerException e) {
+            Utils.showExceptionDialog("", "", "", e);
+            LOGGER.error(e);
+        }
+    }
+
     /**
      * Perform a step back
      *
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java
index c53f20c179186b982fc3d287c1893d574adfeeb3..3874a9fc78b47df16a5296f674bbaaaf67a03be9 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java
@@ -3,12 +3,14 @@ package edu.kit.iti.formal.psdbg.gui.controls;
 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.dbg.PTreeNode;
 import javafx.beans.Observable;
 import javafx.beans.property.ReadOnlyObjectProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.collections.FXCollections;
 import javafx.fxml.FXML;
 import javafx.scene.Node;
+import javafx.scene.control.ComboBox;
 import javafx.scene.control.ListCell;
 import javafx.scene.control.ListView;
 import javafx.scene.control.TextField;
@@ -18,6 +20,8 @@ import javafx.scene.input.KeyCombination;
 import javafx.scene.input.MouseEvent;
 import javafx.scene.layout.BorderPane;
 import javafx.scene.layout.HBox;
+import javafx.util.StringConverter;
+import lombok.Getter;
 
 /**
  * Right part of the splitpane that displays the different parts of a state
@@ -29,11 +33,14 @@ public class InspectionView extends BorderPane {
             new InspectionModel()
     );
 
+    public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
+
+    @FXML @Getter
+    private ComboBox<PTreeNode<KeyData>> frames;
+
     @FXML
     private TextField txtSearchPattern;
 
-    public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
-
     @FXML
     private SequentView sequentView;
 
@@ -46,6 +53,26 @@ public class InspectionView extends BorderPane {
     public InspectionView() {
         Utils.createWithFXML(this);
 
+        frames.valueProperty().addListener((prop, o, n) -> {
+                    model.get().getGoals().setAll(
+                            n.getStateBeforeStmt().getGoals());
+                    model.get().setSelectedGoalNodeToShow(
+                            n.getStateBeforeStmt().getSelectedGoalNode());
+                }
+        );
+
+        frames.setConverter(new StringConverter<PTreeNode<KeyData>>() {
+            @Override
+            public String toString(PTreeNode<KeyData> object) {
+                return object.getSingleRepresentation();
+            }
+
+            @Override
+            public PTreeNode<KeyData> fromString(String string) {
+                return null;
+            }
+        });
+
         model.get().selectedGoalNodeToShowProperty().addListener((o, a, b) -> {
             goalView.getSelectionModel().select(b);
         });
@@ -72,7 +99,7 @@ public class InspectionView extends BorderPane {
 
         final KeyCombination kb = new KeyCodeCombination(KeyCode.F, KeyCombination.SHORTCUT_DOWN);
         sequentView.setOnKeyReleased(event -> {
-           // System.out.println(event);
+            // System.out.println(event);
             if (kb.match(event)) {
                 event.consume();
                 //nice animation here
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
index 646aa0fc67ff1b1d49bd275a0d7ce3d0a8eb96d7..4fdb2fea2caf2e2de08e7131caae7f453432ea4f 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
@@ -94,7 +94,8 @@ public class ProofTree extends BorderPane {
             if (old != null) {
                 old.removeProofTreeListener(proofTreeListener);
             }
-            n.addProofTreeListener(proofTreeListener);
+            if (n != null)
+                n.addProofTreeListener(proofTreeListener);
         });
         init();
     }
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
index 5da1113ffd6593f882af5c6130ab3728ee800e2d..1152e19224936362bd3f85c5a84060d973e69c29 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptArea.java
@@ -120,7 +120,7 @@ public class ScriptArea extends CodeArea {
         textProperty().addListener((prop, oldValue, newValue) -> {
             dirty.set(true);
             if (newValue.isEmpty()) {
-                System.err.println("text cleared");
+                LOGGER.debug("text cleared");
             } else {
                 updateMainScriptMarker();
                 updateHighlight();
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java
index 96f5f34457dfbb0b5b14bc19d21116fc5338c839..2ba7181ae4e824eda855758e3c5e2c16e25fdb7b 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ScriptController.java
@@ -65,18 +65,21 @@ public class ScriptController {
     @Subscribe
     public void handle(Events.NewNodeExecuted newNode) {
         logger.debug("Handling new node added event!");
-
         ASTNode scriptNode = newNode.getCorrespondingASTNode();
-        ScriptArea editor = findEditor(scriptNode);
+        highlightASTNode(newNode.getCorrespondingASTNode());
+    }
+
+    public void highlightASTNode(ASTNode node) {
+        ScriptArea editor = findEditor(node);
         editor.removeExecutionMarker();
         LineMapping lm = new LineMapping(editor.getText());
-        int pos = lm.getLineEnd(scriptNode.getStartPosition().getLineNumber() - 1);
-        System.out.println(pos);
-        //    editor.insertExecutionMarker(pos);
+        int pos = lm.getLineEnd(node.getStartPosition().getLineNumber() - 1);
+        logger.debug("Highlight position: {}", pos);
+        // editor.insertExecutionMarker(pos);
     }
 
     private ScriptArea findEditor(ASTNode node) {
-        File f = new File(node.getRuleContext().getStart().getInputStream().getSourceName());
+        File f = new File(node.getOrigin());
         return findEditor(f);
     }
 
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
index 39588860b025db1ab3b167ae7a72c685be041e61..b863e29f0455105651a2abb6df239d1240ba9e67 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/SequentView.java
@@ -36,12 +36,19 @@ public class SequentView extends CodeArea {
     private Services services;
 
     private LogicPrinter lp;
+
     private IdentitySequentPrintFilter filter;
+
     private LogicPrinter.PosTableStringBackend backend;
+
     private SimpleObjectProperty<de.uka.ilkd.key.proof.Goal> goal = new SimpleObjectProperty<>();
+
     private SimpleObjectProperty<de.uka.ilkd.key.proof.Node> node = new SimpleObjectProperty<>();
+
     private ObservableBooleanValue rulesAvailable = goal.isNotNull();
+
     private KeYProofFacade keYProofFacade;
+
     private TacletContextMenu menu;
 
 
@@ -57,12 +64,15 @@ public class SequentView extends CodeArea {
         if (backend == null) return;
         CharacterHit hit = hit(mouseEvent.getX(), mouseEvent.getY());
         int insertionPoint = hit.getInsertionIndex();
-        PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
-        if (pis != null) {
-            Range r = backend.getPositionTable().rangeForIndex(insertionPoint, getLength());
-            hightlightRange(r.start(), r.end());
-        } else {
-            hightlightRange(0, 0);
+        try {
+            PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
+            if (pis != null) {
+                Range r = backend.getPositionTable().rangeForIndex(insertionPoint, getLength());
+                hightlightRange(r.start(), r.end());
+            } else {
+                hightlightRange(0, 0);
+            }
+        } catch (NullPointerException npe) {
         }
         mouseEvent.consume();
     }
diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml
index 8e39ac59c997c8ecf805d4329aa5f8b7a114cd57..27d37db603ba586df063c62c5d8be6b36237223f 100644
--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml
@@ -118,7 +118,7 @@
                         </SplitMenuButton>
 
 
-                        <Button disable="${controller.stepNotPossible}">
+                        <Button onAction="#stepInto" disable="${controller.stepNotPossible}">
                             <graphic>
                                 <MaterialDesignIconView glyphName="DEBUG_STEP_INTO" size="24.0"/>
                             </graphic>
diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.fxml
index c447defaa59c971e22e08a23f492690aec2a6393..894d6ac3bb6087bc8a633e3d9da5a9a9a5a324a1 100644
--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.fxml
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.fxml
@@ -4,8 +4,7 @@
 <?import edu.kit.iti.formal.psdbg.gui.controls.SectionPane?>
 <?import edu.kit.iti.formal.psdbg.gui.controls.SequentView?>
 <?import javafx.scene.control.*?>
-<?import javafx.scene.layout.BorderPane?>
-<?import javafx.scene.layout.HBox?>
+<?import javafx.scene.layout.*?>
 <fx:root xmlns:fx="http://javafx.com/fxml"
          xmlns="http://javafx.com/javafx"
          type="javafx.scene.layout.BorderPane"
@@ -22,7 +21,14 @@
                         </Button>
                     </headerRight>
                     <center>
-                        <ListView fx:id="goalView"/>
+                        <VBox>
+                            <!--<BreadCrumbBar fx:id="frames"/>-->
+                            <HBox alignment="BASELINE_LEFT">
+                                <Label labelFor="$frames" text="Contexts:"  />
+                                <ComboBox fx:id="frames" />
+                            </HBox>
+                            <ListView fx:id="goalView"/>
+                        </VBox>
                     </center>
                 </SectionPane>