A lot of simplifications

src/main/java/edu/kit/formal/gui/ProofScriptDebugger.java

@@ -8,6 +8,7 @@ package edu.kit.formal.gui;
 
 import de.uka.ilkd.key.util.KeYConstants;
 import javafx.application.Application;
+import javafx.application.Platform;
 import javafx.fxml.FXMLLoader;
 import javafx.scene.Parent;
 import javafx.scene.Scene;
@@ -39,6 +40,7 @@ public class ProofScriptDebugger extends Application {
             Parent root = fxmlLoader.load();
             //DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
             Scene scene = new Scene(root);
+            primaryStage.setOnCloseRequest(event -> Platform.exit());
             scene.getStylesheets().addAll(
                     getClass().getResource("debugger-ui.css").toExternalForm(),
                     DockNode.class.getResource("default.css").toExternalForm()
@@ -55,10 +57,14 @@ public class ProofScriptDebugger extends Application {
             logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
             //logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
 
+
         } catch (IOException e) {
             e.printStackTrace();
         }
+    }
 
-
+    @Override
+    public void stop() throws Exception {
+        System.exit(0);//needed, else non-termination of process
     }
 }

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

@@ -12,6 +12,7 @@ import javafx.stage.Modality;
 import lombok.Getter;
 
 import java.awt.event.KeyEvent;
+import java.util.List;
 
 /**
  * A Contract Chooser is a modal dialog, which shows a list of contracts and lets the user select one.
@@ -66,6 +67,11 @@ public class ContractChooser extends Dialog<Contract> {
         listOfContractsView.itemsProperty().bind(contracts);
     }
 
+    public ContractChooser(Services service, List<Contract> contracts) {
+        this(service);
+        listOfContractsView.itemsProperty().get().setAll(contracts);
+    }
+
     public MultipleSelectionModel<Contract> getSelectionModel() {
         return selectionModel;
     }

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

-package edu.kit.formal.gui.controller;
-
-import edu.kit.formal.gui.controls.Utils;
-import edu.kit.formal.gui.model.RootModel;
-import edu.kit.formal.interpreter.data.GoalNode;
-import edu.kit.formal.interpreter.data.KeyData;
-import javafx.beans.property.SimpleListProperty;
-import javafx.fxml.FXML;
-import javafx.fxml.FXMLLoader;
-import javafx.scene.control.ListCell;
-import javafx.scene.control.ListView;
-import javafx.scene.control.TextArea;
-import javafx.scene.layout.VBox;
-
-import java.io.IOException;
-
-/**
- * Created by sarah on 5/27/17.
- */
-public class ListGoalView extends VBox {
-    protected SimpleListProperty<GoalNode<KeyData>> localGoalListProperty = new SimpleListProperty<>();
-    @FXML
-    private ListView<GoalNode<KeyData>> listOfGoalsView;
-    @FXML
-    private TextArea goalNodeView;
-
-    private RootModel rootModel;
-
-    public ListGoalView() {
-        Utils.createWithFXML(this);
-        listOfGoalsView.setCellFactory(list -> new GoalNodeCell());
-    }
-
-
-    public void setRootModel(RootModel rootModel) {
-        this.rootModel = rootModel;
-    }
-
-    /**
-     * Set Bindings and listener
-     */
- /*   public void init() {
-        listOfGoalsView.itemsProperty().bind(this.rootModel.currentGoalNodesProperty());
-
-        listOfGoalsView.getSelectionModel().selectedItemProperty().addListener(new ChangeListener<GoalNode<KeyData>>() {
-            @Override
-            public void changed(ObservableValue<? extends GoalNode<KeyData>> observable, GoalNode<KeyData> oldValue, GoalNode<KeyData> newValue) {
-                goalNodeView.setText(newValue.toCellTextForKeYData());
-            }
-        });
-
-    }
-*/
-
-    private static class GoalNodeCell extends ListCell<GoalNode<KeyData>> {
-
-        @Override
-        protected void updateItem(GoalNode<KeyData> item, boolean empty) {
-            super.updateItem(item, empty);
-            if (item != null) {
-                setText(item.toListLabelForKeYData());
-            }
-        }
-
-    }
-}

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

 package edu.kit.formal.gui.controls;
 
 import edu.kit.formal.gui.model.InspectionModel;
-import edu.kit.formal.gui.model.RootModel;
 import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.KeyData;
 import javafx.beans.Observable;
@@ -20,7 +19,7 @@ import javafx.scene.layout.BorderPane;
  *
  * @author S. Grebing
  */
