First part of splitting mainwindowcontroller

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

@@ -53,7 +53,7 @@ public class ProofScriptDebugger extends Application {
             logger.info("KeY: " + KeYConstants.COPYRIGHT);
             logger.info("KeY Version: " + KeYConstants.VERSION);
             logger.info("KeY Internal: " + KeYConstants.INTERNAL_VERSION);
-            logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
+            //logger.error("sfklsajflksajfsdajfsdalfjsdaf", new IllegalAccessError("dlfsdalfjsadflj"));
 
         } catch (IOException e) {
             e.printStackTrace();

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

 package edu.kit.formal.gui.controller;
 
-import de.uka.ilkd.key.logic.op.IProgramMethod;
-import de.uka.ilkd.key.pp.ProgramPrinter;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.speclang.Contract;
 import edu.kit.formal.gui.controls.*;
@@ -71,7 +69,7 @@ public class DebuggerMainWindowController implements Initializable {
     //@FXML
     //private ScriptArea scriptArea;
     @FXML
-    private ScriptTabsController tabPane;
+    private ScriptTabPane tabPane;
     //@FXML
     //private Tab startTab;
     /***********************************************************************************************************
@@ -89,14 +87,16 @@ public class DebuggerMainWindowController implements Initializable {
     @FXML
     private ToolBar toolbar;
     @FXML
-    private Button buttonStartInterpreter;
+    private SplitMenuButton buttonStartInterpreter;
     @FXML
     private Button startDebugMode;
     /***********************************************************************************************************
      *      GoalView
      * **********************************************************************************************************/
+    //@FXML
+    //private ListView<GoalNode<KeyData>> goalView;
     @FXML
-    private ListView<GoalNode<KeyData>> goalView;
+    private InspectionViewTabPane inspectionViewTabPane;
     private ExecutorService executorService = Executors.newFixedThreadPool(2);
     private KeYProofFacade facade = new KeYProofFacade();
     private ContractLoaderService contractLoaderService = new ContractLoaderService();
@@ -112,11 +112,11 @@ public class DebuggerMainWindowController implements Initializable {
 
     private File initialDirectory;
 
-    @FXML
-    private JavaArea javaSourceCode;
+    // @FXML
+    // private JavaArea javaSourceCode;
 
-    @FXML
-    private SequentView sequentView;
+    //@FXML
+    //private SequentView sequentView;
 
 
     private InterpretingService interpreterService = new InterpretingService();
@@ -169,25 +169,9 @@ public class DebuggerMainWindowController implements Initializable {
         model.scriptFileProperty().addListener((observable, oldValue, newValue) -> {
             statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
         });
+        inspectionViewTabPane.createNewInspectionViewTab(model, true);
 
 
-        model.chosenContractProperty().addListener(o -> {
-            IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
-            javaSourceCode.clear();
-            javaSourceCode.getLineToClass().clear();
-            StringWriter writer = new StringWriter();
-            ProgramPrinter pp = new ProgramPrinter(writer);
-            try {
-                pp.printFullMethodSignature(method);
-                pp.printStatementBlock(method.getBody());
-                writer.flush();
-            } catch (IOException e) {
-                e.printStackTrace();
-            }
-            javaSourceCode.insertText(0, writer.toString());
-        });
-
-//        scriptArea.getMarkedLines().addListener(new SetChangeListener<Integer>() {
         tabPane.getActiveScriptAreaTab().getScriptArea().getMarkedLines().addListener(new SetChangeListener<Integer>() {
 
             @Override
@@ -201,42 +185,9 @@ public class DebuggerMainWindowController implements Initializable {
             model.currentGoalNodesProperty().setAll(fresh);
         });
         model.currentSelectedGoalNodeProperty().bind(blocker.currentSelectedGoalProperty());
-        goalView.itemsProperty().bind(model.currentGoalNodesProperty());
-
-        model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> {
-            goalView.getSelectionModel().select(fresh);
 
-            /* TODO get lines of active statements marked lines
-            javaSourceCode.getMarkedLines().clear();
-            javaSourceCode.getMarkedLines().addAll(
-            );*/
-        });
-
-        goalView.getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> {
-            sequentView.setNode(newValue.getData().getNode());
-        });
-
-        goalView.setCellFactory(GoalNodeListCell::new);
         CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane);
 
-      /*  startTab.textProperty().bind(new StringBinding() {
-            {
-                super.bind(model.scriptFileProperty());
-            }
-
-            @Override
-            protected String computeValue() {
-                if (model.scriptFileProperty().getValue() != null) {
-                    System.out.println(model.scriptFileProperty());
-                    return model.scriptFileProperty().get().getName();
-                } else {
-                    return "Untitled";
-                }
-            }
-
-        });*/
-
-
     }
 
     //region Actions: Execution
@@ -280,8 +231,9 @@ public class DebuggerMainWindowController implements Initializable {
 
             if (debugMode) {
                 blocker.getStepUntilBlock().set(1);
-                blocker.install(currentInterpreter);
             }
+            blocker.install(currentInterpreter);
+
             interpreterService.interpreter.set(currentInterpreter);
             interpreterService.mainScript.set(scripts.get(0));
             interpreterService.start();
@@ -403,14 +355,16 @@ public class DebuggerMainWindowController implements Initializable {
      */
     private File openFileChooserSaveDialog(String title, String description, String... fileEndings) {
         FileChooser fileChooser = getFileChooser(title, description, fileEndings);
-        File file = fileChooser.showSaveDialog(goalView.getScene().getWindow());
+        // File file = fileChooser.showSaveDialog(inspectionViewTabPane.getInspectionViewTab().getGoalView().getScene().getWindow());
+        File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow());
         if (file != null) initialDirectory = file.getParentFile();
         return file;
     }
 
     private File openFileChooserOpenDialog(String title, String description, String... fileEndings) {
         FileChooser fileChooser = getFileChooser(title, description, fileEndings);
-        File file = fileChooser.showOpenDialog(goalView.getScene().getWindow());
+        //File file = fileChooser.showOpenDialog(inspectionViewTabPane.getInspectionViewTab().getGoalView().getScene().getWindow());
+        File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow());
         if (file != null) initialDirectory = file.getParentFile();
         return file;
     }

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

-package edu.kit.formal.gui.controls;
-
-import edu.kit.formal.gui.model.InspectionModel;
-import javafx.fxml.FXMLLoader;
-import javafx.scene.control.Tab;
-
-import java.io.IOException;
-
-/**
- * Right part of the splitpane that displays the different parts of a state
- */
-public class InspectionViewControl extends Tab {
-    public final InspectionModel inspectionModel;
-
-    public InspectionViewControl(InspectionModel inspectionModel) {
-        super();
-        this.inspectionModel = inspectionModel;
-        FXMLLoader loader = new FXMLLoader(getClass().getResource("InspectionView.fxml"));
-        loader.setRoot(this);
-        loader.setController(this);
-        try {
-            loader.load();
-        } catch (IOException e) {
-            e.printStackTrace();
-        }
-
-
-    }
-
-
-}

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

+package edu.kit.formal.gui.controls;
+
+import de.uka.ilkd.key.logic.op.IProgramMethod;
+import de.uka.ilkd.key.pp.ProgramPrinter;
+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.fxml.FXML;
+import javafx.fxml.FXMLLoader;
+import javafx.fxml.Initializable;
+import javafx.scene.Node;
+import javafx.scene.control.ListView;
+import javafx.scene.control.Tab;
+import javafx.scene.input.MouseEvent;
+
+import java.io.IOException;
+import java.io.StringWriter;
+import java.net.URL;
+import java.util.ResourceBundle;
+
+/**
+ * Right part of the splitpane that displays the different parts of a state
+ */
+public class InspectionViewTab extends Tab implements Initializable {
+
+    @FXML
+    private SequentView sequentView;
+    @FXML
+    private JavaArea javaSourceCode;
+    @FXML
+    private ListView goalView;
+    private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
+
+    public InspectionViewTab() {
+        super();
+        FXMLLoader loader = new FXMLLoader(getClass().getResource("InspectionView.fxml"));
+        loader.setRoot(this);
+        loader.setController(this);
+        try {
+            loader.load();
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+
+        goalView.setVisible(true);
+    }
+
+    public SequentView getSequentView() {
+        return sequentView;
+    }
+
+    public JavaArea getJavaSourceCode() {
+        return javaSourceCode;
+    }
+
+    public ListView<GoalNode<KeyData>> getGoalView() {
+        return goalView;
+    }
+
+    public GoalOptionsMenu getGoalOptionsMenu() {
+        return goalOptionsMenu;
+    }
+
+    public void showGoalOptions(MouseEvent actionEvent) {
+        Node n = (Node) actionEvent.getTarget();
+        goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
+    }
+
+    public void initialize(InspectionModel model) {
+
+        System.out.println("model");
+    }
+
+    public void refresh(RootModel model) {
+        IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
+        getJavaSourceCode().clear();
+        getJavaSourceCode().getLineToClass().clear();
+        //javaSourceCode.clear();
+        //javaSourceCode.getLineToClass().clear();
+        StringWriter writer = new StringWriter();
+        ProgramPrinter pp = new ProgramPrinter(writer);
+        try {
+            pp.printFullMethodSignature(method);
+            pp.printStatementBlock(method.getBody());
+            writer.flush();
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+        getJavaSourceCode().insertText(0, writer.toString());
+        // javaSourceCode.insertText(0, writer.toString());
+
+    }
+
+
+    @Override
+    public void initialize(URL location, ResourceBundle resources) {
+        getGoalView().getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> {
+            getSequentView().setNode(newValue.getData().getNode());
+        });
+    }
+}

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

+package edu.kit.formal.gui.controls;
+
+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;
+import javafx.fxml.FXML;
+import javafx.fxml.FXMLLoader;
+import javafx.scene.control.ListCell;
+import javafx.scene.control.ListView;
+import javafx.scene.control.TabPane;
+
+import java.io.IOException;
+
+/**
+ * TabPane on the right side of the GUI containing the inspection view as tabs
+ */
+public class InspectionViewTabPane extends TabPane {
+
+    private InspectionViewTab activeInterpreterTab;
+    @FXML
+    private InspectionViewTab inspectionViewTab;
+
+    public InspectionViewTabPane() {
+        super();
+        FXMLLoader loader = new FXMLLoader(getClass().getResource("InspectionViewTabPane.fxml"));
+        loader.setRoot(this);
+        loader.setController(this);
+        try {
+            loader.load();
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+
+        // this.setActiveInterpreterTab(inspectionViewTab);
+
+
+        // getActiveInspectionViewTab().getGoalView().setCellFactory(GoalNodeListCell::new);
+
+
+    }
+
+    public InspectionViewTab getInspectionViewTab() {
+        return inspectionViewTab;
+    }
+
+    public void setActiveInterpreterTab(InspectionViewTab activeInterpreterTab) {
+        this.activeInterpreterTab = activeInterpreterTab;
+    }
+
+    public InspectionViewTab getActiveInspectionViewTab() {
+        return this.activeInterpreterTab;
+    }
+
+    public void createNewInspectionViewTab(RootModel model, boolean activeTab) {
+        InspectionViewTab tab = new InspectionViewTab();
+        if (activeTab) {
+            this.setActiveInterpreterTab(tab);
+        }
+        tab.getGoalView().setCellFactory(GoalNodeListCell::new);
+        model.chosenContractProperty().addListener(o -> {
+            tab.refresh(model);
+        });
+        bindGoalNodesWithCurrentTab(model);
+        tab.getGoalView().setCellFactory(GoalNodeListCell::new);
+        tab.setText("New Tab");
+        if (activeTab) {
+            this.setActiveInterpreterTab(tab);
+        }
+        this.getTabs().add(tab);
+
+
+        // inspectionViewTabPane.getInspectionViewTab().getGoalView().setCellFactory(GoalNodeListCell::new);
+
+    }
+
+    public void refresh(RootModel model) {
+        getActiveInspectionViewTab().refresh(model);
+    }
+
+    public void bindGoalNodesWithCurrentTab(RootModel model) {
+        getActiveInspectionViewTab().getGoalView().itemsProperty().bind(model.currentGoalNodesProperty());
+        model.currentSelectedGoalNodeProperty().addListener((p, old, fresh) -> {
+            getActiveInspectionViewTab().getGoalView().getSelectionModel().select(fresh);
+            /* TODO get lines of active statements marked lines
+            javaSourceCode.getMarkedLines().clear();
+            javaSourceCode.getMarkedLines().addAll(
+            );*/
+        });
+
+    }
+
+    /**
+     * Cells for GoalView
+     */
+    private class GoalNodeListCell extends ListCell<GoalNode<KeyData>> {
+
+        public GoalNodeListCell(ListView<GoalNode<KeyData>> goalNodeListView) {
+            itemProperty().addListener(this::update);
+
+            // goalOptionsMenu.selectedViewOptionProperty().addListener(this::update);
+        }
+
+        private void update(Observable observable) {
+            if (getItem() == null) {
+                setText("");
+                return;
+            }
+            KeyData item = getItem().getData();
+            String text = "n/a";
+           /* if (goalOptionsMenu.getSelectedViewOption() != null) {
+                text = goalOptionsMenu.getSelectedViewOption().getText(item);
+            }*/
+            setText(text);
+        }
+    }
+
+
+}

src/main/java/edu/kit/formal/gui/controls/ScriptTabsController.java → src/main/java/edu/kit/formal/gui/controls/ScriptTabPane.java

@@ -13,7 +13,7 @@ import java.util.Iterator;
 /**
  * Controller for TabPane
  */
-public class ScriptTabsController extends TabPane {
+public class ScriptTabPane extends TabPane {
     /**
      * String is filepath; if string already exists if new tab should be created nothing happens
      * If wished for, instead of filepath an object with omre script information may be used
@@ -23,7 +23,7 @@ public class ScriptTabsController extends TabPane {
 
     private SimpleObjectProperty<Tab> activeTab = new SimpleObjectProperty<>();
 
-    public ScriptTabsController() {
+    public ScriptTabPane() {
         super();
         FXMLLoader loader = new FXMLLoader(getClass().getResource("TabPaneScriptArea.fxml"));
         loader.setRoot(this);

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

@@ -30,4 +30,77 @@ public class InspectionModel {
     private Set<Integer> highlightedJavaLines;
 
     private boolean closable;
+    private boolean isInterpreterTab;
+
+    public ASTNode getNode() {
+        return node;
+    }
+
+    public void setNode(ASTNode node) {
+        this.node = node;
+    }
+
+    public List<GoalNode> getCurrentGoals() {
+        return currentGoals;
+    }
+
+    public void setCurrentGoals(List<GoalNode> currentGoals) {
+        this.currentGoals = currentGoals;
+    }
+
+    public GoalNode getSelectedGoalNodeToShow() {
+        return selectedGoalNodeToShow;
+    }
+
+    public void setSelectedGoalNodeToShow(GoalNode selectedGoalNodeToShow) {
+        this.selectedGoalNodeToShow = selectedGoalNodeToShow;
+    }
+
+    public Map<GoalNode, Color> getColorofEachGoalNodeinListView() {
+        return colorofEachGoalNodeinListView;
+    }
+
+    public void setColorofEachGoalNodeinListView(Map<GoalNode, Color> colorofEachGoalNodeinListView) {
+        this.colorofEachGoalNodeinListView = colorofEachGoalNodeinListView;
+    }
+
+    public boolean isShowJavaView() {
+        return showJavaView;
+    }
+
+    public void setShowJavaView(boolean showJavaView) {
+        this.showJavaView = showJavaView;
+    }
+
+    public String getJavaString() {
+        return javaString;
+    }
+
+    public void setJavaString(String javaString) {
+        this.javaString = javaString;
+    }
+
+    public Set<Integer> getHighlightedJavaLines() {
+        return highlightedJavaLines;
+    }
+
+    public void setHighlightedJavaLines(Set<Integer> highlightedJavaLines) {
+        this.highlightedJavaLines = highlightedJavaLines;
+    }
+
+    public boolean isClosable() {
+        return closable;
+    }
+
+    public void setClosable(boolean closable) {
+        this.closable = closable;
+    }
+
+    public boolean isInterpreterTab() {
+        return isInterpreterTab;
+    }
+
+    public void setInterpreterTab(boolean interpreterTab) {
+        isInterpreterTab = interpreterTab;
+    }
 }

src/main/resources/DebuggerMain.fxml

@@ -2,11 +2,12 @@
 
 
 <?import de.jensd.fx.glyphs.materialdesignicons.*?>
-<?import edu.kit.formal.gui.controls.*?>
-<?import javafx.geometry.Insets?>
+<?import edu.kit.formal.gui.controls.DebuggerStatusBar?>
+<?import edu.kit.formal.gui.controls.InspectionViewTabPane?>
+<?import edu.kit.formal.gui.controls.ScriptTabPane?>
 <?import javafx.scene.control.*?>
-<?import javafx.scene.layout.*?>
-<?import org.controlsfx.control.StatusBar?>
+<?import javafx.scene.layout.BorderPane?>
+<?import javafx.scene.layout.VBox?>
 <BorderPane xmlns:fx="http://javafx.com/fxml/1" fx:id="rootPane" xmlns="http://javafx.com/javafx/8.0.112"
             fx:controller="edu.kit.formal.gui.controller.DebuggerMainWindowController"
             prefWidth="1024" prefHeight="640">
@@ -18,7 +19,7 @@
                         <ToolBar fx:id="toolbar">
                             <items>
 
-                                <SplitMenuButton onAction="#executeScript"
+                                <SplitMenuButton fx:id="buttonStartInterpreter" onAction="#executeScript"
                                                  disable="${controller.executeNotPossible}">
                                     <graphic>
                                         <MaterialDesignIconView glyphName="PLAY" size="24.0"/>
@@ -98,8 +99,8 @@
                                 </Button>
                             </items>
                         </ToolBar>
-                        <ScriptTabsController fx:id="tabPane" side="left" styleClass="tab-pane"
-                                              tabClosingPolicy="SELECTED_TAB" VBox.vgrow="ALWAYS"/>
+                        <ScriptTabPane fx:id="tabPane" side="left" styleClass="tab-pane"
+                                       tabClosingPolicy="SELECTED_TAB" VBox.vgrow="ALWAYS"/>
                         <!--    <TabPane fx:id="tabPane" side="left" styleClass="tab-pane"
                                      tabClosingPolicy="SELECTED_TAB" VBox.vgrow="ALWAYS">
                                 <tabs>
@@ -114,9 +115,10 @@
 
                     </children>
                 </VBox>
-                <SplitPane orientation="VERTICAL" dividerPositions="0.25,0.75">
+                <InspectionViewTabPane fx:id="inspectionViewTabPane"></InspectionViewTabPane>
+                <!--<SplitPane orientation="VERTICAL" dividerPositions="0.25,0.75">
                     <items>
-                        <SectionPane title="Current Goals">
+                       <SectionPane title="Current Goals">
                             <headerRight>
                                 <Button onMouseClicked="#showGoalOptions">
                                     <graphic>
@@ -154,7 +156,7 @@
                             </items>
                         </SplitPane>
                     </items>
-                </SplitPane>
+                </SplitPane>-->
             </items>
         </SplitPane>
     </center>

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

@@ -6,7 +6,9 @@
 <?import javafx.scene.control.*?>
 <fx:root xmlns:fx="http://javafx.com/fxml"
          xmlns="http://javafx.com/javafx"
-         type="javafx.scene.control.Tab">
+         type="edu.kit.formal.gui.controls.InspectionViewTab">
+    <SplitPane orientation="VERTICAL" dividerPositions="0.25,0.75">
+        <items>
     <SectionPane title="Current Goals">
         <headerRight>
             <Button onMouseClicked="#showGoalOptions">
@@ -44,5 +46,7 @@
             </SectionPane>
         </items>
     </SplitPane>
+        </items>
+    </SplitPane>
 
 </fx:root>
\ No newline at end of file

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

+<?xml version="1.0" encoding="UTF-8"?>
+
+<?import edu.kit.formal.gui.controls.InspectionViewTabPane?>
+<fx:root xmlns:fx="http://javafx.com/fxml/1" prefHeight="100" prefWidth="250" styleClass="tab-pane"
+         type="edu.kit.formal.gui.controls.InspectionViewTabPane" xmlns="http://javafx.com/javafx/8.0.112">