Merge remote-tracking branch 'origin/master'

README.md

@@ -27,5 +27,12 @@ debugging to the analysis of failed proof attempts.
 # About this Repository
 
 The latest build as jar file can be downloaded here. 
-Plese note that some funtionlities may not work in this jar as it is the build 
-of the development version of PSDBG.
\ No newline at end of file
+Please note that some funtionlities may not work in this jar as it is the build 
+of the development version of PSDBG.
+
+# Usage Notes
+
+Terms in KPS are enquoted using backticks [`]. Entering these requires a 
+keyboard layout with the option "no dead keys".
+If this is not possible the terms can be entered by using the shortcut Ctrl+E 
+which adds a pair of backticks to the cursor position.
\ No newline at end of file

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

@@ -5,6 +5,7 @@ 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.parser.ast.CallStatement;
+import edu.kit.iti.formal.psdbg.storage.KeyPersistentFacade;
 import javafx.application.Platform;
 import javafx.scene.control.Alert;
 import javafx.scene.control.ButtonType;
@@ -73,6 +74,7 @@ public class SaveCommand implements CommandHandler<KeyData> {
 
             if(execute.get())
                 interpreter.getSelectedNode().getData().getProof().saveToFile(newFile);
+            //KeyPersistentFacade.write();
             //TODO Call to key persistend facade
         } catch (IOException e) {
             e.printStackTrace();

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

@@ -66,6 +66,7 @@ import org.reactfx.util.Timer;
 
 import javax.annotation.Nullable;
 import javax.swing.*;
+import java.awt.im.InputContext;
 import java.io.File;
 import java.io.FileWriter;
 import java.io.IOException;
@@ -256,6 +257,7 @@ public class DebuggerMain implements Initializable {
         Events.register(this);
         // model.setDebugMode(false);
         scriptController = new ScriptController(dockStation);
+
         interactiveModeController = new InteractiveModeController(scriptController);
         btnInteractiveMode.setSelected(false);
         inspectionViewsController = new InspectionViewsController(dockStation);
@@ -277,6 +279,7 @@ public class DebuggerMain implements Initializable {
             ImmutableList<Goal> openGoals = p.getSubtreeGoals(p.root());
             KeyData kd = new KeyData(openGoals.get(0), env, p);
             scriptController.getAutoCompleter().getArgumentCompleter().setDefaultKeyData(kd);
+
         };
         getFacade().environmentProperty().addListener(invalidationListener);
         getFacade().proofProperty().addListener(invalidationListener);
@@ -346,7 +349,9 @@ public class DebuggerMain implements Initializable {
         BooleanBinding disableStepping = FACADE.loadingProperty().
                 or(FACADE.proofProperty().isNull()).
                 or(model.interpreterStateProperty().isNotEqualTo(InterpreterThreadState.WAIT));
-
+        FACADE.loadingProperty().addListener((observable, oldValue, newValue) -> {
+            scriptController.disablePropertyForAreasProperty().set(newValue);
+        });
       /*  model.statePointerProperty().addListener((observable, oldValue, newValue) -> {
 
             //set all steppings -> remove binding
@@ -676,8 +681,8 @@ public class DebuggerMain implements Initializable {
 
     private void onInterpreterError(DebuggerFramework<KeyData> keyDataDebuggerFramework, Throwable throwable) {
         Platform.runLater(() -> {
-            Utils.showExceptionDialog("Error during Execution", "Error during Script Execution",
-                    "Here should be some really good text...\nNothing will be the same. Everything broken.",
+            Utils.showExceptionDialog("An error has occurred during execution.", "Error during Script Execution",
+                    "Please reload the problem to get a consistent proof state.",
                     throwable
             );
         });

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

@@ -103,9 +103,15 @@ public class FileReloadingService extends TimerTask {
                 try {
                     String content = FileUtils.readFileToString(child.toFile(), Charset.defaultCharset());
                     CONSOLE_LOGGER.info("Auto-reload {}", child);
-                    Platform.runLater(() -> callbacks.get(child).fileChanged(content));
+                    Platform.runLater(() -> {
+                            if(callbacks.get(child)!= null) {
+                                callbacks.get(child).fileChanged(content);
+                            }
+                    });
                 } catch (IOException e) {
                     CONSOLE_LOGGER.catching(e);
+                } catch (NullPointerException npe){
+                    CONSOLE_LOGGER.catching(npe);
                 }
             }
             boolean valid = key.reset();

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

@@ -34,6 +34,7 @@ import javafx.scene.Node;
 import javafx.scene.Scene;
 import javafx.scene.control.*;
 import javafx.scene.input.*;
+import static javafx.scene.input.KeyCombination.CONTROL_ANY;
 import javafx.scene.layout.*;
 import javafx.scene.paint.Color;
 import javafx.scene.paint.Paint;
@@ -89,6 +90,7 @@ public class ScriptArea extends BorderPane {
 
     public static final FileReloadingService FILE_RELOADING_SERVICE = new FileReloadingService();
 
+
     /**
      * Underlying filepath, should not be null
      */
@@ -141,6 +143,7 @@ public class ScriptArea extends BorderPane {
 
     private void init() {
         codeArea.setAutoScrollOnDragDesired(false);
+
         InputMap<KeyEvent> inputMap = sequence(
                 process(EventPattern.keyPressed(),
                         (e) -> {
@@ -148,6 +151,8 @@ public class ScriptArea extends BorderPane {
                             inlineToolbar.hide();
                             return PROCEED;
                         }),
+                consume(keyPressed(new KeyCodeCombination(KeyCode.E, KeyCombination.CONTROL_DOWN))
+                       , (e) -> addBackticks()),
                 consumeWhen(keyPressed(KeyCode.ENTER), autoCompletion::isVisible,
                         e -> autoCompletion.complete()),
                 consume(keyPressed(KeyCode.ENTER, SHORTCUT_DOWN),
@@ -241,6 +246,7 @@ public class ScriptArea extends BorderPane {
             //this.moveTo(characterPosition, NavigationActions.SelectionPolicy.CLEAR);
         });
 
+        
         mainScript.addListener((observable) -> updateMainScriptMarker());
         filePath.addListener((p, o, n) -> {
             if (o != null)
@@ -357,6 +363,14 @@ public class ScriptArea extends BorderPane {
     }
 
 
+    private void addBackticks(){
+        int pos = codeArea.getCaretPosition();
+        insertText(pos, "``");
+        codeArea.displaceCaret(pos+1);
+
+
+
+    }
     private void highlightProblems() {
         LinterStrategy ls = LinterStrategy.getDefaultLinter();
         try {
@@ -412,8 +426,11 @@ public class ScriptArea extends BorderPane {
             if (p.includeTextPosition(chIdx)) {
                 Label lbl = new Label(p.getMessage());
                 lbl.getStyleClass().addAll("problem-popup-label",
-                        "problem-popup-label-" + p.getIssue().getRulename(),
-                        "problem-popup-label-" + p.getIssue().getSeverity());
+                        "problem-popup-label-" + p.getIssue(),
+                                //.getRulename(),
+                        "problem-popup-label-" + p.getIssue()
+                                //.getSeverity()
+                        );
                 box.getChildren().add(lbl);
             }
         }

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

@@ -15,10 +15,7 @@ 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 javafx.beans.property.ListProperty;
-import javafx.beans.property.ObjectProperty;
-import javafx.beans.property.SimpleListProperty;
-import javafx.beans.property.SimpleObjectProperty;
+import javafx.beans.property.*;
 import javafx.beans.value.ChangeListener;
 import javafx.beans.value.ObservableValue;
 import javafx.collections.FXCollections;
@@ -52,6 +49,23 @@ public class ScriptController {
 
     private final DockPane parent;
 
+    public boolean isDisablePropertyForAreas() {
+        return disablePropertyForAreas.get();
+    }
+
+    public SimpleBooleanProperty disablePropertyForAreasProperty() {
+        return disablePropertyForAreas;
+    }
+
+    public void setDisablePropertyForAreas(boolean disablePropertyForAreas) {
+        this.disablePropertyForAreas.set(disablePropertyForAreas);
+    }
+
+    /**
+     * Property to globally disable or enable scriptareas
+     */
+    private SimpleBooleanProperty disablePropertyForAreas = new SimpleBooleanProperty(true);
+
     private final ObservableMap<ScriptArea, DockNode> openScripts = FXCollections.observableMap(new HashMap<>());
     private final ListProperty<SavePoint> mainScriptSavePoints
             = new SimpleListProperty<>(FXCollections.observableArrayList());
@@ -191,7 +205,9 @@ public class ScriptController {
             area.setAutoCompletionController(getAutoCompleter());
             area.mainScriptProperty().bindBidirectional(mainScript);
             area.setFilePath(filePath);
+            area.disableProperty().bindBidirectional(this.disablePropertyForAreas);
             DockNode dockNode = createDockNode(area);
+
             openScripts.put(area, dockNode);
 
             if (filePath.exists()) {