fixing repeat

rt-key/src/main/java/edu/kit/iti/formal/psdbg/interpreter/exceptions/ScriptCommandNotApplicableException.java

@@ -6,7 +6,7 @@ import java.util.Map;
 /**
  * Exception for not applicable Rules
  */
-public class ScriptCommandNotApplicableException extends RuntimeException {
+public class ScriptCommandNotApplicableException extends InterpreterRuntimeException {
 
     public ScriptCommandNotApplicableException(Exception e) {
         super(e);

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

@@ -31,7 +31,7 @@ import java.util.stream.Stream;
  */
 public class Interpreter<T> extends DefaultASTVisitor<Object>
         implements ScopeObservable {
-    private static final int MAX_ITERATIONS = 5;
+    private static final int MAX_ITERATIONS = 10000;
 
     protected static Logger logger = LogManager.getLogger(Interpreter.class);
 
@@ -594,17 +594,21 @@ public class Interpreter<T> extends DefaultASTVisitor<Object>
         enterScope(repeatStatement);
         int counter = 0;
         boolean b = false;
-        do {
-            counter++;
-            State<T> prev = getCurrentState();
-            repeatStatement.getBody().accept(this);
-            State<T> end = getCurrentState();
-
-            Set<GoalNode<T>> prevNodes = new HashSet<>(prev.getGoals());
-            Set<GoalNode<T>> endNodes = new HashSet<>(end.getGoals());
-            b = prevNodes.equals(endNodes);
-            b = b && counter <= MAX_ITERATIONS;
-        } while (b);
+        try {
+            do {
+                counter++;
+                State<T> prev = getCurrentState();
+                repeatStatement.getBody().accept(this);
+                State<T> end = getCurrentState();
+
+                Set<GoalNode<T>> prevNodes = new HashSet<>(prev.getGoals());
+                Set<GoalNode<T>> endNodes = new HashSet<>(end.getGoals());
+                b = prevNodes.equals(endNodes);
+                b = b && counter <= MAX_ITERATIONS;
+            } while (b);
+        }catch (InterpreterRuntimeException e) {
+            logger.debug("Catched!", e);
+        }
         exitScope(repeatStatement);
         return null;
     }

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

@@ -2,11 +2,14 @@ package edu.kit.iti.formal.psdbg.gui;
 
 
 import de.uka.ilkd.key.util.KeYConstants;
+import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
 import javafx.application.Application;
 import javafx.application.Platform;
 import javafx.fxml.FXMLLoader;
 import javafx.scene.Parent;
 import javafx.scene.Scene;
+import javafx.scene.input.KeyCode;
+import javafx.scene.input.KeyCodeCombination;
 import javafx.stage.Stage;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
@@ -25,7 +28,9 @@ import java.util.Locale;
  */
 public class ProofScriptDebugger extends Application {
     public static final String NAME = "Proof Script Debugger";
+
     public static final String VERSION = "0.1";
+
     public static final String KEY_VERSION = KeYConstants.VERSION;
 
     private Logger logger = LogManager.getLogger("psdbg");
@@ -47,8 +52,42 @@ public class ProofScriptDebugger extends Application {
             FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.fxml"));
             //"/edu/kit/formal/psdb/gui/controller/DebuggerMain.fxml"));
             Parent root = fxmlLoader.load();
-            //DebuggerMain controller = fxmlLoader.<DebuggerMain>getController();
+            DebuggerMain controller = fxmlLoader.getController();
             Scene scene = new Scene(root);
+
+
+            scene.getAccelerators().put(
+                    new KeyCodeCombination(KeyCode.F1),
+                    () -> controller.showCommandHelp(null)
+            );
+
+            scene.getAccelerators().put(
+                    new KeyCodeCombination(KeyCode.F12),
+                    () -> controller.showWelcomeDock(null)
+            );
+
+            scene.getAccelerators().put(
+                    new KeyCodeCombination(KeyCode.F5),
+                    () -> controller.stepBack(null)
+            );
+
+            scene.getAccelerators().put(
+                    new KeyCodeCombination(KeyCode.F6),
+                    () -> controller.stepOver(null)
+            );
+
+
+            scene.getAccelerators().put(
+                    new KeyCodeCombination(KeyCode.F7),
+                    () -> controller.stepInto(null)
+            );
+
+            scene.getAccelerators().put(
+                    new KeyCodeCombination(KeyCode.F3),
+                    controller::executeStepwise
+            );
+
+
             primaryStage.setOnCloseRequest(event -> Platform.exit());
             scene.getStylesheets().addAll(
                     getClass().getResource("debugger-ui.css").toExternalForm(),

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

@@ -15,6 +15,8 @@ import javafx.beans.value.ChangeListener;
 import javafx.beans.value.ObservableValue;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableMap;
+import javafx.geometry.Point2D;
+import javafx.scene.Cursor;
 import org.antlr.v4.runtime.CharStream;
 import org.antlr.v4.runtime.CharStreams;
 import org.apache.commons.io.FileUtils;
@@ -295,10 +297,13 @@ public class ScriptController {
             logger.debug("Region for highlighting: {}", r);
 
             ScriptArea area = findEditor(node);
+            double scrollY = area.getEstimatedScrollY();
             area.getMarkedRegions().add(r);
 
             getDockNode(area).focus();
             area.requestFocus();
+            //area.scrollBy(new Point2D(0, scrollY));
+            area.selectRange(0, r.start, 0, r.stop);
 
             lastScriptArea = area;
             lastRegion = r;

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

-script agascript() {
+script SolveAgathaRiddle_1() {
     impRight;
     andLeft;
     notLeft;
@@ -18,9 +18,9 @@ script agascript() {
     exLeft;
     andLeft;
     eqSymm formula = `agatha = butler`;
+    auto;
 
     //nnf_imp2or on= `hates(agatha, w6) -> hates(butler, w6)`;
-
     //nnf_imp2or; -> wirft hier ScriptCommandNotApplicableException
     //wirft ansonsten immer java.lang.RuntimeException: de.uka.ilkd.key.macros.scripts.meta.ConversionException: Could not convert value hates(agatha, w6) -> hates(butler, w6) to type interface de.uka.ilkd.key.logic.Term
     //	at
@@ -28,22 +28,13 @@ script agascript() {
     //nnf_imp2or on = `hates(agatha, w6) -> hates(butler, w6)` formula=` \forall S w6; (hates(agatha, w6) -> hates(butler, w6))`;
 }
 
-script agascript2() {
+script SolveAgathaRiddle_2() {
     impRight;
     andLeft;
     notLeft;
-
     repeat { andLeft; }
-
     exLeft;
     andLeft;
     eqSymm formula = `agatha = butler`;
-
-    //nnf_imp2or on= `hates(agatha, w6) -> hates(butler, w6)`;
-
-    //nnf_imp2or; -> wirft hier ScriptCommandNotApplicableException
-    //wirft ansonsten immer java.lang.RuntimeException: de.uka.ilkd.key.macros.scripts.meta.ConversionException: Could not convert value hates(agatha, w6) -> hates(butler, w6) to type interface de.uka.ilkd.key.logic.Term
-    //	at
-    //nnf_imp2or formula= `hates(agatha, w6) -> hates(butler, w6)`;
-    //nnf_imp2or on = `hates(agatha, w6) -> hates(butler, w6)` formula=` \forall S w6; (hates(agatha, w6) -> hates(butler, w6))`;
+    auto;
 }
\ No newline at end of file