embedd a docking framework

* works, but needed some adaptions or fixes

.gitmodules

 [submodule "doc"]
 	path = doc
 	url = git@git.scc.kit.edu:xt9634/ProofScriptParser.wiki.git
+[submodule "lib/AnchorFX"]
+	path = lib/AnchorFX
+	url = https://github.com/alexbodogit/AnchorFX.git
+[submodule "lib/DockFX"]
+	path = lib/DockFX
+	url = https://github.com/RobertBColton/DockFX.git

AnchorFX @ 0773eb44

+Subproject commit 0773eb4419e126d2cfa18863306ad1c48050e9b6

DockFX @ bbbc5765

+Subproject commit bbbc57653d6a0bc7463539de30fec075443c0843

pom.xml

@@ -72,6 +72,51 @@
         </pluginManagement>
 
         <plugins>
+            <plugin>
+                <groupId>org.codehaus.mojo</groupId>
+                <artifactId>build-helper-maven-plugin</artifactId>
+                <version>1.7</version>
+                <executions>
+                    <execution>
+                        <id>released-version</id>
+                        <goals>
+                            <goal>released-version</goal>
+                        </goals>
+                    </execution>
+
+                    <execution>
+                        <id>add-source</id>
+                        <phase>generate-sources</phase>
+                        <goals>
+                            <goal>add-source</goal>
+                        </goals>
+                        <configuration>
+                            <sources>
+                                <source>lib/AnchorFX/src/main/java</source>
+                                <source>lib/DockFX/src/main/java</source>
+                            </sources>
+                        </configuration>
+                    </execution>
+
+                    <execution>
+                        <id>add-resource</id>
+                        <phase>generate-resources</phase>
+                        <goals>
+                            <goal>add-resource</goal>
+                        </goals>
+                        <configuration>
+                            <resources>
+                                <resource>
+                                    <directory>lib/AnchorFX/src/main/resources</directory>
+                                    <directory>lib/DockFX/src/main/resources</directory>
+                                </resource>
+                            </resources>
+                        </configuration>
+                    </execution>
+
+                </executions>
+            </plugin>
+
             <plugin>
                 <groupId>org.codehaus.mojo</groupId>
                 <artifactId>jaxb2-maven-plugin</artifactId>

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

@@ -14,6 +14,7 @@ import javafx.scene.Scene;
 import javafx.stage.Stage;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
+import org.dockfx.DockNode;
 
 import java.io.IOException;
 import java.util.Locale;
