Execution Marker

src/main/antlr4/edu/kit/formal/proofscriptparser/ScriptLanguage.g4

@@ -178,6 +178,8 @@ IMP : '==>' ;
 EQUIV : '<=>' ;
 NOT: 'not';
 
+EXE_MARKER: '\u2316' -> channel(HIDDEN);
+
 DIGITS : DIGIT+ ;
 fragment DIGIT : [0-9] ;
-ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' )* ;
\ No newline at end of file
+ID : [a-zA-Z] ([_a-zA-Z0-9] | '.' | '\\' )* ;

src/main/java/edu/kit/formal/gui/controls/ScriptArea.java

@@ -48,6 +48,7 @@ import org.reactfx.value.Val;
 import java.io.File;
 import java.time.Duration;
 import java.util.*;
+import java.util.function.Consumer;
 import java.util.function.IntFunction;
 
 /**
@@ -56,11 +57,13 @@ import java.util.function.IntFunction;
  * It displays the script code and allows highlighting of lines and setting of breakpoints
  */
 public class ScriptArea extends CodeArea {
-    private static final Logger LOGGER = LogManager.getLogger(ScriptArea.class);
+    public static final Logger LOGGER = LogManager.getLogger(ScriptArea.class);
+    public static final String EXECUTION_MARKER = "\u2316";
+
     /**
      * Underlying filepath, should not be null
      */
-    private final ObjectProperty<File> filePath = new SimpleObjectProperty<>(new File(Utils.getRandomName()));
+    private final ObjectProperty<File> filePath = new SimpleObjectProperty<>(this, "filePath", new File(Utils.getRandomName()));
 
     /**
      * If true, the content was changed since last save.
@@ -71,6 +74,7 @@ public class ScriptArea extends CodeArea {
      * CSS classes for regions, used for "manually" highlightning. e.g. debugging marker
      */
     private final SetProperty<RegionStyle> markedRegions = new SimpleSetProperty<>(FXCollections.observableSet());
+
     /**
      * set by {@link ScriptController}
      */
@@ -82,6 +86,9 @@ public class ScriptArea extends CodeArea {
     private SimpleObjectProperty<CharacterHit> currentMouseOver = new SimpleObjectProperty<>();
     private ScriptAreaContextMenu contextMenu = new ScriptAreaContextMenu();
 
+    private Consumer<Token> onPostMortem = token -> {
+    };
+    private int getTextWithoutMarker;
 
     public ScriptArea() {
         init();
@@ -96,14 +103,17 @@ public class ScriptArea extends CodeArea {
         getStyleClass().add("script-area");
         installPopup();
 
-        setOnMouseClicked(this::showContextMenu);
+        // setOnMouseClicked(this::showContextMenu);
+        setContextMenu(contextMenu);
 
         textProperty().addListener((prop, oldValue, newValue) -> {
             dirty.set(true);
             updateMainScriptMarker();
             updateHighlight();
             highlightProblems();
+            highlightNonExecutionArea();
         });
+
         markedRegions.addListener((InvalidationListener) o -> updateHighlight());
 
                /* .successionEnds(Duration.ofMillis(100))
@@ -118,7 +128,6 @@ public class ScriptArea extends CodeArea {
                     }
                 }).subscribe(s -> setStyleSpans(0, s));*/
 
-
         this.addEventHandler(MouseEvent.MOUSE_PRESSED, (MouseEvent e) -> {
             CharacterHit hit = this.hit(e.getX(), e.getY());
             currentMouseOver.set(this.hit(e.getX(), e.getY()));
@@ -131,6 +140,16 @@ public class ScriptArea extends CodeArea {
         mainScript.addListener((observable) -> updateMainScriptMarker());
     }
 
+    private void highlightNonExecutionArea() {
+        if (hasExecutionMarker()) {
+            setStyle(0, getExecutionMarkerPosition(), Collections.singleton("NON_EXE_AREA"));
+        }
+    }
+
+    private boolean hasExecutionMarker() {
+        return getText().contains(EXECUTION_MARKER);
+    }
+
     public void showContextMenu(MouseEvent mouseEvent) {
         if (contextMenu.isShowing())
             contextMenu.hide();
@@ -160,7 +179,8 @@ public class ScriptArea extends CodeArea {
     private void updateMainScriptMarker() {
         try {
             MainScriptIdentifier ms = mainScript.get();
-            System.out.println("ScriptArea.updateMainScriptMarker");
+            LOGGER.debug("ScriptArea.updateMainScriptMarker");
+
             if (ms != null && filePath.get().getAbsolutePath().equals(ms.getSourceName())) {
                 System.out.println(ms);
                 CharStream stream = CharStreams.fromString(getText(), filePath.get().getAbsolutePath());
@@ -239,6 +259,7 @@ public class ScriptArea extends CodeArea {
     }
 
     public void setText(String text) {
+        clear();
         insertText(0, text);
     }
 
@@ -306,6 +327,57 @@ public class ScriptArea extends CodeArea {
         d.show((Node) event.getTarget(), event.getScreenX(), event.getScreenY());
     }
 
+    public Consumer<Token> getOnPostMortem() {
+        return onPostMortem;
+    }
+
+    public void setOnPostMortem(Consumer<Token> onPostMortem) {
+        this.onPostMortem = onPostMortem;
+    }
+
+    public ObservableSet<RegionStyle> getMarkedRegions() {
+        return markedRegions.get();
+    }
+
+    public void setMarkedRegions(ObservableSet<RegionStyle> markedRegions) {
+        this.markedRegions.set(markedRegions);
+    }
+
+    public SetProperty<RegionStyle> markedRegionsProperty() {
+        return markedRegions;
+    }
+
+    public boolean isDirty() {
+        return dirty.get();
+    }
+
+    public void setDirty(boolean dirty) {
+        this.dirty.set(dirty);
+    }
+
+    public BooleanProperty dirtyProperty() {
+        return dirty;
+    }
+
+
+    public void removeExecutionMarker() {
+        setText(getTextWithoutMarker());
+    }
+
+    private String getTextWithoutMarker() {
+        return getText().replace("" + EXECUTION_MARKER, "");
+    }
+
+    public void insertExecutionMarker(int pos) {
+        LOGGER.debug("ScriptArea.insertExecutionMarker");
+        String text = getText();
+        setText(text.substring(0, pos) + EXECUTION_MARKER + text.substring(pos));
+    }
+
+    public int getExecutionMarkerPosition() {
+        return getText().lastIndexOf(EXECUTION_MARKER);
+    }
+
     private static class GutterView extends HBox {
         private final SimpleObjectProperty<GutterAnnotation> annotation = new SimpleObjectProperty<>();
 
@@ -463,6 +535,13 @@ public class ScriptArea extends CodeArea {
         }
     }
 
+    @RequiredArgsConstructor
+    @Data
+    public static class RegionStyle {
+        public final int start, stop;
+        public final String clazzName;
+    }
+
     public class GutterFactory implements IntFunction<Node> {
         private final Background defaultBackground =
                 new Background(new BackgroundFill(Color.web("#ddd"), null, null));
@@ -553,7 +632,9 @@ public class ScriptArea extends CodeArea {
         public void showPostMortem(ActionEvent event) {
             LOGGER.debug("ScriptAreaContextMenu.showPostMortem " + event);
 
-
+            CharacterHit pos = currentMouseOver.get();
+            Token node = Utils.findToken(getText(), pos.getInsertionIndex());
+            onPostMortem.accept(node);
 
             //TODO forward to ProofTreeController, it jumps to the node and this should be done via the callbacks.
 
@@ -564,36 +645,12 @@ public class ScriptArea extends CodeArea {
                 area.highlightStmt(lineNumber, "line-highlight-postmortem");
             }*/
         }
-    }
-
-    public ObservableSet<RegionStyle> getMarkedRegions() {
-        return markedRegions.get();
-    }
 
-    public SetProperty<RegionStyle> markedRegionsProperty() {
-        return markedRegions;
-    }
-
-    public void setMarkedRegions(ObservableSet<RegionStyle> markedRegions) {
-        this.markedRegions.set(markedRegions);
-    }
-
-    public boolean isDirty() {
-        return dirty.get();
-    }
-
-    public BooleanProperty dirtyProperty() {
-        return dirty;
-    }
-
-    public void setDirty(boolean dirty) {
-        this.dirty.set(dirty);
-    }
-
-    @RequiredArgsConstructor
-    @Data
-    public static class RegionStyle {
-        public final int start, stop;
-        public final String clazzName;
+        public void setExecutionMarker(ActionEvent event) {
+            LOGGER.debug("ScriptAreaContextMenu.setExecutionMarker");
+            int pos = getCaretPosition();
+            removeExecutionMarker();
+            insertExecutionMarker(pos);
+        }
     }
 }

src/main/java/edu/kit/formal/gui/controls/Utils.java

@@ -3,6 +3,7 @@ package edu.kit.formal.gui.controls;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
 import de.uka.ilkd.key.pp.ProgramPrinter;
 import de.uka.ilkd.key.speclang.Contract;
+import edu.kit.formal.proofscriptparser.ScriptLanguageLexer;
 import javafx.beans.property.Property;
 import javafx.beans.value.ChangeListener;
 import javafx.beans.value.ObservableValue;
@@ -12,6 +13,8 @@ import javafx.scene.control.Label;
 import javafx.scene.control.TextArea;
 import javafx.scene.layout.GridPane;
 import javafx.scene.layout.Priority;
+import org.antlr.v4.runtime.CharStreams;
+import org.antlr.v4.runtime.Token;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 
@@ -192,4 +195,18 @@ public class Utils {
         o.addListener((ChangeListener<Object>) (observable, oldValue, newValue) ->
                 logger.debug("Observable {} changed from {} to {}", id, oldValue, newValue));
     }
+
+    public static Token findToken(String text, int insertionIndex) {
+        ScriptLanguageLexer lexer = new ScriptLanguageLexer(CharStreams.fromString(text));
+        for (Token t : lexer.getAllTokens()) {
+            if (t.getType() == ScriptLanguageLexer.WS
+                    || t.getType() == ScriptLanguageLexer.MULTI_LINE_COMMENT
+                    || t.getType() == ScriptLanguageLexer.SINGLE_LINE_COMMENT)
+                continue;
+
+            if (t.getStopIndex() >= insertionIndex)
+                return t;
+        }
+        return null;
+    }
 }

src/main/resources/edu/kit/formal/gui/controls/ScriptAreaContextMenu.fxml

@@ -2,12 +2,15 @@
 
 <?import edu.kit.formal.gui.controls.*?>
 <?import javafx.scene.control.MenuItem?>
+<?import javafx.scene.control.SeparatorMenuItem?>
 <fx:root type="edu.kit.formal.gui.controls.ScriptArea.ScriptAreaContextMenu"
          xmlns="http://javafx.com/javafx"
          xmlns:fx="http://javafx.com/fxml" >
 <items>
-    <MenuItem text="show post mortem" onAction="#showPostMortem"/>
-    <MenuItem text="Set main script" onAction="#setMainScript"/>
+    <MenuItem text="Show post mortem" onAction="#showPostMortem"/>
+    <SeparatorMenuItem/>
+    <MenuItem text="Set Main Script" onAction="#setMainScript"/>
+    <MenuItem text="Set Execution Marker" onAction="#setExecutionMarker" accelerator="Ctrl+m"/>
 </items>
 
 </fx:root>

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

@@ -35,6 +35,21 @@
 
   }
 
+
+  .EXE_MARKER {
+    -fx-fill: @violet;
+    -fx-border-color: red;
+    -fx-font-size: 120%;
+    -fx-font-weight: bold;
+  }
+
+  .NON_EXE_AREA {
+    -rtfx-background: @cyan;
+    -rtfx-underline-cap: butt;
+    -rtfx-underline-color: @cyan;
+    -rtfx-underline-width: 1px;
+  }
+
   // Structures
   .FOREACH, .CASES, .CASE, .DEFAULT
   .THEONLY, .SCRIPT, .USING, .REPEAT {