-public class InspectionViewTab extends BorderPane {
+public class InspectionView extends BorderPane {
     public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
 
     @FXML
@@ -33,8 +32,7 @@ public class InspectionViewTab extends BorderPane {
             new InspectionModel()
     );
 
-    public InspectionViewTab() {
-        super();
+    public InspectionView() {
         Utils.createWithFXML(this);
 
         model.get().selectedGoalNodeToShowProperty().bind(
@@ -85,21 +83,6 @@ public class InspectionViewTab extends BorderPane {
         goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
     }
 
-    public void refresh(RootModel model) {
-     /*   IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
-        StringWriter writer = new StringWriter();
-        ProgramPrinter pp = new ProgramPrinter(writer);
-        try {
-            pp.printFullMethodSignature(method);
-            pp.printStatementBlock(method.getBody());
-            writer.flush();
-        } catch (IOException e) {
-            e.printStackTrace();
-        }
-        */
-
-    }
-
     /**
      * Cells for GoalView
      */

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

 package edu.kit.formal.gui.controls;
 
-import edu.kit.formal.gui.model.RootModel;
 import javafx.beans.property.SimpleMapProperty;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableMap;
 import org.dockfx.DockNode;
 
 /**
- * TabPane on the right side of the GUI containing the inspection view as tabs
+ * This controller manages a list of {@link InspectionView} and the associated {@link DockNode}s.
+ *
+ * Espeically, this class holds the active tab, which is connected with the {@link edu.kit.formal.interpreter.graphs.ProofTreeController},
+ * and shows the current interpreter state.
+ *
+ * @author weigl
  */
 public class InspectionViewsController {
 
@@ -16,23 +20,31 @@ public class InspectionViewsController {
      * This tab can be changed and later on in this tab it should be possible to select proof commands
      * All other tabs are only post morten tabs which cannot be shown
      */
-    private final InspectionViewTab activeInterpreterTab = new InspectionViewTab();
+    private final InspectionView activeInterpreterTab = new InspectionView();
     private final DockNode activeInterpreterTabDock = new DockNode(activeInterpreterTab, "Active");
+    private final ObservableMap<InspectionView, DockNode> inspectionViews = new SimpleMapProperty<>(FXCollections.observableHashMap());
 
-    private final ObservableMap<InspectionViewTab, DockNode> inspectionViews = new SimpleMapProperty<>(FXCollections.observableHashMap());
-
-    public InspectionViewTab getActiveInspectionViewTab() {
+    public InspectionView getActiveInspectionViewTab() {
         return this.activeInterpreterTab;
     }
+
     public DockNode getActiveInterpreterTabDock() {
         return activeInterpreterTabDock;
     }
 
-    public void connectActiveView(RootModel model) {
+
+    public DockNode newPostMortemInspector() {
+        InspectionView iv = new InspectionView();
+        DockNode dn = new DockNode(iv, "post mortem: ");
+        inspectionViews.put(iv, dn);
+        return dn;
+    }
+
+    /*public void connectActiveView(DebuggerModel model) {
         getActiveInspectionViewTab().getGoalView().itemsProperty().bind(model.currentGoalNodesProperty());
         model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> {
             getActiveInspectionViewTab().getGoalView().getSelectionModel().select(fresh);
         });
 
-    }
+    }*/
 }

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

@@ -34,6 +34,8 @@ import lombok.RequiredArgsConstructor;
 import org.antlr.v4.runtime.CharStream;
 import org.antlr.v4.runtime.CharStreams;
 import org.antlr.v4.runtime.Token;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 import org.controlsfx.control.PopOver;
 import org.fxmisc.richtext.CharacterHit;
 import org.fxmisc.richtext.CodeArea;
@@ -49,19 +51,26 @@ import java.util.*;
 import java.util.function.IntFunction;
 
 /**
- * ScriptArea is the textarea on the left side of the GUI.
+ * ScriptArea is the {@link CodeArea} for writing Proof Scripts.
+ * <p>
  * It displays the script code and allows highlighting of lines and setting of breakpoints
  */
 public class ScriptArea extends CodeArea {
-    private final ObjectProperty<File> filePath = new SimpleObjectProperty<>();
+    private static final Logger LOGGER = LogManager.getLogger(ScriptArea.class);
+    /**
+     * Underlying filepath, should not be null
+     */
+    private final ObjectProperty<File> filePath = new SimpleObjectProperty<>(new File(Utils.getRandomName()));
 
+    /**
+     * If true, the content was changed since last save.
+     */
     private final BooleanProperty dirty = new SimpleBooleanProperty(this, "dirty", false);
 
     /**
-     * Lines to highlight?
+     * CSS classes for regions, used for "manually" highlightning. e.g. debugging marker
      */
-    private final SetProperty<RegionStyle> markedRegions =
-            new SimpleSetProperty<>(FXCollections.observableSet());
+    private final SetProperty<RegionStyle> markedRegions = new SimpleSetProperty<>(FXCollections.observableSet());
     /**
      * set by {@link ScriptController}
      */
@@ -71,7 +80,7 @@ public class ScriptArea extends CodeArea {
     private ANTLR4LexerHighlighter highlighter;
     private ListProperty<LintProblem> problems = new SimpleListProperty<>(FXCollections.observableArrayList());
     private SimpleObjectProperty<CharacterHit> currentMouseOver = new SimpleObjectProperty<>();
-    private ScriptAreaContextMenu contextMenu;
+    private ScriptAreaContextMenu contextMenu = new ScriptAreaContextMenu();
 
 
     public ScriptArea() {
@@ -84,8 +93,11 @@ public class ScriptArea extends CodeArea {
         highlighter = new ANTLR4LexerHighlighter(
                 (String val) -> new ScriptLanguageLexer(CharStreams.fromString(val)));
         this.setParagraphGraphicFactory(gutter);
-        //getStylesheets().add(getClass().getResource("script-keywords.css").toExternalForm());
         getStyleClass().add("script-area");
+        installPopup();
+
+        setOnMouseClicked(this::showContextMenu);
+
         textProperty().addListener((prop, oldValue, newValue) -> {
             dirty.set(true);
             updateMainScriptMarker();
@@ -105,8 +117,6 @@ public class ScriptArea extends CodeArea {
                         return Optional.empty();
                     }
                 }).subscribe(s -> setStyleSpans(0, s));*/
-        getStyleClass().add("script-area");
-        installPopup();
 
 
         this.addEventHandler(MouseEvent.MOUSE_PRESSED, (MouseEvent e) -> {
@@ -118,10 +128,20 @@ public class ScriptArea extends CodeArea {
             this.moveTo(characterPosition, NavigationActions.SelectionPolicy.CLEAR);
         });
 
-        mainScript.addListener((observable) ->
-                updateMainScriptMarker());
+        mainScript.addListener((observable) -> updateMainScriptMarker());
+    }
+
+    public void showContextMenu(MouseEvent mouseEvent) {
+        if (contextMenu.isShowing())
+            contextMenu.hide();
+
+        if (mouseEvent.getButton() == MouseButton.SECONDARY) {
+            contextMenu.setAutoHide(true);
+            contextMenu.show(this, mouseEvent.getScreenX(), mouseEvent.getScreenY());
+            mouseEvent.consume();
+        } else {
 
-        contextMenu = new ScriptAreaContextMenu();
+        }
     }
 
     private void updateHighlight() {
@@ -517,7 +537,7 @@ public class ScriptArea extends CodeArea {
         }
 
         public void setMainScript(ActionEvent event) {
-            System.out.println("ScriptAreaContextMenu.setMainScript");
+            LOGGER.debug("ScriptAreaContextMenu.setMainScript");
             List<ProofScript> ast = Facade.getAST(getText());
             int pos = currentMouseOver.get().getInsertionIndex();
             ast.stream().filter(ps ->
@@ -531,6 +551,10 @@ public class ScriptArea extends CodeArea {
         }
 
         public void showPostMortem(ActionEvent event) {
+            LOGGER.debug("ScriptAreaContextMenu.showPostMortem " + event);
+
+
+
             //TODO forward to ProofTreeController, it jumps to the node and this should be done via the callbacks.
 
             /*ScriptArea area = ScriptArea.this;

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

 package edu.kit.formal.gui.controls;
 
 import edu.kit.formal.gui.controller.DebuggerMainWindowController;
+import javafx.event.ActionEvent;
 import javafx.scene.layout.AnchorPane;
 
-import java.awt.event.ActionEvent;
 import java.io.File;
 
 /**
@@ -17,7 +17,7 @@ public class WelcomePane extends AnchorPane {
         Utils.createWithFXML(this);
     }
 
-    public void loadContraPosition(javafx.event.ActionEvent event) {
+    public void loadContraPosition(ActionEvent event) {
         proofScriptDebugger.getWelcomePaneDock().close();
         proofScriptDebugger.showActiveInspector(null);
         proofScriptDebugger.openScript(
@@ -28,4 +28,15 @@ public class WelcomePane extends AnchorPane {
                 new File("src/test/resources/edu/kit/formal/interpreter/contraposition/contraposition.key"));
 
     }
+
+    public void loadJavaTest(ActionEvent event) {
+        proofScriptDebugger.getWelcomePaneDock().close();
+        proofScriptDebugger.showActiveInspector(null);
+        proofScriptDebugger.openScript(
+                new File("src/test/resources/edu/kit/formal/interpreter/dbg.kps")
+        );
+
+        proofScriptDebugger.openJavaFile(
+                new File("src/test/resources/edu/kit/formal/interpreter/javaExample/TwoWaySwap.java"));
+    }
 }

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

@@ -24,6 +24,8 @@ public class InspectionModel {
     private final ObjectProperty<ASTNode> node = new SimpleObjectProperty<>();
     private final ListProperty<GoalNode<KeyData>> goals = new SimpleListProperty<>();
     private final ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShow = new SimpleObjectProperty<>();
+    private final ObjectProperty<GoalNode<KeyData>> currentInterpreterGoal = new SimpleObjectProperty<>();
+
     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());
@@ -31,6 +33,31 @@ public class InspectionModel {
     private final BooleanProperty isInterpreterTab = new SimpleBooleanProperty();
     private ObjectProperty<Mode> mode = new SimpleObjectProperty<>();
 
+
+    public GoalNode<KeyData> getCurrentInterpreterGoal() {
+        return currentInterpreterGoal.get();
+    }
+
+    public ObjectProperty<GoalNode<KeyData>> currentInterpreterGoalProperty() {
+        return currentInterpreterGoal;
+    }
+
+    public void setCurrentInterpreterGoal(GoalNode<KeyData> currentInterpreterGoal) {
+        this.currentInterpreterGoal.set(currentInterpreterGoal);
+    }
+
+    public Mode getMode() {
+        return mode.get();
+    }
+
+    public ObjectProperty<Mode> modeProperty() {
+        return mode;
+    }
+
+    public void setMode(Mode mode) {
+        this.mode.set(mode);
+    }
+
     public ASTNode getNode() {
         return node.get();
     }

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

-package edu.kit.formal.gui.model;
-
-
-import de.uka.ilkd.key.speclang.Contract;
-import edu.kit.formal.interpreter.data.GoalNode;
-import edu.kit.formal.interpreter.data.KeyData;
-import javafx.beans.property.ListProperty;
-import javafx.beans.property.SimpleListProperty;
-import javafx.beans.property.SimpleObjectProperty;
-import javafx.collections.FXCollections;
-import javafx.collections.ObservableList;
-
-import java.io.File;
-
-/**
- * Model for the root window
- *
- * @author S. Grebing
- */
-public class RootModel {
-
-    /**
-     * Property: current loaded ScriptFile
-     */
-    private final SimpleObjectProperty<File> scriptFile = new SimpleObjectProperty<>();
-
-
-    /**
-     * Property: current loaded javaFile
-     */
-    private final SimpleObjectProperty<File> javaFile = new SimpleObjectProperty<>();
-
-    /**
-     * Property: current loaded KeY File
-     */
-    private final SimpleObjectProperty<File> keYFile = new SimpleObjectProperty<>();
-
-
-    /**
-     * ListProperty: list of goal nodes in the current state (depending on interpreter state)
-     */
-    private final ListProperty<GoalNode<KeyData>> currentGoalNodes = new SimpleListProperty<>(FXCollections.observableArrayList());
-
-    /**
-     * Current SelectedGoalNode
-     */
-    private final SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalNode = new SimpleObjectProperty<>();
-
-    /**
-     * Loaded contracts
-     */
-    private final SimpleListProperty<Contract> loadedContracts = new SimpleListProperty<>(FXCollections.observableArrayList());
-
-    /**
-     * Chosen contract for problem
-     */
-    private final SimpleObjectProperty<Contract> chosenContract = new SimpleObjectProperty<>();
-
-    public RootModel() {
-
-    }
-
-
-    /*****************************************************************************************************************
-     *                                          Property Getter and Setter
-     ***************************************************************************************************************/
-    public File getScriptFile() {
-        return scriptFile.get();
-    }
-
-    public void setScriptFile(File scriptFile) {
-        this.scriptFile.set(scriptFile);
-    }
-
-    public SimpleObjectProperty<File> scriptFileProperty() {
-        return scriptFile;
-    }
-
-    public File getKeYFile() {
-        return keYFile.get();
-    }
-
-    public void setKeYFile(File keYFile) {
-        this.keYFile.set(keYFile);
-    }
-
-    public SimpleObjectProperty<File> keYFileProperty() {
-        return keYFile;
-    }
-
-    public ObservableList<GoalNode<KeyData>> getCurrentGoalNodes() {
-        return currentGoalNodes.get();
-    }
-
-    public void setCurrentGoalNodes(ObservableList<GoalNode<KeyData>> currentGoalNodes) {
-        this.currentGoalNodes.set(currentGoalNodes);
-    }
-
-    public ListProperty<GoalNode<KeyData>> currentGoalNodesProperty() {
-        return currentGoalNodes;
-    }
-
-    public GoalNode<KeyData> getCurrentSelectedGoalNode() {
-        return currentSelectedGoalNode.get();
-    }
-
-    public void setCurrentSelectedGoalNode(GoalNode<KeyData> currentSelectedGoalNode) {
-        this.currentSelectedGoalNode.set(currentSelectedGoalNode);
-    }
-
-    public SimpleObjectProperty<GoalNode<KeyData>> currentSelectedGoalNodeProperty() {
-        return currentSelectedGoalNode;
-    }
-
-    public File getJavaFile() {
-        return javaFile.get();
-    }
-
-    public void setJavaFile(File javaFile) {
-        this.javaFile.set(javaFile);
-    }
-
-    public SimpleObjectProperty<File> javaFileProperty() {
-        return javaFile;
-    }
-
-    public ObservableList<Contract> getLoadedContracts() {
-        return loadedContracts.get();
-    }
-
-    public void setLoadedContracts(ObservableList<Contract> loadedContracts) {
-        this.loadedContracts.set(loadedContracts);
-    }
-
-    public SimpleListProperty<Contract> loadedContractsProperty() {
-        return loadedContracts;
-    }
-
-    public Contract getChosenContract() {
-        return chosenContract.get();
-    }
-
-    public void setChosenContract(Contract chosenContract) {
-        this.chosenContract.set(chosenContract);
-    }
-
-    public SimpleObjectProperty<Contract> chosenContractProperty() {
-        return chosenContract;
-    }
-
-
-}

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

 package edu.kit.formal.interpreter;
 
-import edu.kit.formal.gui.controller.DebuggerMainWindowController;
 import edu.kit.formal.gui.controller.PuppetMaster;
+import edu.kit.formal.gui.controls.Utils;
 import edu.kit.formal.interpreter.data.KeyData;
 import edu.kit.formal.interpreter.data.State;
 import edu.kit.formal.proofscriptparser.ast.ProofScript;
@@ -50,7 +50,7 @@ public class InterpretingService extends Service<State<KeyData>> {
     @Override
     protected void failed() {
         getException().printStackTrace();
-        DebuggerMainWindowController.showExceptionDialog("Execution failed", "", "", getException());
+        Utils.showExceptionDialog("Execution failed", "", "", getException());
         updateView();
     }
 

src/main/java/edu/kit/formal/interpreter/graphs/ProofTreeController.java

@@ -11,6 +11,8 @@ import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import javafx.application.Platform;
 import javafx.beans.property.*;
 import javafx.collections.FXCollections;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
 
 import java.util.List;
 
@@ -20,6 +22,7 @@ import java.util.List;
  * @author S. Grebing
  */
 public class ProofTreeController {
+    private static final Logger LOGGER = LogManager.getLogger(ProofTreeController.class);
 
     /**
      * To control stepping
@@ -240,10 +243,12 @@ public class ProofTreeController {
      * @param state
      */
     private void setNewState(State<KeyData> state) {
-        this.setCurrentGoals(state.getGoals());
-        this.setCurrentSelectedGoal(state.getSelectedGoalNode());
+        setCurrentGoals(state.getGoals());
+        setCurrentSelectedGoal(state.getSelectedGoalNode());
         setCurrentHighlightNode(statePointer.getScriptstmt());
-        System.out.println("New State from this command: " + this.statePointer.getScriptstmt().getNodeName() + "@" + this.statePointer.getScriptstmt().getStartPosition());
+        LOGGER.debug("New State from this command: %s@%s",
+                this.statePointer.getScriptstmt().getNodeName(),
+                this.statePointer.getScriptstmt().getStartPosition());
     }
 
     /**************************************************************************************************************