working on KeyData.java

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

 package edu.kit.formal.gui.controller;
 
+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.proof.init.ProofInputException;
@@ -18,6 +19,7 @@ import javafx.beans.property.*;
 import javafx.beans.value.ChangeListener;
 import javafx.beans.value.ObservableBooleanValue;
 import javafx.beans.value.ObservableValue;
+import javafx.collections.FXCollections;
 import javafx.concurrent.Service;
 import javafx.concurrent.Task;
 import javafx.event.ActionEvent;
@@ -51,12 +53,12 @@ import java.util.concurrent.Executors;
  * @author Alexander Weigl
  */
 public class DebuggerMainWindowController implements Initializable {
+    public static final KeYProofFacade FACADE = new KeYProofFacade();
     protected static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class);
+    public final ContractLoaderService contractLoaderService = new ContractLoaderService();
     private final ProofTreeController proofTreeController = new ProofTreeController();
     private final InspectionViewsController inspectionViewsController = new InspectionViewsController();
     private final ExecutorService executorService = Executors.newFixedThreadPool(2);
-    public static final KeYProofFacade FACADE = new KeYProofFacade();
-    public final ContractLoaderService contractLoaderService = new ContractLoaderService();
     /**
      * Property: current loaded javaFile
      */
@@ -70,8 +72,10 @@ public class DebuggerMainWindowController implements Initializable {
      */
     private final ObjectProperty<Contract> chosenContract = new SimpleObjectProperty<>(this, "chosenContract");
     private ScriptController scriptController;
+
     @FXML
     private DebuggerStatusBar statusBar;
+
     @FXML
     private DockPane dockStation;
     private JavaArea javaArea = new JavaArea();
@@ -107,6 +111,8 @@ public class DebuggerMainWindowController implements Initializable {
 
     @Override
     public void initialize(URL location, ResourceBundle resources) {
+        Events.register(this);
+
         setDebugMode(false);
         scriptController = new ScriptController(dockStation);
 
@@ -115,12 +121,14 @@ public class DebuggerMainWindowController implements Initializable {
         registerToolbarToStatusBar();
         marriageProofTreeControllerWithActiveInspectionView();
         //statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
-
+        marriageJavaCode();
 
         //Debugging
         Utils.addDebugListener(javaCode);
         Utils.addDebugListener(executeNotPossible, "executeNotPossible");
 
+        scriptController.mainScriptProperty().bindBidirectional(statusBar.mainScriptIdentifierProperty());
+
     }
 
     /**
@@ -133,20 +141,29 @@ public class DebuggerMainWindowController implements Initializable {
         proofTreeController.currentGoalsProperty().addListener((o, old, fresh) -> {
             if (fresh != null) {
                 imodel.setGoals(fresh);
+            } else {
+                // no goals, set an empty list
+                imodel.setGoals(FXCollections.observableArrayList());
             }
         });
 
         proofTreeController.currentSelectedGoalProperty().addListener((observable, oldValue, newValue) -> {
-            if (newValue != null) {
-                imodel.setCurrentInterpreterGoal(newValue);
-            }
+            imodel.setCurrentInterpreterGoal(newValue);
+            //also update the selected to be shown
+            imodel.setSelectedGoalNodeToShow(newValue);
         });
 
         proofTreeController.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> {
             scriptController.getDebugPositionHighlighter().highlight(newValue);
         });
 
-        javaFileProperty().addListener((observable, oldValue, newValue) -> {
+        Utils.addDebugListener(proofTreeController.currentGoalsProperty(), Utils::reprKeyDataList);
+        Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty(), Utils::reprKeyData);
+        Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty());
+    }
+
+    public void marriageJavaCode() {
+        /*javaFileProperty().addListener((observable, oldValue, newValue) -> {
             showCodeDock(null);
             try {
                 String code = FileUtils.readFileToString(newValue, Charset.defaultCharset());
@@ -154,8 +171,14 @@ public class DebuggerMainWindowController implements Initializable {
             } catch (IOException e) {
                 e.printStackTrace();
             }
+        });*/
+
+        chosenContract.addListener(o -> {
+            javaCode.set(Utils.getJavaCode(chosenContract.get()));
+            showCodeDock(null);
         });
 
+
         javaCode.addListener(new ChangeListener<String>() {
             @Override
             public void changed(ObservableValue<? extends String> observable, String oldValue, String newValue) {
@@ -166,11 +189,10 @@ public class DebuggerMainWindowController implements Initializable {
                 }
             }
         });
-        Utils.addDebugListener(proofTreeController.currentGoalsProperty());
-        Utils.addDebugListener(proofTreeController.currentSelectedGoalProperty());
-        Utils.addDebugListener(proofTreeController.currentHighlightNodeProperty());
+
     }
 
+
     /**
      * If the mouse moves other toolbar button, the help text should display in the status bar
      */

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

 package edu.kit.formal.gui.controller;
 
 import com.google.common.eventbus.EventBus;
+import edu.kit.formal.gui.controls.ScriptArea;
+import lombok.Data;
 
 /**
  * See http://codingjunkie.net/guava-eventbus/ for an introduction.
@@ -10,11 +12,24 @@ import com.google.common.eventbus.EventBus;
 public class Events {
     public static final EventBus GLOBAL_EVENT_BUS = new EventBus();
 
-    public void register(Object object) {
+    public static void register(Object object) {
         GLOBAL_EVENT_BUS.register(object);
     }
 
-    public void unregister(Object object) {
+    public static void unregister(Object object) {
         GLOBAL_EVENT_BUS.unregister(object);
     }
+
+    public static void fire(Object focusScriptArea) {
+        GLOBAL_EVENT_BUS.post(focusScriptArea);
+    }
+
+    @Data
+    public static class FocusScriptArea {
+        private final ScriptArea scriptArea;
+
+        public FocusScriptArea(ScriptArea area) {
+            this.scriptArea = area;
+        }
+    }
 }

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

@@ -89,7 +89,7 @@ public class PuppetMaster {
      * Publish state is called after the interpreter or debugger thread terminated. The resulting goals are set in the root model
      */
     public void publishState() {
-        System.out.println("PuppetMaster.publishState");
+        //("PuppetMaster.publishState");
         //puppet is null if successful interpreter state and publish state
         if (puppet != null) {
 

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

@@ -2,10 +2,9 @@ package edu.kit.formal.gui.controls;
 
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
-import javafx.beans.property.ListProperty;
-import javafx.beans.property.SimpleListProperty;
-import javafx.beans.property.SimpleObjectProperty;
-import javafx.beans.property.SimpleStringProperty;
+import edu.kit.formal.gui.controller.Events;
+import edu.kit.formal.gui.model.MainScriptIdentifier;
+import javafx.beans.property.*;
 import javafx.beans.value.ObservableStringValue;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableList;
@@ -33,22 +32,23 @@ import java.util.LinkedList;
  */
 public class DebuggerStatusBar extends StatusBar {
     private static final Logger LOGGER = LogManager.getLogger(DebuggerStatusBar.class);
-
+    private final Appender loggerHandler = createAppender();
+    private final ContextMenu contextMenu = createContextMenu();
+    private ObjectProperty<MainScriptIdentifier> mainScriptIdentifier = new SimpleObjectProperty<>();
     private Label lblCurrentNodes = new Label("#nodes: %s");
+    private Label lblMainscript = new Label();
     private ProgressIndicator progressIndicator = new ProgressIndicator();
     private LogCatchHandlerFX logCatchHandler = new LogCatchHandlerFX();
+    private final Dialog<Void> loggerDialog = createDialog();
     private EventHandler<MouseEvent> toolTipHandler = event -> {
         publishMessage(((Control) event.getTarget()).getTooltip().getText());
     };
 
-
-    private final ContextMenu contextMenu = createContextMenu();
-    private final Dialog<Void> loggerDialog = createDialog();
-
     public DebuggerStatusBar() {
         listenOnField("psdbg");
 
         getRightItems().addAll(
+                lblMainscript,
                 lblCurrentNodes,
                 progressIndicator
         );
@@ -60,9 +60,32 @@ public class DebuggerStatusBar extends StatusBar {
         });
 
 
-    }
+        mainScriptIdentifier.addListener((ov, o, n) -> {
+            if (n != null) {
+                lblMainscript.setText("Main Script: " +
+                        n.getScriptArea().getFilePath().getName() +
+                        (n.getScriptName() != null
+                                ? '\\' + n.getScriptName()
+                                : " @ " + n.getLineNumber()));
+                lblMainscript.setStyle("-fx-background-color: greenyellow;-fx-padding: 5pt;");
+            } else {
+                lblMainscript.setStyle("-fx-background-color: orangered;-fx-padding: 5pt;");
+                lblMainscript.setText("No main script selected");
+            }
+        });
 
-    private final Appender loggerHandler = createAppender();
+        lblMainscript.setStyle("-fx-background-color: orangered;-fx-padding: 5pt;");
+        lblMainscript.setText("No main script selected");
+
+        lblMainscript.setOnMouseClicked(event -> {
+            if (event.getClickCount() == 2) {
+                event.consume();
+                ScriptArea area = mainScriptIdentifier.get().getScriptArea();
+                Events.fire(new Events.FocusScriptArea(area));
+            }
+        });
+
+    }
 
     private Appender createAppender() {
         PatternLayout layout = PatternLayout.createDefaultLayout();
@@ -117,6 +140,18 @@ public class DebuggerStatusBar extends StatusBar {
         return cm;
     }
 
+    public MainScriptIdentifier getMainScriptIdentifier() {
+        return mainScriptIdentifier.get();
+    }
+
+    public void setMainScriptIdentifier(MainScriptIdentifier mainScriptIdentifier) {
+        this.mainScriptIdentifier.set(mainScriptIdentifier);
+    }
+
+    public ObjectProperty<MainScriptIdentifier> mainScriptIdentifierProperty() {
+        return mainScriptIdentifier;
+    }
+
     private void showLog(ActionEvent actionEvent) {
         loggerDialog.show();
     }
@@ -192,14 +227,14 @@ public class DebuggerStatusBar extends StatusBar {
             return records.get();
         }
 
-        public ListProperty<LogEvent> recordsProperty() {
-            return records;
-        }
-
         public void setRecords(ObservableList<LogEvent> records) {
             this.records.set(records);
         }
 
+        public ListProperty<LogEvent> recordsProperty() {
+            return records;
+        }
+
         public int getMaxRecords() {
             return maxRecords;
         }

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

@@ -35,15 +35,19 @@ public class InspectionView extends BorderPane {
     public InspectionView() {
         Utils.createWithFXML(this);
 
-        model.get().selectedGoalNodeToShowProperty().bind(
-                goalView.getSelectionModel().selectedItemProperty()
-        );
+        model.get().selectedGoalNodeToShowProperty().addListener((o, a, b) -> {
+            goalView.getSelectionModel().select(b);
+        });
+        goalView.getSelectionModel().selectedItemProperty().addListener((o, a, b) -> {
+            model.get().setSelectedGoalNodeToShow(b);
+        });
 
         model.get().selectedGoalNodeToShowProperty().addListener(
                 (observable, oldValue, newValue) -> {
                     goalView.getSelectionModel().select(newValue);
                     if (newValue != null && newValue.getData() != null) {
-                        getSequentView().setNode(newValue.getData().getGoal());
+                        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();
@@ -83,6 +87,14 @@ public class InspectionView extends BorderPane {
         goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
     }
 
+    public InspectionModel getModel() {
+        return model.get();
+    }
+
+    public ReadOnlyObjectProperty<InspectionModel> modelProperty() {
+        return model;
+    }
+
     /**
      * Cells for GoalView
      */
@@ -106,12 +118,4 @@ public class InspectionView extends BorderPane {
             setText(text);
         }
     }
-
-    public InspectionModel getModel() {
-        return model.get();
-    }
-
-    public ReadOnlyObjectProperty<InspectionModel> modelProperty() {
-        return model;
-    }
 }

src/main/java/edu/kit/formal/gui/controls/ScriptController.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 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;
@@ -21,6 +23,7 @@ import org.apache.logging.log4j.Logger;
 import org.dockfx.DockNode;
 import org.dockfx.DockPane;
 import org.dockfx.DockPos;
+import sun.reflect.generics.reflectiveObjects.NotImplementedException;
 
 import java.io.File;
 import java.io.IOException;
@@ -44,6 +47,13 @@ public class ScriptController {
 
     public ScriptController(DockPane parent) {
         this.parent = parent;
+        Events.register(this);
+    }
+
+    @Subscribe public void handle(Events.FocusScriptArea fsa) {
+        logger.debug("FocusScriptArea handled!");
+        openScripts.get(fsa.getScriptArea()).focus();
+        fsa.getScriptArea().requestFocus();
     }
 
     public ObservableMap<ScriptArea, DockNode> getOpenScripts() {
@@ -111,7 +121,7 @@ public class ScriptController {
 
         this.lastScriptArea = area;
         area.focusedProperty().addListener((observable, oldValue, newValue) -> {
-            System.out.println("area = [" + area + "]");
+            logger.debug("area = [" + area + "]");
             if (newValue)
                 lastScriptArea = area;
         });
@@ -168,7 +178,19 @@ public class ScriptController {
     }
 
     public void saveCurrentScript() {
-        //TODO
+        throw new NotImplementedException();
+    }
+
+    public MainScriptIdentifier getMainScript() {
+        return mainScript.get();
+    }
+
+    public ObjectProperty<MainScriptIdentifier> mainScriptProperty() {
+        return mainScript;
+    }
+
+    public void setMainScript(MainScriptIdentifier mainScript) {
+        this.mainScript.set(mainScript);
     }
 
     private ScriptArea findEditor(ASTNode node) {
@@ -186,13 +208,20 @@ public class ScriptController {
         }
 
         public void remove() {
-            if (lastScriptArea != null)
+            logger.debug("remove highlight");
+            if (lastScriptArea != null) {
+                logger.debug("previous highlight on {} for {}", lastScriptArea, lastRegion);
                 lastScriptArea.getMarkedRegions().remove(lastRegion);
+            }
         }
 
         public void highlight(ASTNode node) {
+            logger.debug("Highlight requested for {}", node);
             remove();
+
             ScriptArea.RegionStyle r = asRegion(node);
+            logger.debug("Region for highlighting: {}", r);
+
             ScriptArea area = findEditor(node);
             area.getMarkedRegions().add(r);
 

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

@@ -5,10 +5,12 @@ import de.uka.ilkd.key.logic.NamespaceSet;
 import de.uka.ilkd.key.logic.Sequent;
 import de.uka.ilkd.key.pp.*;
 import de.uka.ilkd.key.proof.Goal;
+import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 import edu.kit.formal.interpreter.KeYProofFacade;
 import javafx.beans.Observable;
 import javafx.beans.property.SimpleObjectProperty;
+import javafx.beans.value.ObservableBooleanValue;
 import javafx.scene.input.MouseButton;
 import javafx.scene.input.MouseEvent;
 import javafx.scene.layout.*;
@@ -28,7 +30,9 @@ public class SequentView extends CodeArea {
     private LogicPrinter lp;
     private IdentitySequentPrintFilter filter;
     private LogicPrinter.PosTableStringBackend backend;
-    private SimpleObjectProperty<de.uka.ilkd.key.proof.Goal> node = new SimpleObjectProperty<>();
+    private SimpleObjectProperty<de.uka.ilkd.key.proof.Goal> goal = new SimpleObjectProperty<>();
+    private SimpleObjectProperty<de.uka.ilkd.key.proof.Node> node = new SimpleObjectProperty<>();
+    private ObservableBooleanValue rulesAvailable = goal.isNotNull();
     private KeYProofFacade keYProofFacade;
     private TacletContextMenu menu;
 
@@ -63,13 +67,13 @@ public class SequentView extends CodeArea {
         if (backend == null) {
             return;
         }
-        if (e.getButton() == MouseButton.SECONDARY) {
+        if (e.getButton() == MouseButton.SECONDARY && rulesAvailable.get()) {
             CharacterHit hit = hit(e.getX(), e.getY());
             int insertionPoint = hit.getInsertionIndex();
             PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter);
             if (pis == null) return;
 
-            menu = new TacletContextMenu(keYProofFacade, pis, node.get());
+            menu = new TacletContextMenu(keYProofFacade, pis, goal.get());
             menu.setAutoFix(true);
             menu.setAutoHide(true);
             menu.show(this, e.getScreenX(), e.getScreenY());
@@ -125,24 +129,36 @@ public class SequentView extends CodeArea {
 
         clear();
         insertText(0, backend.getString());
-        if (node.get().node().isClosed()) {
+        if (node.get().isClosed()) {
             this.setBorder(new Border(new BorderStroke(Color.RED, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT)));
             this.getStyleClass().add("closed-sequent-view");
         }
     }
 
-    public Goal getNode() {
-        return node.get();
+    public Goal getGoal() {
+        return goal.get();
     }
 
-    public SimpleObjectProperty<Goal> nodeProperty() {
-        return node;
+    public void setGoal(Goal goal) {
+        this.goal.set(goal);
+    }
+
+    public SimpleObjectProperty<Goal> goalProperty() {
+        return goal;
+    }
+
+    public Node getNode() {
+        return node.get();
     }
 
-    public void setNode(Goal node) {
+    public void setNode(Node node) {
         this.node.set(node);
     }
 
+    public SimpleObjectProperty<Node> nodeProperty() {
+        return node;
+    }
+
     public KeYProofFacade getKeYProofFacade() {
         return keYProofFacade;
     }
@@ -150,4 +166,6 @@ public class SequentView extends CodeArea {
     public void setKeYProofFacade(KeYProofFacade keYProofFacade) {
         this.keYProofFacade = keYProofFacade;
     }
+
+
 }

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

@@ -14,6 +14,7 @@ import edu.kit.formal.gui.controller.DebuggerMainWindowController;
 import edu.kit.formal.interpreter.KeYProofFacade;
 import javafx.event.ActionEvent;
 import javafx.fxml.FXML;
+import javafx.scene.Node;
 import javafx.scene.control.ContextMenu;
 import javafx.scene.control.Menu;
 import javafx.scene.control.MenuItem;

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

@@ -3,10 +3,13 @@ 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.interpreter.data.GoalNode;
+import edu.kit.formal.interpreter.data.KeyData;
 import edu.kit.formal.proofscriptparser.ScriptLanguageLexer;
 import javafx.beans.property.Property;
 import javafx.beans.value.ChangeListener;
 import javafx.beans.value.ObservableValue;
+import javafx.collections.ObservableList;
 import javafx.fxml.FXMLLoader;
 import javafx.scene.control.Alert;
 import javafx.scene.control.Label;
@@ -190,9 +193,13 @@ public class Utils {
     }
 
     public static <T> void addDebugListener(Property<T> property, java.util.function.Function<T, String> conv) {
-        property.addListener((observable, oldValue, newValue) ->
-                logger.debug("Property '{}' of '%s' changed from {} to {}", property.getName(),
-                        property.getBean().getClass().getSimpleName(), conv.apply(oldValue), conv.apply(newValue)));
+        property.addListener((observable, oldValue, newValue) -> {
+            String simpleName = property.getBean() != null ? property.getBean().getClass().getSimpleName() : "<n/a>";
+            logger.debug("Property '{}' of '{}' changed from {} to {}", property.getName(),
+                    simpleName,
+                    oldValue == null ? "<null>" : conv.apply(oldValue),
+                    newValue == null ? "<null>" : conv.apply(newValue));
+        });
     }
 
     public static void addDebugListener(ObservableValue<?> o, String id) {
@@ -213,4 +220,15 @@ public class Utils {
         }
         return null;
     }
+
+    public static String reprKeyDataList(ObservableList<GoalNode<KeyData>> kd) {
+        return kd.stream()
+                .map(Utils::reprKeyData)
+                .reduce((a, b) -> a + b)
+                .orElse("<no goal nodes>");
+    }
+
+    public static <T> String reprKeyData(GoalNode<KeyData> t) {
+        return String.valueOf(t.getData().getNode().serialNr());
+    }
 }

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

@@ -21,7 +21,8 @@ public class WelcomePane extends AnchorPane {
         proofScriptDebugger.getWelcomePaneDock().close();
         proofScriptDebugger.showActiveInspector(null);
         proofScriptDebugger.openScript(
-                new File("src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps")
+        //        new File("src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps")
+                new File("src/test/resources/edu/kit/formal/interpreter/contraposition/wo_branching.kps")
         );
 
         proofScriptDebugger.openKeyFile(

src/main/java/edu/kit/formal/interpreter/InterpreterBuilder.java

@@ -161,7 +161,7 @@ public class InterpreterBuilder {
 
             @Override
             public void evaluate(Interpreter<KeyData> interpreter, CallStatement call, VariableAssignment params) {
-                System.out.println("InterpreterBuilder.evaluate");
+                //System.out.println("InterpreterBuilder.evaluate");
             }
         };
         lookup.getBuilders().add(0, ignoreHandler);