@@ -33,15 +34,14 @@ public class ProofScriptDebugger extends Application {
     public void start(Stage primaryStage) {
         Locale.setDefault(Locale.ENGLISH);
 
-        
-
         try {
             FXMLLoader fxmlLoader = new FXMLLoader(getClass().getResource("/DebuggerMain.fxml"));
             Parent root = fxmlLoader.load();
             //DebuggerMainWindowController controller = fxmlLoader.<DebuggerMainWindowController>getController();
             Scene scene = new Scene(root);
             scene.getStylesheets().addAll(
-                    getClass().getResource("debugger-ui.css").toExternalForm()
+                    getClass().getResource("debugger-ui.css").toExternalForm(),
+                    DockNode.class.getResource("default.css").toExternalForm()
             );
             primaryStage.setTitle(NAME + " (" + VERSION + ") with KeY:" + KEY_VERSION);
             primaryStage.setScene(scene);

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

 package edu.kit.formal.gui.controller;
 
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
+import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.proof.init.ProofInputException;
 import de.uka.ilkd.key.speclang.Contract;
 import edu.kit.formal.gui.controls.*;
@@ -10,16 +12,18 @@ import edu.kit.formal.interpreter.KeYProofFacade;
 import edu.kit.formal.interpreter.data.KeyData;
 import edu.kit.formal.interpreter.graphs.PTreeNode;
 import edu.kit.formal.interpreter.graphs.ProofTreeController;
-import edu.kit.formal.proofscriptparser.Facade;
 import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import javafx.beans.property.SimpleBooleanProperty;
 import javafx.beans.value.ObservableBooleanValue;
+import javafx.collections.FXCollections;
+import javafx.collections.ObservableList;
 import javafx.concurrent.Service;
 import javafx.concurrent.Task;
 import javafx.event.ActionEvent;
 import javafx.fxml.FXML;
 import javafx.fxml.Initializable;
 import javafx.scene.control.*;
+import javafx.scene.image.Image;
 import javafx.scene.layout.GridPane;
 import javafx.scene.layout.Pane;
 import javafx.scene.layout.Priority;
@@ -28,6 +32,10 @@ import org.antlr.v4.runtime.RecognitionException;
 import org.apache.commons.io.FileUtils;
 import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
+import org.dockfx.DockNode;
+import org.dockfx.DockPane;
+import org.dockfx.DockPos;
+import org.dockfx.demo.DockFX;
 
 import java.io.File;
 import java.io.IOException;
@@ -48,20 +56,23 @@ import java.util.concurrent.Executors;
  */
 public class DebuggerMainWindowController implements Initializable {
     private static final Logger LOGGER = LogManager.getLogger(DebuggerMainWindowController.class);
-
     private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
 
 
     @FXML
     private Pane rootPane;
+
     @FXML
-    private SplitPane splitPane;
+    private DockPane dockStation;
+
+    //@FXML
+    //private SplitPane splitPane;
     /***********************************************************************************************************
      *      Code Area
      * **********************************************************************************************************/
 
-    @FXML
-    private ScriptTabPane tabPane;
+    //@FXML
+    private ScriptController scriptController;
 
     /***********************************************************************************************************
      *      MenuBar
@@ -142,6 +153,12 @@ public class DebuggerMainWindowController implements Initializable {
         alert.showAndWait();
     }
 
+    private ObservableList<ScriptArea> openScripts = FXCollections.observableArrayList();
+    private WelcomePane welcomePane = new WelcomePane();
+    private DockNode welcomePaneDock = new DockNode(welcomePane,"Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
+
+
+
     /**
      * @param location
      * @param resources
@@ -149,8 +166,23 @@ public class DebuggerMainWindowController implements Initializable {
     @Override
     public void initialize(URL location, ResourceBundle resources) {
         setDebugMode(false);
+        scriptController = new ScriptController(dockStation);
+
+        Image dockImage = new Image(DockFX.class.getResource("docknode.png").toExternalForm());
+        welcomePaneDock.dock(dockStation, DockPos.LEFT);
+
+        /*
+        DockNode scripts = AnchorageSystem.createDock("Scripts", scriptController);
+        DockNode a = AnchorageSystem.createDock("Abc", new ScriptArea());
+        DockNode b = AnchorageSystem.createDock("Def", new ScriptArea());
 
-        toolbar.getChildrenUnmodifiable().forEach(
+        scripts.dock(dockStation, DockNode.DockPosition.CENTER);
+        a.dock(dockStation, DockNode.DockPosition.LEFT);
+        b.dock(dockStation, DockNode.DockPosition.LEFT);
+        */
+
+
+/*        toolbar.getChildrenUnmodifiable().forEach(
                 n -> n.setOnMouseEntered(statusBar.getTooltipHandler()));
 
         buttonStartInterpreter.setOnMouseEntered(statusBar.getTooltipHandler());
@@ -162,11 +194,11 @@ public class DebuggerMainWindowController implements Initializable {
         /**
          * create a new inspectionviewtab that is the main tab and not closable
          */
-        inspectionViewTabPane.createNewInspectionViewTab(model, true);
+      //  inspectionViewTabPane.createNewInspectionViewTab(model, true);
 
 
         //TODO this does not work any more
-        /*tabPane.getActiveScriptAreaTab().getScriptArea().getMarkedLines().addListener((SetChangeListener<Integer>) change -> {
+        /*scriptController.getActiveScriptAreaTab().getScriptArea().getMarkedRegions().addListener((SetChangeListener<Integer>) change -> {
             blocker.getBreakpoints().clear();
             blocker.getBreakpoints().addAll(change.getSet());
         });*/
@@ -178,7 +210,7 @@ public class DebuggerMainWindowController implements Initializable {
 
         //model.currentGoalNodesProperty().bind(pc.currentGoalsProperty());
 
-        CustomTabPaneSkin skin = new CustomTabPaneSkin(tabPane);
+        //CustomTabPaneSkin skin = new CustomTabPaneSkin(scriptController);
 
     }
 
@@ -197,7 +229,7 @@ public class DebuggerMainWindowController implements Initializable {
 //        int line = lm.getLine(scriptArea.getCaretPosition());
 //        int inLine = lm.getCharInLine(scriptArea.getCaretPosition());
 //*/
-//        ib.ignoreLinesUntil(tabPane.getSelectedScriptArea().getCaretPosition());
+//        ib.ignoreLinesUntil(scriptController.getSelectedScriptArea().getCaretPosition());
 //        executeScript(ib, true);
     }
 
@@ -217,7 +249,7 @@ public class DebuggerMainWindowController implements Initializable {
         this.debugMode.set(debugMode);
         statusBar.publishMessage("Parse ...");
         try {
-            List<ProofScript> scripts = Facade.getAST(tabPane.getSelectedScriptArea().getText());
+            List<ProofScript> scripts = scriptController.getCombinedAST();
             statusBar.publishMessage("Creating new Interpreter instance ...");
             ib.setScripts(scripts);
 
@@ -235,18 +267,11 @@ public class DebuggerMainWindowController implements Initializable {
                 model.setCurrentGoalNodes(newValue);
             });
 
-            pc.startHighlightPositionPropertyProperty().addListener((observable, oldValue, newValue) -> {
-                if (newValue.getLineNumber() > -1) {
-                    tabPane.getSelectedScriptArea().highlightStmt(newValue.getLineNumber(), "line-highlight-postmortem");
-                }
-                if (oldValue.getLineNumber() > -1) {
-                    tabPane.getSelectedScriptArea().removeHighlightStmt(oldValue.getLineNumber());
-                }
-
-
+            pc.currentHighlightNodeProperty().addListener((observable, oldValue, newValue) -> {
+                scriptController.getPostMortemHighlighter().highlight(newValue);
             });
             //highlight signature of main script
-            tabPane.getSelectedScriptArea().setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
+            //scriptController.setDebugMark(scripts.get(0).getStartPosition().getLineNumber());
         } catch (RecognitionException e) {
             showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
         }
@@ -278,7 +303,7 @@ public class DebuggerMainWindowController implements Initializable {
 
     private void saveScript(File scriptFile) {
         try {
-            FileUtils.write(scriptFile, tabPane.getSelectedScriptArea().getText(), Charset.defaultCharset());
+            scriptController.saveCurrentScriptAs(scriptFile);
         } catch (IOException e) {
             showExceptionDialog("Could not save sourceName", "blubb", "...fsfsfsf fsa", e);
         }
@@ -296,7 +321,7 @@ public class DebuggerMainWindowController implements Initializable {
         assert scriptFile != null;
         try {
             String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset());
-            ScriptArea area = tabPane.createNewTab(scriptFile);
+            ScriptArea area = scriptController.createNewTab(scriptFile);
             openScript(code, area);
             model.setScriptFile(scriptFile);
         } catch (IOException e) {
@@ -432,10 +457,14 @@ public class DebuggerMainWindowController implements Initializable {
     public void stopDebugMode(ActionEvent actionEvent) {
 
         //linenumberMainscript from model?
-        //tabPane.getActiveScriptAreaTab().getScriptArea().removeHighlightStmt(lineNumberMainScript);
+        //scriptController.getActiveScriptAreaTab().getScriptArea().removeHighlightStmt(lineNumberMainScript);
         //inspectionViewTabPane.getInspectionViewTab.clear();
     }
 
+    public void newScript(ActionEvent actionEvent) {
+        scriptController.newScript();
+    }
+
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected Task<List<Contract>> createTask() {

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

 package edu.kit.formal.gui.controls;
 
-import com.sun.org.apache.xpath.internal.operations.Mod;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.logic.op.IProgramMethod;
@@ -19,8 +18,8 @@ import javafx.scene.Node;
 import javafx.scene.control.ListCell;
 import javafx.scene.control.ListView;
 import javafx.scene.control.SplitPane;
-import javafx.scene.control.Tab;
 import javafx.scene.input.MouseEvent;
+import javafx.scene.layout.BorderPane;
 
 import java.io.IOException;
 import java.io.StringWriter;
@@ -30,7 +29,7 @@ import java.io.StringWriter;
  *
  * @author S. Grebing
  */
-public class InspectionViewTab extends Tab {
+public class InspectionViewTab extends BorderPane {
     public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
     @FXML
     private SectionPane sectionPaneJavaCode;

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

 package edu.kit.formal.gui.controls;
 
 import edu.kit.formal.gui.model.RootModel;
-import javafx.fxml.FXML;
-import javafx.scene.control.TabPane;
+import org.dockfx.DockNode;
 
 /**
  * TabPane on the right side of the GUI containing the inspection view as tabs
  */
-public class InspectionViewTabPane extends TabPane {
+public class InspectionViewTabPane {
 
     /**
      * active tab in which the interpreter resp. Debugger state is shown.
      * 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 InspectionViewTab activeInterpreterTab;
-
-
-    @FXML
-    private InspectionViewTab inspectionViewTab;
-
-    public InspectionViewTabPane() {
-        super();
-        Utils.createWithFXML(this);
-    }
-
-
-    public void setActiveInterpreterTab(InspectionViewTab activeInterpreterTab) {
-        this.activeInterpreterTab = activeInterpreterTab;
-    }
+    private final InspectionViewTab activeInterpreterTab = new InspectionViewTab();
+    private final DockNode activeInterpreterTabDock = new DockNode(activeInterpreterTab, "Active");
 
     public InspectionViewTab getActiveInspectionViewTab() {
         return this.activeInterpreterTab;
@@ -61,8 +47,8 @@ public class InspectionViewTabPane extends TabPane {
             getActiveInspectionViewTab().getGoalView().getSelectionModel().select(fresh);
 
             /* TODO get lines of active statements marked lines
-            javaSourceCode.getMarkedLines().clear();
-            javaSourceCode.getMarkedLines().addAll(
+            javaSourceCode.getMarkedRegions().clear();
+            javaSourceCode.getMarkedRegions().addAll(
             );*/
         });
 

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

@@ -9,11 +9,13 @@ import edu.kit.formal.proofscriptparser.ScriptLanguageLexer;
 import edu.kit.formal.proofscriptparser.ast.ProofScript;
 import edu.kit.formal.proofscriptparser.lint.LintProblem;
 import edu.kit.formal.proofscriptparser.lint.LinterStrategy;
+import javafx.beans.InvalidationListener;
 import javafx.beans.Observable;
 import javafx.beans.binding.BooleanBinding;
 import javafx.beans.property.*;
 import javafx.collections.FXCollections;
 import javafx.collections.ObservableList;
+import javafx.collections.ObservableSet;
 import javafx.event.ActionEvent;
 import javafx.fxml.FXML;
 import javafx.geometry.Insets;
@@ -27,6 +29,8 @@ import javafx.scene.paint.Color;
 import javafx.scene.paint.Paint;
 import javafx.scene.text.Font;
 import javafx.scene.text.FontPosture;
+import lombok.Data;
+import lombok.RequiredArgsConstructor;
 import org.antlr.v4.runtime.CharStream;
 import org.antlr.v4.runtime.CharStreams;
 import org.antlr.v4.runtime.Token;
@@ -35,9 +39,7 @@ import org.fxmisc.richtext.CharacterHit;
 import org.fxmisc.richtext.CodeArea;
 import org.fxmisc.richtext.MouseOverTextEvent;
 import org.fxmisc.richtext.model.NavigationActions;
-import org.fxmisc.richtext.model.Paragraph;
 import org.fxmisc.richtext.model.StyleSpans;
-import org.fxmisc.richtext.model.StyledText;
 import org.reactfx.collection.LiveList;
 import org.reactfx.value.Val;
 
@@ -52,13 +54,16 @@ import java.util.function.IntFunction;
  */
 public class ScriptArea extends CodeArea {
     private final ObjectProperty<File> filePath = new SimpleObjectProperty<>();
+
+    private final BooleanProperty dirty = new SimpleBooleanProperty(this, "dirty", false);
+
     /**
      * Lines to highlight?
      */
-    private final SetProperty<Integer> markedLines =
+    private final SetProperty<RegionStyle> markedRegions =
             new SimpleSetProperty<>(FXCollections.observableSet());
     /**
-     * set by {@link ScriptTabPane}
+     * set by {@link ScriptController}
      */
     private final ObjectProperty<MainScriptIdentifier> mainScript = new SimpleObjectProperty<>();
 
@@ -82,15 +87,14 @@ public class ScriptArea extends CodeArea {
         //getStylesheets().add(getClass().getResource("script-keywords.css").toExternalForm());
         getStyleClass().add("script-area");
         textProperty().addListener((prop, oldValue, newValue) -> {
-            if (newValue.length() != 0) {
-                clearStyle(0, newValue.length());
-                StyleSpans<? extends Collection<String>> spans = highlighter.highlight(newValue);
-                if (spans != null) setStyleSpans(0, spans);
-            }
-            highlightProblems();
-
+            dirty.set(true);
             updateMainScriptMarker();
+            updateHighlight();
+            highlightProblems();
         });
+
+        markedRegions.addListener((InvalidationListener) o -> updateHighlight());
+
                /* .successionEnds(Duration.ofMillis(100))
                 .hook(collectionRichTextChange -> this.getUndoManager().mark())
                 .supplyTask(this::computeHighlightingAsync).awaitLatest(richChanges())
@@ -121,6 +125,19 @@ public class ScriptArea extends CodeArea {
         contextMenu = new ScriptAreaContextMenu();
     }
 
+    private void updateHighlight() {
+        String newValue = getText();
+        if (newValue.length() != 0) {
+            clearStyle(0, newValue.length());
+            StyleSpans<? extends Collection<String>> spans = highlighter.highlight(newValue);
+            if (spans != null) setStyleSpans(0, spans);
+        }
+
+        markedRegions.forEach(reg -> {
+            setStyle(reg.start, reg.stop, Collections.singleton(reg.clazzName));
+        });
+    }
+
     private void updateMainScriptMarker() {
         try {
             MainScriptIdentifier ms = mainScript.get();
@@ -211,49 +228,6 @@ public class ScriptArea extends CodeArea {
         a.setBreakpoint(!a.isBreakpoint());
     }
 
-    /**
-     * Highlight line given by the characterindex
-     *
-     * @param lineNumber
-     */
-    public void highlightStmt(int lineNumber, String cssStyleTag) {
-        //calculate line number from characterindex
-        //int lineNumber = this.offsetToPosition(chrIdx, Bias.Forward).getMajor();
-        Paragraph<Collection<String>, StyledText<Collection<String>>, Collection<String>> paragraph = this.getParagraph(lineNumber);
-        //calculate start and endposition
-        //int startPos = getAbsolutePosition(this.offsetToPosition(chrIdx, Bias.Forward).getMajor(), 0);
-        int startPos = getAbsolutePosition(lineNumber, 0);
-
-        int length = paragraph.length();
-        //highlight line
-
-        this.setStyle(startPos, startPos + length, Collections.singleton(cssStyleTag));
-
-    }
-
-    /**
-     * Remove the highlighting of a statement
-     *
-     * @param lineNumber
-     */
-    public void removeHighlightStmt(int lineNumber) {
-        highlightStmt(lineNumber, "line-unhighlight");
-    }
-
-    /**
-     * Set a mark in the gutter next to the definition of the main script
-     *
-     * @param lineNumberOfSigMainScript
-     */
-    public void setDebugMark(int lineNumberOfSigMainScript) {
-        highlightStmt(lineNumberOfSigMainScript - 1, "line-highlight-mainScript");
-
-    }
-
-    public void unsetDebugMark(int lineNumberOfSigMainScript) {
-        removeHighlightStmt(lineNumberOfSigMainScript - 1);
-    }
-
     public File getFilePath() {
         return filePath.get();
     }
@@ -558,12 +532,45 @@ public class ScriptArea extends CodeArea {
         }
 
         public void showPostMortem(ActionEvent event) {
-            ScriptArea area = ScriptArea.this;
+            //TODO forward to ProofTreeController, it jumps to the node and this should be done via the callbacks.
+
+            /*ScriptArea area = ScriptArea.this;
             int chrIdx = currentMouseOver.get().getCharacterIndex().orElse(0);
             if (chrIdx != 0) {
                 int lineNumber = area.offsetToPosition(chrIdx, Bias.Forward).getMajor();
                 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;
+    }
 }
\ No newline at end of file

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

-package edu.kit.formal.gui.controls;
-
-import edu.kit.formal.gui.model.Breakpoint;
-import edu.kit.formal.gui.model.MainScriptIdentifier;
-import javafx.beans.property.ObjectProperty;
-import javafx.beans.property.SimpleObjectProperty;
-import javafx.scene.control.Tab;
-import javafx.scene.control.TabPane;
-import org.apache.logging.log4j.LogManager;
-import org.apache.logging.log4j.Logger;
-
-import java.io.File;
-import java.util.HashSet;
-import java.util.Set;
-
-/**
- * Controller for TabPane
- *
- * @author Sarah Grebing
- */
-public class ScriptTabPane extends TabPane {
-    private static Logger logger = LogManager.getLogger(ScriptTabPane.class);
-    private ObjectProperty<MainScriptIdentifier> mainScript = new SimpleObjectProperty<>();
-
-    public ScriptTabPane() {
-        Utils.createWithFXML(this);
-    }
-
-    /**
-     * Create a new tab with the specified title
-     *
-     * @param
-     */
-    public ScriptArea createNewTab(String filePath) {
-        return createNewTab(new File(filePath));
-    }
-
-    public ScriptArea createNewTab(File filePath) {
-        filePath = filePath.getAbsoluteFile();
-        if (findTabForFile(filePath) == null) {
-            Tab newTab = new Tab(filePath.getName());
-            ScriptArea area = new ScriptArea();
-            newTab.setContent(area);