Skip to content

GitLab

P
ProofScriptParser
Commit ca4ce23b authored by Alexander Weigl's avatar Alexander Weigl
Browse files
Options

docking framework seems good

parent f581dea7
Pipeline #11951 failed with stage
    in 1 minute and 23 seconds
    Hide whitespace changes
    Inline Side-by-side
    Showing with 257 additions and 264 deletions
    DockFX @ bbbc5765
    Compare 80c5e583...bbbc5765
    Subproject commit 80c5e58344850b9ec92c84cb6fb9b56d6a1066f3
    Subproject commit bbbc57653d6a0bc7463539de30fec075443c0843
    pom.xml
    View file @ ca4ce23b
    ......@@ -92,7 +92,6 @@
    </goals>
    <configuration>
    <sources>
    <source>lib/AnchorFX/src/main/java</source>
    <source>lib/DockFX/src/main/java</source>
    </sources>
    </configuration>
    ......@@ -107,7 +106,6 @@
    <configuration>
    <resources>
    <resource>
    <directory>lib/AnchorFX/src/main/resources</directory>
    <directory>lib/DockFX/src/main/resources</directory>
    </resource>
    </resources>
    ......
    src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java
    View file @ ca4ce23b
    ......@@ -15,8 +15,6 @@ import edu.kit.formal.interpreter.graphs.ProofTreeController;
    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;
    ......@@ -96,8 +94,17 @@ public class DebuggerMainWindowController implements Initializable {
    * GoalView
    * **********************************************************************************************************/
    @FXML
    private InspectionViewTabPane inspectionViewTabPane;
    private final InspectionViewsController inspectionViewsController = new InspectionViewsController();
    /**
    *
    */
    private JavaArea javaArea = new JavaArea();
    private DockNode javaAreaDock = new DockNode(javaArea, "Java Source",
    new MaterialDesignIconView(MaterialDesignIcon.CODEPEN)
    );
    private ExecutorService executorService = Executors.newFixedThreadPool(2);
    private KeYProofFacade facade = new KeYProofFacade();
    private ContractLoaderService contractLoaderService = new ContractLoaderService();
    ......@@ -122,6 +129,10 @@ public class DebuggerMainWindowController implements Initializable {
    //TODO
    private ObservableBooleanValue executeNotPossible = pc.executeNotPossibleProperty().or(facade.readyToExecuteProperty().not());
    private WelcomePane welcomePane = new WelcomePane(this);
    private DockNode welcomePaneDock = new DockNode(welcomePane, "Welcome", new MaterialDesignIconView(MaterialDesignIcon.ACCOUNT));
    private DockNode activeInspectorDock = inspectionViewsController.getActiveInterpreterTabDock();
    public static void showExceptionDialog(String title, String headerText, String contentText, Throwable ex) {
    Alert alert = new Alert(Alert.AlertType.ERROR);
    ......@@ -153,12 +164,6 @@ 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
    ......@@ -172,20 +177,10 @@ public class DebuggerMainWindowController implements Initializable {
    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());
    scripts.dock(dockStation, DockNode.DockPosition.CENTER);
    a.dock(dockStation, DockNode.DockPosition.LEFT);
    b.dock(dockStation, DockNode.DockPosition.LEFT);
    */
    /* toolbar.getChildrenUnmodifiable().forEach(
    toolbar.getChildrenUnmodifiable().forEach(
    n -> n.setOnMouseEntered(statusBar.getTooltipHandler()));
    buttonStartInterpreter.setOnMouseEntered(statusBar.getTooltipHandler());
    */
    model.scriptFileProperty().addListener((observable, oldValue, newValue) -> {
    statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a"));
    ......@@ -194,24 +189,15 @@ public class DebuggerMainWindowController implements Initializable {
    /**
    * create a new inspectionviewtab that is the main tab and not closable
    */
    // inspectionViewTabPane.createNewInspectionViewTab(model, true);
    inspectionViewsController.connectActiveView(model);
    //TODO this does not work any more
    /*scriptController.getActiveScriptAreaTab().getScriptArea().getMarkedRegions().addListener((SetChangeListener<Integer>) change -> {
    blocker.getBreakpoints().clear();
    blocker.getBreakpoints().addAll(change.getSet());
    });*/
    /*pc.currentGoalsProperty().addListener((o, old, fresh) -> {
    /*pc.goalsProperty().addListener((o, old, fresh) -> {
    model.currentGoalNodesProperty().setAll(fresh);
    });
    model.currentSelectedGoalNodeProperty().bind(pc.currentSelectedGoalProperty());*/
    //model.currentGoalNodesProperty().bind(pc.currentGoalsProperty());
    //model.currentGoalNodesProperty().bind(pc.goalsProperty());
    //CustomTabPaneSkin skin = new CustomTabPaneSkin(scriptController);
    }
    //region Actions: Execution
    ......@@ -330,7 +316,7 @@ public class DebuggerMainWindowController implements Initializable {
    }
    }
    private void openScript(String code, ScriptArea area) {
    public void openScript(String code, ScriptArea area) {
    model.setScriptFile(null);
    if (!area.textProperty().getValue().isEmpty()) {
    area.deleteText(0, area.textProperty().getValue().length());
    ......@@ -342,8 +328,12 @@ public class DebuggerMainWindowController implements Initializable {
    @FXML
    protected void loadKeYFile() {
    File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "script");
    this.model.setKeYFile(keyFile);
    openKeyFile(keyFile);
    }
    public void openKeyFile(File keyFile) {
    if (keyFile != null) {
    this.model.setKeYFile(keyFile);
    Task<Void> task = facade.loadKeyFileTask(keyFile);
    task.setOnSucceeded(event -> {
    statusBar.publishMessage("Loaded key sourceName: %s", keyFile);
    ......@@ -373,6 +363,10 @@ public class DebuggerMainWindowController implements Initializable {
    @FXML
    protected void loadJavaFile() {
    File javaFile = openFileChooserOpenDialog("Select Java File", "Java Files", "java");
    openJavaFile(javaFile);
    }
    public void openJavaFile(File javaFile) {
    if (javaFile != null) {
    model.setJavaFile(javaFile);
    contractLoaderService.start();
    ......@@ -389,7 +383,7 @@ public class DebuggerMainWindowController implements Initializable {
    */
    private File openFileChooserSaveDialog(String title, String description, String... fileEndings) {
    FileChooser fileChooser = getFileChooser(title, description, fileEndings);
    // File sourceName = fileChooser.showSaveDialog(inspectionViewTabPane.getInspectionViewTab().getGoalView().getScene().getWindow());
    // File sourceName = fileChooser.showSaveDialog(inspectionViewsController.getInspectionViewTab().getGoalView().getScene().getWindow());
    File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow());
    if (file != null) initialDirectory = file.getParentFile();
    return file;
    ......@@ -397,7 +391,7 @@ public class DebuggerMainWindowController implements Initializable {
    private File openFileChooserOpenDialog(String title, String description, String... fileEndings) {
    FileChooser fileChooser = getFileChooser(title, description, fileEndings);
    //File sourceName = fileChooser.showOpenDialog(inspectionViewTabPane.getInspectionViewTab().getGoalView().getScene().getWindow());
    //File sourceName = fileChooser.showOpenDialog(inspectionViewsController.getInspectionViewTab().getGoalView().getScene().getWindow());
    File file = fileChooser.showOpenDialog(statusBar.getScene().getWindow());
    if (file != null) initialDirectory = file.getParentFile();
    return file;
    ......@@ -458,13 +452,44 @@ public class DebuggerMainWindowController implements Initializable {
    //linenumberMainscript from model?
    //scriptController.getActiveScriptAreaTab().getScriptArea().removeHighlightStmt(lineNumberMainScript);
    //inspectionViewTabPane.getInspectionViewTab.clear();
    //inspectionViewsController.getInspectionViewTab.clear();
    }
    public void newScript(ActionEvent actionEvent) {
    scriptController.newScript();
    }
    public void showCodeDock(ActionEvent actionEvent) {
    if (!javaAreaDock.isDocked()) {
    javaAreaDock.dock(dockStation, DockPos.RIGHT);
    }
    }
    public void showWelcomeDock(ActionEvent actionEvent) {
    if (!welcomePaneDock.isDocked()) {
    welcomePaneDock.dock(dockStation, DockPos.CENTER);
    }
    }
    public void showActiveInspector(ActionEvent actionEvent) {
    if (!activeInspectorDock.isDocked() &&
    !activeInspectorDock.isFloating()) {
    activeInspectorDock.dock(dockStation, DockPos.CENTER);
    }
    }
    public DockNode getJavaAreaDock() {
    return javaAreaDock;
    }
    public DockNode getWelcomePaneDock() {
    return welcomePaneDock;
    }
    public DockNode getActiveInspectorDock() {
    return activeInspectorDock;
    }
    public class ContractLoaderService extends Service<List<Contract>> {
    @Override
    protected Task<List<Contract>> createTask() {
    ......
    src/main/java/edu/kit/formal/gui/controls/InspectionViewTab.java
    View file @ ca4ce23b
    package edu.kit.formal.gui.controls;
    import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
    import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
    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.beans.Observable;
    import javafx.beans.property.BooleanProperty;
    import javafx.beans.property.ObjectProperty;
    import javafx.beans.property.SimpleBooleanProperty;
    import javafx.beans.property.ReadOnlyObjectProperty;
    import javafx.beans.property.SimpleObjectProperty;
    import javafx.fxml.FXML;
    import javafx.scene.Node;
    ......@@ -21,9 +16,6 @@ import javafx.scene.control.SplitPane;
    import javafx.scene.input.MouseEvent;
    import javafx.scene.layout.BorderPane;
    import java.io.IOException;
    import java.io.StringWriter;
    /**
    * Right part of the splitpane that displays the different parts of a state
    *
    ......@@ -31,32 +23,43 @@ import java.io.StringWriter;
    */
    public class InspectionViewTab extends BorderPane {
    public GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
    @FXML
    private SectionPane sectionPaneJavaCode;
    @FXML
    private SplitPane lowerSplitPane;
    @FXML
    private SequentView sequentView;
    @FXML
    private JavaArea javaSourceCode;
    @FXML
    private ListView goalView;
    private ObjectProperty<Mode> mode = new SimpleObjectProperty<>();
    @FXML
    private ListView<GoalNode<KeyData>> goalView;
    private BooleanProperty showCode = new SimpleBooleanProperty(true);
    private ObjectProperty<InspectionModel> model = new SimpleObjectProperty<>(
    new InspectionModel()
    );
    public InspectionViewTab() {
    super();
    Utils.createWithFXML(this);
    getGoalView().getSelectionModel().selectedItemProperty().addListener((observable, oldValue, newValue) -> {
    if (newValue != null && newValue.getData() != null) {
    getSequentView().setNode(newValue.getData().getNode());
    }
    });
    model.get().selectedGoalNodeToShowProperty().bind(
    goalView.getSelectionModel().selectedItemProperty()
    );
    model.get().selectedGoalNodeToShowProperty().addListener(
    (observable, oldValue, newValue) -> {
    goalView.getSelectionModel().select(newValue);
    if (newValue != null && newValue.getData() != null) {
    getSequentView().setNode(newValue.getData().getNode());
    // TODO weigl: get marked lines of the program, and set it
    model.get().highlightedJavaLinesProperty().get()
    .clear();
    }
    });
    model.get().goalsProperty().bindBidirectional(goalView.itemsProperty());
    getGoalView().setCellFactory(GoalNodeListCell::new);
    /*TODO redefine CSS bases on selected mode
    mode.addListener(o -> {
    getStyleClass().removeAll(
    Mode.DEAD.name(),
    ......@@ -64,34 +67,14 @@ public class InspectionViewTab extends BorderPane {
    Mode.POSTMORTEM.name()
    );
    getStyleClass().add(mode.get().name());
    if (mode.get() == Mode.LIVING) {
    MaterialDesignIconView icon = new MaterialDesignIconView(MaterialDesignIcon.RUN);
    setClosable(false);
    setGraphic(icon);
    } else {
    setGraphic(null);
    setClosable(true);
    }
    });
    showCode.addListener(o -> {
    if (showCode.get())
    lowerSplitPane.getItems().add(sectionPaneJavaCode);
    else
    lowerSplitPane.getItems().remove(sectionPaneJavaCode);
    });
    showCode.set(false);
    */
    }
    public SequentView getSequentView() {
    return sequentView;
    }
    public JavaArea getJavaSourceCode() {
    return javaSourceCode;
    }
    public ListView<GoalNode<KeyData>> getGoalView() {
    return goalView;
    ......@@ -106,16 +89,8 @@ public class InspectionViewTab extends BorderPane {
    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();
    /* IProgramMethod method = (IProgramMethod) model.getChosenContract().getTarget();
    StringWriter writer = new StringWriter();
    ProgramPrinter pp = new ProgramPrinter(writer);
    try {
    ......@@ -125,39 +100,10 @@ public class InspectionViewTab extends BorderPane {
    } catch (IOException e) {
    e.printStackTrace();
    }
    getJavaSourceCode().insertText(0, writer.toString());
    // javaSourceCode.insertText(0, writer.toString());
    */
    }
    public Mode getMode() {
    return mode.get();
    }
    public void setMode(Mode mode) {
    this.mode.set(mode);
    }
    public ObjectProperty<Mode> modeProperty() {
    return mode;
    }
    public boolean isShowCode() {
    return showCode.get();
    }
    public void setShowCode(boolean showCode) {
    this.showCode.set(showCode);
    }
    public BooleanProperty showCodeProperty() {
    return showCode;
    }
    enum Mode {
    LIVING, DEAD, POSTMORTEM,
    }
    /**
    * Cells for GoalView
    */
    ......@@ -181,4 +127,12 @@ public class InspectionViewTab extends BorderPane {
    setText(text);
    }
    }
    public InspectionModel getModel() {
    return model.get();
    }
    public ReadOnlyObjectProperty<InspectionModel> modelProperty() {
    return model;
    }
    }
    src/main/java/edu/kit/formal/gui/controls/InspectionViewTabPane.java → src/main/java/edu/kit/formal/gui/controls/InspectionViewsController.java
    View file @ ca4ce23b
    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
    */
    public class InspectionViewTabPane {
    public class InspectionViewsController {
    /**
    * active tab in which the interpreter resp. Debugger state is shown.
    ......@@ -16,40 +19,19 @@ public class InspectionViewTabPane {
    private final InspectionViewTab activeInterpreterTab = new InspectionViewTab();
    private final DockNode activeInterpreterTabDock = new DockNode(activeInterpreterTab, "Active");
    private final ObservableMap<InspectionViewTab, DockNode> inspectionViews = new SimpleMapProperty<>(FXCollections.observableHashMap());
    public InspectionViewTab getActiveInspectionViewTab() {
    return this.activeInterpreterTab;
    }
    public void createNewInspectionViewTab(RootModel model, boolean activeTab) {
    InspectionViewTab tab = new InspectionViewTab();
    if (activeTab) {
    System.out.println(this.getActiveInspectionViewTab() == null);
    this.setActiveInterpreterTab(tab);
    tab.setText("Active Tab");
    tab.setClosable(false);
    this.setActiveInterpreterTab(tab);
    }
    model.chosenContractProperty().addListener(o -> {
    tab.refresh(model);
    });
    bindGoalNodesWithCurrentTab(model);
    this.getTabs().add(tab);
    public DockNode getActiveInterpreterTabDock() {
    return activeInterpreterTabDock;
    }
    //TODO schauen wie Goallist ins model kommt
    public void bindGoalNodesWithCurrentTab(RootModel model) {
    public void connectActiveView(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.getMarkedRegions().clear();
    javaSourceCode.getMarkedRegions().addAll(
    );*/
    });
    }
    ......
    src/main/java/edu/kit/formal/gui/controls/ScriptController.java
    View file @ ca4ce23b
    ......@@ -67,8 +67,6 @@ public class ScriptController {
    area.setFilePath(filePath);
    DockNode dockNode = createDockNode(area);
    openScripts.put(area, dockNode);
    dockNode.dock(parent, DockPos.LEFT);
    return area;
    } else {
    logger.info("File already exists. Will not load it again");
    ......
    src/main/java/edu/kit/formal/gui/controls/WelcomePane.java
    View file @ ca4ce23b
    package edu.kit.formal.gui.controls;
    import edu.kit.formal.gui.controller.DebuggerMainWindowController;
    import javafx.scene.layout.AnchorPane;
    import java.awt.event.ActionEvent;
    import java.io.File;
    /**
    * Created by weigl on 7/7/17.
    */
    public class WelcomePane extends AnchorPane {
    private final DebuggerMainWindowController proofScriptDebugger;
    public WelcomePane() {
    public WelcomePane(DebuggerMainWindowController debugger) {
    this.proofScriptDebugger = debugger;
    Utils.createWithFXML(this);
    }
    public void loadContraPosition(javafx.event.ActionEvent event) {
    proofScriptDebugger.getWelcomePaneDock().close();
    proofScriptDebugger.showActiveInspector(null);
    proofScriptDebugger.openScript(
    new File("src/test/resources/edu/kit/formal/interpreter/contraposition/test.kps")
    );
    proofScriptDebugger.openKeyFile(
    new File("src/test/resources/edu/kit/formal/interpreter/contraposition/contraposition.key"));
    }
    }
    src/main/java/edu/kit/formal/gui/model/InspectionModel.java
    View file @ ca4ce23b
    package edu.kit.formal.gui.model;
    import edu.kit.formal.interpreter.data.GoalNode;
    import edu.kit.formal.interpreter.data.KeyData;
    import edu.kit.formal.proofscriptparser.ast.ASTNode;
    import javafx.beans.property.SimpleListProperty;
    import javafx.beans.property.SimpleObjectProperty;
    import javafx.beans.property.*;
    import javafx.collections.FXCollections;
    import javafx.collections.ObservableList;
    import javafx.collections.ObservableMap;
    import javafx.collections.ObservableSet;
    import javafx.scene.paint.Color;
    import java.util.Map;
    import java.util.Set;
    /**
    * Model for the inspection view
    *
    * @author S.Grebing
    * @author Alexander Weigl
    */
    public class InspectionModel {
    enum Mode {
    LIVING, DEAD, POSTMORTEM,
    }
    private ASTNode node;
    private SimpleListProperty<GoalNode> currentGoals;
    private SimpleObjectProperty<GoalNode> selectedGoalNodeToShow;
    private Map<GoalNode, Color> colorofEachGoalNodeinListView;
    private boolean showJavaView;
    private String javaString;
    private Set<Integer> highlightedJavaLines;
    private boolean closable;
    private boolean isInterpreterTab;
    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 MapProperty<GoalNode, Color> colorofEachGoalNodeinListView = new SimpleMapProperty<>(FXCollections.observableHashMap());
    //private final StringProperty javaString = new SimpleStringProperty();
    private final SetProperty<Integer> highlightedJavaLines = new SimpleSetProperty<>(FXCollections.observableSet());
    private final BooleanProperty closable = new SimpleBooleanProperty();
    private final BooleanProperty isInterpreterTab = new SimpleBooleanProperty();
    private ObjectProperty<Mode> mode = new SimpleObjectProperty<>();
    public InspectionModel() {
    public ASTNode getNode() {
    return node.get();
    }
    /***************************************************************************************************************
    * Getter and Setter
    *
    ***************************************************************************************************************/
    public ASTNode getNode() {
    public ObjectProperty<ASTNode> nodeProperty() {
    return node;
    }
    public void setNode(ASTNode node) {
    this.node = node;
    this.node.set(node);
    }
    public ObservableList<GoalNode> getCurrentGoals() {
    return currentGoals.get();
    public ObservableList<GoalNode<KeyData>> getGoals() {
    return goals.get();
    }
    public void setCurrentGoals(ObservableList<GoalNode> currentGoals) {
    this.currentGoals.set(currentGoals);
    public ListProperty<GoalNode<KeyData>> goalsProperty() {
    return goals;
    }
    public SimpleListProperty<GoalNode> currentGoalsProperty() {
    return currentGoals;
    public void setGoals(ObservableList<GoalNode<KeyData>> goals) {
    this.goals.set(goals);
    }
    public GoalNode getSelectedGoalNodeToShow() {
    return selectedGoalNodeToShow.get();
    }
    public ObjectProperty<GoalNode<KeyData>> selectedGoalNodeToShowProperty() {
    return selectedGoalNodeToShow;
    }
    public void setSelectedGoalNodeToShow(GoalNode selectedGoalNodeToShow) {