First preparations for Savepoints

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ASTDiff.java

@@ -93,6 +93,7 @@ public class ASTDiff extends DefaultASTVisitor<ASTNode> {
         return null;
     }
 
+
     @Override
     public ASTNode visit(TheOnlyStatement theOnly) {
         return null;

lang/src/main/java/edu/kit/iti/formal/psdbg/parser/ast/Statements.java

@@ -26,6 +26,7 @@ package edu.kit.iti.formal.psdbg.parser.ast;
 import edu.kit.iti.formal.psdbg.parser.ScriptLanguageParser;
 import edu.kit.iti.formal.psdbg.parser.Visitable;
 import edu.kit.iti.formal.psdbg.parser.Visitor;
+import lombok.NoArgsConstructor;
 import lombok.ToString;
 
 import java.util.*;
@@ -39,10 +40,16 @@ import java.util.stream.Stream;
  * @version 1 (27.04.17)
  */
 @ToString
+@NoArgsConstructor
 public class Statements extends ASTNode<ScriptLanguageParser.StmtListContext>
         implements Visitable, Iterable<Statement> {
     private final List<Statement> statements = new ArrayList<>();
 
+
+    public Statements(Statements body) {
+        statements.addAll(body.statements);
+    }
+
     public Iterator<Statement> iterator() {
         return statements.iterator();
     }

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

+package edu.kit.iti.formal.psdbg.interpreter.data;
+
+import edu.kit.iti.formal.psdbg.parser.ast.*;
+import lombok.Data;
+import lombok.Getter;
+import lombok.RequiredArgsConstructor;
+
+import java.io.File;
+
+@Data
+@RequiredArgsConstructor
+public class SavePoint   {
+
+    private final String savepointName;
+
+    private int start = -1;
+
+    private int end = -1;
+
+    public SavePoint(CallStatement call){
+        if(isSaveCommand(call)){
+            Parameters p = call.getParameters();
+            savepointName = ((StringLiteral) p.get(new Variable("#2"))).getText();
+            start = call.getRuleContext().getStart().getStartIndex();
+            end = call.getRuleContext().getStart().getStopIndex();
+        }
+        throw new IllegalArgumentException(call.getCommand()+" is not a save statement");
+    }
+
+    public static boolean isSaveCommand(CallStatement call){
+        return (call.getCommand().equals("save"));
+    }
+
+    public File getProofFile(File dir){
+        return new File(dir, savepointName+".proof");
+    }
+
+    public static boolean isSaveCommand(Statement statement) {
+        try{
+            CallStatement c = (CallStatement) statement;
+            return isSaveCommand(c);
+        }catch (ClassCastException e) {
+            return false;
+        }
+    }
+
+    public boolean isThisStatement(Statement statement) {
+        if(isSaveCommand(statement)){
+            CallStatement c = (CallStatement) statement;
+            return c.getCommand().equals(savepointName);
+
+        }
+        return false;
+    }
+}

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

@@ -30,14 +30,14 @@ import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 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.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
+import edu.kit.iti.formal.psdbg.parser.ast.Statements;
 import javafx.application.Platform;
 import javafx.beans.InvalidationListener;
 import javafx.beans.binding.BooleanBinding;
-import javafx.beans.property.BooleanProperty;
-import javafx.beans.property.SimpleBooleanProperty;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableList;
 import javafx.concurrent.Service;
@@ -602,6 +602,7 @@ public class DebuggerMain implements Initializable {
      */
     private void executeScript(InterpreterBuilder ib, boolean addInitBreakpoint) {
         try {
+
             Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
             // get possible scripts and the main script!
             List<ProofScript> scripts = scriptController.getCombinedAST();
@@ -621,6 +622,59 @@ public class DebuggerMain implements Initializable {
             LOGGER.debug("MainScript: {}", ms.getName());
 
             ib.setScripts(scripts);
+            executeScript0(ib, breakpoints, ms, addInitBreakpoint);
+        } catch (RecognitionException e) {
+            LOGGER.error(e);
+            Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
+        }
+            
+        }
+        
+        
+        
+        private void executeScriptFromSavePoint(InterpreterBuilder ib, SavePoint point) {
+        try {
+            Set<Breakpoint> breakpoints = scriptController.getBreakpoints();
+            // get possible scripts and the main script!
+            List<ProofScript> scripts = scriptController.getCombinedAST();
+            if (scriptController.getMainScript() == null) {
+                scriptController.setMainScript(scripts.get(0));
+            }
+            Optional<ProofScript> mainScript = scriptController.getMainScript().find(scripts);
+            ProofScript ms;
+            if (!mainScript.isPresent()) {
+                scriptController.setMainScript(scripts.get(0));
+                ms = scripts.get(0);
+            } else {
+                ms = mainScript.get();
+            }
+
+            Statements body = new Statements();
+            boolean flag =false;
+            for (int i = 0; i < ms.getBody().size(); i++) {
+                if(flag) {body.add(ms.getBody().get(i));
+                    continue;}
+                flag = point.isThisStatement(ms.getBody().get(i));
+            }
+
+            ms.setBody(body);
+
+            LOGGER.debug("Parsed Scripts, found {}", scripts.size());
+            LOGGER.debug("MainScript: {}", ms.getName());
+            //ib.setDirectory(model.getKeyFile() != null ? model.getKeyFile() : model.getJavaFile());
+            ib.setScripts(scripts);
+            executeScript0(ib, breakpoints, ms, false);
+        } catch (RecognitionException e) {
+            LOGGER.error(e);
+            Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
+        }
+            
+        }
+        
+        
+        private void executeScript0(InterpreterBuilder ib,
+                                    Collection<? extends Breakpoint> breakpoints,
+                                    ProofScript ms, boolean addInitBreakpoint) {
             KeyInterpreter interpreter = ib.build();
             DebuggerFramework<KeyData> df = new DebuggerFramework<>(interpreter, ms, null);
             df.setSucceedListener(this::onInterpreterSucceed);
@@ -631,12 +685,7 @@ public class DebuggerMain implements Initializable {
             df.getBreakpoints().addAll(breakpoints);
             df.getStatePointerListener().add(this::handleStatePointer);
             df.start();
-
             model.setDebuggerFramework(df);
-        } catch (RecognitionException e) {
-            LOGGER.error(e);
-            Utils.showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
-        }
     }
 
     private void onInterpreterSucceed(DebuggerFramework<KeyData> keyDataDebuggerFramework) {
@@ -1007,7 +1056,7 @@ public class DebuggerMain implements Initializable {
      */
     public void saveProof(ActionEvent actionEvent) {
         FileChooser fc = new FileChooser();
-        File file = fc.showOpenDialog(btnInteractiveMode.getScene().getWindow());
+        File file = fc.showSaveDialog(btnInteractiveMode.getScene().getWindow());
         if (file != null) {
             try {
                 saveProof(file);

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

@@ -11,15 +11,20 @@ import edu.kit.iti.formal.psdbg.gui.actions.inline.InlineActionSupplier;
 import edu.kit.iti.formal.psdbg.gui.controller.Events;
 import edu.kit.iti.formal.psdbg.gui.model.MainScriptIdentifier;
 import edu.kit.iti.formal.psdbg.gui.actions.acomplete.Suggestion;
+import edu.kit.iti.formal.psdbg.interpreter.data.SavePoint;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.Breakpoint;
 import edu.kit.iti.formal.psdbg.parser.Facade;
 import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
+import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
+import edu.kit.iti.formal.psdbg.parser.ast.Statement;
 import javafx.beans.property.ObjectProperty;
+import javafx.beans.property.SimpleListProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.beans.value.ChangeListener;
 import javafx.beans.value.ObservableValue;
 import javafx.collections.FXCollections;
+import javafx.collections.ObservableList;
 import javafx.collections.ObservableMap;
 import lombok.Getter;
 import lombok.Setter;
@@ -64,10 +69,37 @@ public class ScriptController {
     @Setter
     private DefaultAutoCompletionController autoCompleter = new DefaultAutoCompletionController();
 
+
+
     public ScriptController(DockPane parent) {
         this.parent = parent;
         Events.register(this);
         addDefaultInlineActions();
+
+        mainScript.addListener((p,o,n)-> {
+            if(o!=null)
+                o.getScriptArea().textProperty().removeListener( a-> updateSavePoints());
+            n.getScriptArea().textProperty().addListener(a->updateSavePoints());
+            updateSavePoints();
+        });
+
+
+    }
+
+    private ObservableList<SavePoint> mainScriptSavePoints
+            = new SimpleListProperty<>(FXCollections.observableArrayList());
+
+    private void updateSavePoints() {
+        Optional<ProofScript> ms = getMainScript().find(getCombinedAST());
+        if(ms.isPresent()) {
+            List<SavePoint> list = ms.get().getBody().stream()
+                    .filter(SavePoint::isSaveCommand)
+                    .map(a -> (CallStatement) a)
+                    .map(SavePoint::new)
+                    .collect(Collectors.toList());
+
+            mainScriptSavePoints.setAll(list);
+        }
     }
 
     private void addDefaultInlineActions() {
@@ -361,5 +393,11 @@ public class ScriptController {
         }
     }
 
+    public ObservableList<SavePoint> getMainScriptSavePoints() {
+        return mainScriptSavePoints;
+    }
 
+    public void setMainScriptSavePoints(ObservableList<SavePoint> mainScriptSavePoints) {
+        this.mainScriptSavePoints = mainScriptSavePoints;
+    }
 }
\ No newline at end of file

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

@@ -253,34 +253,14 @@ public class Utils {
 
     public static void showClosedProofDialog(String scriptName) {
         Alert alert = new Alert(Alert.AlertType.INFORMATION);
+
         alert.setTitle("Proof Closed");
         alert.setHeaderText("The proof is closed");
         alert.setContentText("The proof using " + scriptName + " is closed");
         alert.setWidth(500);
         alert.setHeight(400);
         alert.setResizable(true);
-        /*StringWriter sw = new StringWriter();
-        PrintWriter pw = new PrintWriter(sw);
-        ex.printStackTrace(pw);
-        String exceptionText = sw.toString();
-
-        Label label = new Label("The exception stacktrace was:");
-        TextArea textArea = new TextArea(exceptionText);
-        textArea.setEditable(false);
-        textArea.setWrapText(true);
 
-        textArea.setMaxWidth(Double.MAX_VALUE);
-        textArea.setMaxHeight(Double.MAX_VALUE);
-        GridPane.setVgrow(textArea, Priority.ALWAYS);
-        GridPane.setHgrow(textArea, Priority.ALWAYS);
-
-        GridPane expContent = new GridPane();
-        expContent.setMaxWidth(Double.MAX_VALUE);
-        expContent.addCell(label, 0, 0);
-        expContent.addCell(textArea, 0, 1);
-
-        alert.getDialogPane().setExpandableContent(expContent);
-        */
         alert.showAndWait();
     }