save without selectors

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/funchdl/SaveCommand.java

+package edu.kit.iti.formal.psdbg.interpreter.funchdl;
+
+import edu.kit.iti.formal.psdbg.interpreter.Interpreter;
+import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
+import edu.kit.iti.formal.psdbg.interpreter.data.VariableAssignment;
+import edu.kit.iti.formal.psdbg.interpreter.funchdl.BuiltinCommands;
+import edu.kit.iti.formal.psdbg.interpreter.funchdl.CommandHandler;
+import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
+import lombok.Getter;
+import lombok.RequiredArgsConstructor;
+import lombok.Setter;
+import sun.security.ssl.Debug;
+
+import javax.annotation.Nullable;
+import java.io.File;
+import java.io.IOException;
+import java.sql.Savepoint;
+import java.util.ArrayList;
+import java.util.List;
+
+public class SaveCommand implements CommandHandler<KeyData>{
+
+    @Getter @Setter
+    private File path;
+
+    public SaveCommand(File path) {
+        this.path = path;
+    }
+
+
+    @Override
+    public boolean handles(CallStatement call, @Nullable KeyData data) throws IllegalArgumentException {
+        return call.getCommand().equals("save");
+    }
+
+    @Override
+    public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params, KeyData data) {
+        SavePoint sp = new SavePoint(call);
+
+        //Not via Parentpath -> dependency on OS
+        String parentpath = path.getAbsolutePath();
+        parentpath = parentpath.substring(0, parentpath.length() - path.getName().length());
+
+        File newfile = new File(parentpath + sp.getSavepointName() + ".key");
+        System.out.println("(Safepoint) Location to be saved to = " + newfile.getAbsolutePath());
+        try {
+            interpreter.getSelectedNode().getData().getProof().saveToFile(newfile);
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+
+
+    }
+}
+
+
+
+
+
+
+

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

@@ -694,8 +694,10 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
             GoalNode<T> selectedGoalNode = stateStack.peek().getSelectedGoalNode();
             if (selectedGoalNode != null) {
                 assert stateStack.peek().getGoals().contains(selectedGoalNode);
+                return selectedGoalNode;
+            }else{
+                throw new IllegalStateException();
             }
-            return selectedGoalNode;
         } catch (IllegalStateException e) {
             if (strictMode)
                 throw e;

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

@@ -254,6 +254,7 @@ public class DebuggerMain implements Initializable {
         Events.register(this);
        // model.setDebugMode(false);
         scriptController = new ScriptController(dockStation);
+        //TODO:
         interactiveModeController = new InteractiveModeController(scriptController);
         btnInteractiveMode.setSelected(false);
         inspectionViewsController = new InspectionViewsController(dockStation);
@@ -399,8 +400,6 @@ public class DebuggerMain implements Initializable {
             @Override
             public void onChanged(Change<? extends SavePoint> c) {
 
-
-
                 if(scriptController.getMainScriptSavePoints().size() > 0){
                     combo_savepoints.setItems(scriptController.getMainScriptSavePoints());
 

ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps

@@ -4,7 +4,14 @@ script test123() {
   impRight;
 save 'test1';
   impLeft;
-//save 'test2';
+
+}
+
+script test2open() {
+  impRight;
+  impRight;
+  impLeft;
+  save 'test2';
 }
 
 script autoScript(){