bug fix

src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java

@@ -158,6 +158,10 @@ public class DebuggerMainWindowController implements Initializable {
             scriptController.getDebugPositionHighlighter().highlight(newValue);
         });
 
+        imodel.highlightedJavaLinesProperty().addListener((observable, oldValue, newValue) -> {
+            javaArea.enableCurrentLineHighlightingProperty();
+        });
+
         Utils.addDebugListener(proofTreeController.currentGoalsProperty(), Utils::reprKeyDataList);
         Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty(), Utils::reprKeyData);
         Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty());
@@ -175,8 +179,14 @@ public class DebuggerMainWindowController implements Initializable {
         });*/
 
         chosenContract.addListener(o -> {
-            javaCode.set(Utils.getJavaCode(chosenContract.get()));
-
+            //javaCode.set(Utils.getJavaCode(chosenContract.get()));
+            try {
+                System.out.println(chosenContract.get().getHTMLText(getFacade().getService()));
+                String encoding = null; //encoding Plattform default
+                javaCode.set(FileUtils.readFileToString(javaFile.get(), encoding));
+            } catch (IOException e) {
+                e.printStackTrace();
+            }
             showCodeDock(null);
         });
 
@@ -186,12 +196,14 @@ public class DebuggerMainWindowController implements Initializable {
             public void changed(ObservableValue<? extends String> observable, String oldValue, String newValue) {
                 try {
                     javaArea.setText(newValue);
+                    javaArea.enableLineHighlightingProperty();
                 } catch (Exception e) {
                     LOGGER.catching(e);
                 }
             }
         });
 
+
     }
 
 
@@ -306,7 +318,7 @@ public class DebuggerMainWindowController implements Initializable {
 
     @FXML
     protected void loadKeYFile() {
-        File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "script");
+        File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps");
         openKeyFile(keyFile);
     }
 

src/main/java/edu/kit/formal/gui/controller/Events.java

 package edu.kit.formal.gui.controller;
 
 import com.google.common.eventbus.EventBus;
+import de.uka.ilkd.key.logic.PosInOccurrence;
 import de.uka.ilkd.key.rule.TacletApp;
 import edu.kit.formal.gui.controls.ScriptArea;
 import lombok.Data;
@@ -37,5 +38,6 @@ public class Events {
     @RequiredArgsConstructor
     public static class TacletApplicationEvent {
         private final TacletApp app;
+        private final PosInOccurrence pio;
     }
 }

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

@@ -6,6 +6,7 @@ import edu.kit.formal.interpreter.data.KeyData;
 import javafx.beans.Observable;
 import javafx.beans.property.ReadOnlyObjectProperty;
 import javafx.beans.property.SimpleObjectProperty;
+import javafx.collections.FXCollections;
 import javafx.fxml.FXML;
 import javafx.scene.Node;
 import javafx.scene.control.ListCell;
@@ -45,19 +46,26 @@ public class InspectionView extends BorderPane {
                     if (newValue != null && newValue.getData() != null) {
                         getSequentView().setNode(newValue.getData().getNode());
                         getSequentView().setGoal(newValue.getData().getGoal());
+
                         // TODO weigl: get marked lines of the program, and set it
-                        model.get().highlightedJavaLinesProperty().get()
-                                .clear();
+                        /*model.get().highlightedJavaLinesProperty().get()
+                                .clear();*/
+                        model.get().setHighlightedJavaLines(FXCollections.observableSet(newValue.getData().constructLinesSet()));
+
+                        System.out.println(newValue.getData().constructLinesSet());
 
                     }
                 });
 
         model.get().goalsProperty().bindBidirectional(goalView.itemsProperty());
+
+
         getGoalView().setCellFactory(GoalNodeListCell::new);
 
         Utils.addDebugListener(model.get().goalsProperty());
         Utils.addDebugListener(model.get().selectedGoalNodeToShowProperty());
         Utils.addDebugListener(model.get().currentInterpreterGoalProperty());
+        Utils.addDebugListener(model.get().highlightedJavaLinesProperty());
 
         /*TODO redefine CSS bases on selected mode
         mode.addListener(o -> {
@@ -71,6 +79,7 @@ public class InspectionView extends BorderPane {
          */
     }
 
