Gutter

+ close KeY
+ SaveAsScript Dialog
+ pruning savepoint load

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

@@ -77,10 +77,12 @@ import javax.swing.*;
 import java.awt.event.WindowAdapter;
 import java.awt.event.WindowEvent;
 import java.awt.event.WindowListener;
+import java.awt.event.WindowStateListener;
 import java.awt.im.InputContext;
 import java.io.*;
 import java.net.URL;
 import java.nio.charset.Charset;
+import java.security.Permission;
 import java.time.Duration;
 import java.util.*;
 import java.util.concurrent.*;
@@ -1190,6 +1192,8 @@ public class DebuggerMain implements Initializable {
 
     @FXML
     public void selectSavepoint(ActionEvent actionEvent) {
+        //TODO remove highlight of SPs
+
         SavePoint selected = cboSavePoints.getValue();
 
         if (selected == null) {
@@ -1197,11 +1201,9 @@ public class DebuggerMain implements Initializable {
             return;
         }
 
-        int currentpos = model.getDebuggerFramework().getCurrentStatePointer().getStatement().getStartPosition().getLineNumber();
-
-        //check intpreter finishes with which script
-        if (model.getInterpreterState().equals(InterpreterThreadState.FINISHED)
-                || selected.getLineNumber() <= currentpos && currentpos > 0) {
+        //prune to savepoint if possible
+        boolean pruneable = false;
+        try{
             Iterator<PTreeNode<KeyData>> iterator = model.getDebuggerFramework().getPtreeManager().getNodes().iterator();
             PTreeNode<KeyData> pTreeNodeOfSave;
             while (iterator.hasNext()) {
@@ -1217,41 +1219,8 @@ public class DebuggerMain implements Initializable {
             //TODO: refresh GUI (Context + Script)
             //State<KeyData> proofstate = KeyPersistentFacade.read(FACADE.getEnvironment(), FACADE.getProof(), new StringReader());
 
-        } else {
-
-
-        /*
-
-
-        // check if selected savepoint has been executed already -> prune to that savepoint
-
-
-        val statePointer = model.getDebuggerFramework().getCurrentStatePointer();
-        int currentpos = statePointer.getStatement().getStartPosition().getLineNumber();
-        if (model.getInterpreterState().equals(InterpreterThreadState.FINISHED)
-                || selected.getLineNumber() <= currentpos && currentpos > 0) {
-
-            System.out.println("Pruning to Savepoint.");
-
-                int line_statePointer = statePointer.getStatement().getStartPosition().getLineNumber();
-                int nrOfStepbacks = line_statePointer - selected.getLineNumber();
-
-                PTreeNode<KeyData> pTreeNodeOfSave = statePointer.getStepInvOver();
-                for (int i = 1; i <= nrOfStepbacks; i++) {
-                    pTreeNodeOfSave = statePointer.getStepInvOver();
-                }
-
-
-
-
-            model.getDebuggerFramework().getPtreeManager();
-            //TODO: find Node to prune
-            // FACADE.getProof().pruneProof(save);
-
+        } catch (Exception ex){
 
-    }
-
-    */
             //Hard Loading of Savepoint
             stopDebugMode(actionEvent);
 
@@ -1267,6 +1236,7 @@ public class DebuggerMain implements Initializable {
             handleStatePointerUI(null);
             //reload getInspectionViewsController().getActiveInspectionViewTab().getModel()
             InspectionModel iModel = getInspectionViewsController().getActiveInspectionViewTab().getModel();
+
             //iModel.setHighlightedJavaLines(FXCollections.emptyObservableSet());
             iModel.clearHighlightLines();
             iModel.getGoals().clear();
@@ -1293,15 +1263,17 @@ public class DebuggerMain implements Initializable {
             }
         }
 
+        //Update Gui
         MainScriptIdentifier msi = scriptController.getMainScript();
         msi.getScriptArea().setSavepointMarker(selected.getLineNumber());
-        //TODO underline ast
+        msi.getScriptArea().getCodeArea().setStyleClass(selected.getStartOffset(), selected.getEndOffset() + 1, "underlinesave");        scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
 
-        msi.getScriptArea().getCodeArea().setStyleClass(selected.getStartOffset(), selected.getEndOffset() + 1, "problem");
-        scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
-    }
+        //TODO: KeyPersistentFacade.read(FACADE.getEnvironment(), FACADE.getProof(), new StringReader(selected.getPersistedStateFile(FACADE.getFilepath()).toString()));
+        //TODO (NullpointerEx: interpreterbuilder == null): scriptExecutionController.executeScriptFromSavePoint(interpreterBuilder, selected);
 
 
+    }
+
 
     @FXML
     public void showWelcomeDock(ActionEvent actionEvent) {
@@ -1393,12 +1365,20 @@ public class DebuggerMain implements Initializable {
         }
 
         SwingUtilities.invokeLater(() -> {
+            SecurityManager secManager = new KeYSecurityManager();
+            System.setSecurityManager(secManager);
+
             // Swing Thread!
-            MainWindow keyWindow = MainWindow.getInstance();
-            keyWindow.addProblem(new SingleProof(FACADE.getProof(), "script"));
-            //keyWindow.getProofList().getModel().addProof();
-            keyWindow.makePrettyView();
-            keyWindow.setVisible(true);
+            try {
+                MainWindow keyWindow = MainWindow.getInstance();
+                keyWindow.addProblem(new SingleProof(FACADE.getProof(), "script"));
+                //keyWindow.getProofList().getModel().addProof();
+                keyWindow.makePrettyView();
+                keyWindow.setVisible(true);
+            } catch (SecurityException e) {
+                e.printStackTrace();
+            }
+
 
 
         });
@@ -1553,6 +1533,17 @@ public class DebuggerMain implements Initializable {
         }
     }
 
+
+    private class KeYSecurityManager extends SecurityManager {
+        @Override public void checkExit(int status) {
+            throw new SecurityException();
+        }
+
+        @Override public void checkPermission(Permission perm) {
+            // Allow other activities by default
+        }
+    }
+
     //endregion
 }
 //deprecated

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

@@ -388,6 +388,10 @@ public class ScriptArea extends BorderPane {
         }
     }
 
+    public void underlineSavepoint(){
+
+    }
+
     private void highlightNonExecutionArea() {
         if (hasExecutionMarker()) {
             LOGGER.debug("getExecutionMarkerPosition() = " + getExecutionMarkerPosition());

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

@@ -97,24 +97,27 @@ public class ScriptController {
     }
 
     private void updateSavePoints() {
-        try{
-        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);
-
-            //set alert gutter annotations
-            List<SavePoint> noForceSp = mainScriptSavePoints.stream()
-                    .filter(a -> a.getForce().equals(SavePoint.ForceOption.NO))
-                    .collect(Collectors.toList());
-            noForceSp.forEach( e -> getMainScript().getScriptArea().setAlertMarker(e.getLineNumber()));
-
-            loggerConsole.info("Found savepoints: " + list);
+        try {
+            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);
+
+                //set alert gutter annotations
+                List<SavePoint> noForceSp = mainScriptSavePoints.stream()
+                        .filter(a -> a.getForce().equals(SavePoint.ForceOption.NO))
+                        .collect(Collectors.toList());
+                noForceSp.forEach(e -> getMainScript().getScriptArea().setAlertMarker(e.getLineNumber()));
+
+                loggerConsole.info("Found savepoints: " + list);
+            }
+        } catch (Exception e) {
+
         }
     }
 

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less

@@ -115,6 +115,13 @@
     -fx-underline: true;
   }
 
+   .underlinesave {
+        -rtfx-underline-cap: butt;
+        -rtfx-underline-color: @cyan;
+        -rtfx-underline-width: 2px;
+        -fx-underline: true;
+    }
+
   .line-highlight-postmortem {
 //    -rtfx-background-color: @cyan;
     -rtfx-background-color: @screenShotMarkerBase;