+
     public SequentView getSequentView() {
         return sequentView;
     }

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

 package edu.kit.formal.gui.controls;
 
+import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
+import de.uka.ilkd.key.logic.SequentFormula;
+import edu.kit.formal.gui.controller.Events;
 import edu.kit.formal.gui.model.Breakpoint;
 import edu.kit.formal.gui.model.MainScriptIdentifier;
 import edu.kit.formal.proofscriptparser.Facade;
@@ -378,6 +381,7 @@ public class ScriptArea extends CodeArea {
 
     public void removeExecutionMarker() {
         setText(getTextWithoutMarker());
+        //Events.unregister(this);
     }
 
     private String getTextWithoutMarker() {
@@ -386,10 +390,33 @@ public class ScriptArea extends CodeArea {
 
     public void insertExecutionMarker(int pos) {
         LOGGER.debug("ScriptArea.insertExecutionMarker");
+        Events.register(this);
         String text = getText();
         setText(text.substring(0, pos) + EXECUTION_MARKER + text.substring(pos));
+
+
     }
 
+    @Subscribe
+    public void handle(Events.TacletApplicationEvent tap) {
+
+        String tapName = tap.getApp().taclet().displayName();
+
+        SequentFormula seqForm = tap.getPio().sequentFormula();
+
+        System.out.println(tap.getPio().sequentFormula());
+        //String on = tap.getApp().ifFormulaInstantiations().toString();
+        String text = getText();
+        System.out.println(text);
+        int posExecMarker = this.getExecutionMarkerPosition();
+        setText(text.substring(0, posExecMarker) + "\n" + tapName + " on=\"" + seqForm + "\";\n" + text.substring(posExecMarker + 1));
+        Events.unregister(this);
+        //this.getMainScript().getScriptArea().insertText(this.getExecutionMarkerPosition(), tapName+" "+on+ ";");
+
+    }
+
+
+
     public int getExecutionMarkerPosition() {
         return getText().lastIndexOf(EXECUTION_MARKER);
     }

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

@@ -130,7 +130,7 @@ public class SequentView extends CodeArea {
         clear();
         insertText(0, backend.getString());
         if (node.get().isClosed()) {
-            this.setBorder(new Border(new BorderStroke(Color.RED, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
+            this.setBorder(new Border(new BorderStroke(Color.GREEN, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
             this.getStyleClass().add("closed-sequent-view");
         }
     }

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

@@ -9,10 +9,7 @@ import de.uka.ilkd.key.pp.AbbrevMap;
 import de.uka.ilkd.key.pp.NotationInfo;
 import de.uka.ilkd.key.pp.PosInSequent;
 import de.uka.ilkd.key.proof.Goal;
-import de.uka.ilkd.key.rule.BuiltInRule;
-import de.uka.ilkd.key.rule.RuleSet;
-import de.uka.ilkd.key.rule.Taclet;
-import de.uka.ilkd.key.rule.TacletApp;
+import de.uka.ilkd.key.rule.*;
 import edu.kit.formal.gui.controller.DebuggerMainWindowController;
 import edu.kit.formal.gui.controller.Events;
 import edu.kit.formal.interpreter.KeYProofFacade;
@@ -134,8 +131,8 @@ public class TacletContextMenu extends ContextMenu {
      */
     private static ImmutableList<TacletApp> removeRewrites(
             ImmutableList<TacletApp> list) {
-        return list;
-        /*
+        // return list;
+
         ImmutableList<TacletApp> result = ImmutableSLList.<TacletApp>nil();
         Iterator<TacletApp> it = list.iterator();
 
@@ -145,7 +142,7 @@ public class TacletContextMenu extends ContextMenu {
             result = (taclet instanceof RewriteTaclet ? result
                     : result.prepend(tacletApp));
         }
-        return result;*/
+        return result;
     }
 
     /**
@@ -319,8 +316,8 @@ public class TacletContextMenu extends ContextMenu {
                 ((TacletMenuItem) event.getSource()).getTaclet(), goal,
                 pos.getPosInOccurrence());*/
 
-        System.out.println("event = [" + event + "]");
-        Events.fire(new Events.TacletApplicationEvent(event));
+        //System.out.println("event = [" + event + "]");
+        Events.fire(new Events.TacletApplicationEvent(event, pos.getPosInOccurrence()));
     }
 
     /**

src/main/java/edu/kit/formal/gui/model/InspectionModel.java

@@ -23,8 +23,8 @@ public class InspectionModel {
     private final ObjectProperty<GoalNode<KeyData>> currentInterpreterGoal = new SimpleObjectProperty<>(this, "currentInterpreterGoal");
     private final MapProperty<GoalNode, Color> colorofEachGoalNodeinListView = new SimpleMapProperty<>(FXCollections.observableHashMap());
     //private final StringProperty javaString = new SimpleStringProperty();
-    private final SetProperty<Integer> highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet());
-    private final BooleanProperty closable = new SimpleBooleanProperty();
+    private final SetProperty<Integer> highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet(), "highlightedJavaLines");
+    private final BooleanProperty closable = new SimpleBooleanProperty(this, "INspectionViewClosableProperty");
     private final BooleanProperty isInterpreterTab = new SimpleBooleanProperty();
     private ObjectProperty<Mode> mode = new SimpleObjectProperty<>();
 

src/main/java/edu/kit/formal/interpreter/data/KeyData.java

 package edu.kit.formal.interpreter.data;
 
 import de.uka.ilkd.key.control.KeYEnvironment;
+import de.uka.ilkd.key.java.SourceElement;
 import de.uka.ilkd.key.proof.Goal;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import lombok.*;
 
+import java.util.HashSet;
+import java.util.Set;
 import java.util.function.Function;
 
 /**
@@ -20,6 +23,7 @@ import java.util.function.Function;
 @RequiredArgsConstructor
 public class KeyData {
     private static final String SEPARATOR = " // ";
+    private static final String RANGE_SEPARATOR = " -- ";
     private final KeYEnvironment env;
     private final Proof proof;
     private Node node;
@@ -38,6 +42,7 @@ public class KeyData {
         this.proof = data.proof;
         this.goal = node;
         this.node = goal.node();
+
     }
 
     public KeyData(Goal g, KeYEnvironment environment, Proof proof) {
@@ -124,13 +129,21 @@ public class KeyData {
 
     /**
      * Get lines of active statement
-     * @return line of active satetment in orginal file (-1 if rewritten by KeY or not applicable)
+     * @return line of active satetment in original file (-1 if rewritten by KeY or not applicable)
      */
     public String getProgramLinesLabel() {
         if (programLinesLabel == null) {
-            programLinesLabel = constructLabel(n ->
-                    Integer.toString(n.getNodeInfo().getActiveStatement().getPositionInfo().getStartPosition().getLine())
-            );
+            programLinesLabel = constructLabel(n -> {
+                int startPos = n.getNodeInfo().getActiveStatement().getPositionInfo().getStartPosition().getLine();
+                int endPos = n.getNodeInfo().getActiveStatement().getPositionInfo().getEndPosition().getLine();
+                if (startPos == endPos) {
+                    return Integer.toString(startPos);
+                } else {
+                    String start = Integer.toString(startPos);
+                    String end = Integer.toString(endPos);
+                    return start + RANGE_SEPARATOR + end;
+                }
+            });
         }
         return programLinesLabel;
     }
@@ -157,4 +170,32 @@ public class KeyData {
         return node;
         //return getGoal().node();
     }
+
+    public Set<Integer> constructLinesSet() {
+        Set<Integer> set = new HashSet<>();
+
+        Node cur = getNode();
+        do {
+
+            SourceElement activeStatement = cur.getNodeInfo().getActiveStatement();
+            if (activeStatement != null) {
+                int startPos = activeStatement.getPositionInfo().getStartPosition().getLine();
+                int endPos = activeStatement.getPositionInfo().getEndPosition().getLine();
+                if (startPos != -1) {
+                    if (startPos == endPos) {
+                        set.add(startPos);
+                    } else {
+                        set.add(startPos);
+                        set.add(endPos);
+                    }
+                }
+            }
+            cur = cur.parent();
+
+        } while (cur != null);
+        return set;
+    }
+
+
+
 }