ProofTree context menu, clean up welcome page

keydeps/pom.xml

@@ -13,18 +13,6 @@
     <packaging>jar</packaging>
     <version>1.0</version>
 
-    <repositories>
-        <repository>
-            <id>local-repo</id>
-            <name>local-repo</name>
-            <url>file:///${basedir}/local-repo</url>
-            <snapshots>
-                <enabled>true</enabled>
-                <updatePolicy>always</updatePolicy>
-                <checksumPolicy>ignore</checksumPolicy>
-            </snapshots>
-        </repository>
-    </repositories>
 
     <dependencies>
         <dependency>
@@ -66,6 +54,7 @@
 
     <build>
         <plugins>
+            <!--
             <plugin>
                 <groupId>org.codehaus.mojo</groupId>
                 <artifactId>exec-maven-plugin</artifactId>
@@ -80,17 +69,18 @@
                 </executions>
                 <configuration>
                     <workingDirectory>${basedir}/../</workingDirectory>
-                    <!--                 <arguments>
+                                     <arguments>
                                 <systemProperties>
                                     <systemProperty>
                                         <key>java.security.policy</key>
                                         <value>policy</value>
                                     </systemProperty>
                                 </systemProperties>
-                            </arguments>-->
+                            </arguments>
                     <mainClass>GenDoc</mainClass>
                 </configuration>
             </plugin>
+            -->
         </plugins>
     </build>
 

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/DebuggerMain.java

 package edu.kit.iti.formal.psdbg.gui.controller;
 
+import com.google.common.eventbus.Subscribe;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIcon;
 import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView;
 import de.uka.ilkd.key.api.ProofApi;
@@ -17,7 +18,9 @@ import edu.kit.iti.formal.psdbg.gui.model.InterpreterThreadState;
 import edu.kit.iti.formal.psdbg.interpreter.InterpreterBuilder;
 import edu.kit.iti.formal.psdbg.interpreter.KeYProofFacade;
 import edu.kit.iti.formal.psdbg.interpreter.KeyInterpreter;
+import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.*;
 import edu.kit.iti.formal.psdbg.parser.ast.ProofScript;
 import javafx.application.Platform;
@@ -142,6 +145,29 @@ public class DebuggerMain implements Initializable {
 
     private Timer interpreterThreadTimer;
 
+    @Subscribe
+    public void handle(Events.PublishMessage message) {
+        if (message.getFlash() == 0)
+            statusBar.publishMessage(message.getMessage());
+        else if (message.getFlash() == 1)
+            statusBar.publishSuccessMessage(message.getMessage());
+        else
+            statusBar.publishErrorMessage(message.getMessage());
+    }
+
+    @Subscribe
+    public void handle(Events.SelectNodeInGoalList evt) {
+        InspectionModel im = getInspectionViewsController().getActiveInspectionViewTab().getModel();
+        for (GoalNode<KeyData> gn : im.getGoals()) {
+            if (gn.getData().getNode().equals(evt.getNode())) {
+                im.setSelectedGoalNodeToShow(gn);
+                return;
+            }
+        }
+
+        statusBar.publishErrorMessage("Node not present in Goal List");
+    }
+
     @Override
     public void initialize(URL location, ResourceBundle resources) {
         Events.register(this);
@@ -208,7 +234,6 @@ public class DebuggerMain implements Initializable {
         renewThreadStateTimer();
     }
 
-
     /**
      * If the mouse moves other toolbar button, the help text should display in the status bar
      */
@@ -236,21 +261,8 @@ public class DebuggerMain implements Initializable {
      * @see {@link #handleStatePointer(PTreeNode)}
      */
     private void handleStatePointerUI(PTreeNode<KeyData> node) {
-        InspectionModel im = getInspectionViewsController().getActiveInspectionViewTab().getModel();
-
-        im.getGoals().setAll(
-                node.getStateBeforeStmt().getGoals()
-        );
-        im.setSelectedGoalNodeToShow(
-                node.getStateBeforeStmt().getSelectedGoalNode());
-
+        getInspectionViewsController().getActiveInspectionViewTab().activate(node, node.getStateBeforeStmt());
         scriptController.getDebugPositionHighlighter().highlight(node.getStatement());
-
-        //Experimental
-        ComboBox<PTreeNode<KeyData>> frames = getInspectionViewsController().getActiveInspectionViewTab().getFrames();
-        List<PTreeNode<KeyData>> ctxn = node.getContextNodes();
-        frames.getItems().setAll(ctxn);
-        frames.getSelectionModel().select(node);
     }
 
     private void marriageJavaCode() {
@@ -458,7 +470,11 @@ public class DebuggerMain implements Initializable {
     private void onInterpreterSucceed(DebuggerFramework<KeyData> keyDataDebuggerFramework) {
         Platform.runLater(() -> {
             scriptController.getDebugPositionHighlighter().remove();
-            statusBar.publishMessage("Interpreter finished.");
+            statusBar.publishSuccessMessage("Interpreter finished.");
+            assert model.getDebuggerFramework() != null;
+            PTreeNode<KeyData> statePointer = model.getDebuggerFramework().getStatePointer();
+            State<KeyData> lastState = statePointer.getStateAfterStmt();
+            getInspectionViewsController().getActiveInspectionViewTab().activate(statePointer, lastState);
         });
     }
 
@@ -588,7 +604,7 @@ public class DebuggerMain implements Initializable {
     }
 
     @FXML
-    protected void loadKeYFile() {
+    public void loadKeYFile() {
         File keyFile = openFileChooserOpenDialog("Select KeY File", "KeY Files", "key", "kps");
         openKeyFile(keyFile);
     }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/Events.java

@@ -2,6 +2,7 @@ package edu.kit.iti.formal.psdbg.gui.controller;
 
 import com.google.common.eventbus.EventBus;
 import de.uka.ilkd.key.logic.PosInOccurrence;
+import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.rule.TacletApp;
 import edu.kit.iti.formal.psdbg.gui.controls.ScriptArea;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
@@ -9,6 +10,7 @@ import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
 import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.parser.ast.ASTNode;
 import edu.kit.iti.formal.psdbg.parser.ast.CallStatement;
+import lombok.AllArgsConstructor;
 import lombok.Data;
 import lombok.RequiredArgsConstructor;
 
@@ -16,7 +18,7 @@ import java.util.List;
 
 /**
  * See http://codingjunkie.net/guava-eventbus/ for an introduction.
- *
+ * <p>
  * Created by weigl on 7/11/17.
  */
 public class Events {
@@ -45,6 +47,7 @@ public class Events {
     @RequiredArgsConstructor
     public static class TacletApplicationEvent {
         private final TacletApp app;
+
         private final PosInOccurrence pio;
     }
 
@@ -52,6 +55,7 @@ public class Events {
     @RequiredArgsConstructor
     public static class ScriptModificationEvent {
         private final int line;
+
         private final CallStatement cs;
     }
 
@@ -73,11 +77,31 @@ public class Events {
      */
     public static class EventForNewGoalView {
         private final ASTNode correspodingASTNode;
+
         private final State<KeyData> newState;
+
         private final List<GoalNode> listOfNotExecutedNodes;
+
         private final List<GoalNode> listOfAlreadyExecutedGoalNodes;
+
         private final List<GoalNode> closedNodes;
+
         private final List<GoalNode> openNodes;
+    }
+
+
+    @Data
+    @RequiredArgsConstructor
+    public static class SelectNodeInGoalList {
+        private final Node node;
+    }
+
+    @Data
+    @RequiredArgsConstructor
+    @AllArgsConstructor
+    public static class PublishMessage {
+        private String message;
 
+        private int flash = 0;
     }
 }

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/DebuggerStatusBar.java

@@ -28,6 +28,8 @@ import org.apache.logging.log4j.LogManager;
 import org.apache.logging.log4j.Logger;
 import org.controlsfx.control.StatusBar;
 
+import java.util.function.DoubleFunction;
+
 /**
  * Created on 09.06.2017
  *
@@ -163,6 +165,16 @@ public class DebuggerStatusBar extends StatusBar {
 
     public void publishErrorMessage(String message) {
         publishMessage(message);
+        flash((frac) -> new Color(1, 0, 0, 1 - frac));
+
+    }
+
+    public void publishSuccessMessage(String message) {
+        publishMessage(message);
+        flash((frac) -> new Color(0, 1, 0, 1 - frac));
+    }
+
+    private void flash(DoubleFunction<Color> color) {
         final Animation animation = new Transition() {
             {
                 setCycleDuration(Duration.millis(1000));
@@ -171,8 +183,7 @@ public class DebuggerStatusBar extends StatusBar {
 
             @Override
             protected void interpolate(double frac) {
-                Color vColor = new Color(1, 0, 0, 1 - frac);
-                setBackground(new Background(new BackgroundFill(vColor, CornerRadii.EMPTY, Insets.EMPTY)));
+                setBackground(new Background(new BackgroundFill(color.apply(frac), CornerRadii.EMPTY, Insets.EMPTY)));
             }
         };
         animation.play();

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/InspectionView.java

@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.gui.controls;
 import edu.kit.iti.formal.psdbg.gui.model.InspectionModel;
 import edu.kit.iti.formal.psdbg.interpreter.data.GoalNode;
 import edu.kit.iti.formal.psdbg.interpreter.data.KeyData;
+import edu.kit.iti.formal.psdbg.interpreter.data.State;
 import edu.kit.iti.formal.psdbg.interpreter.dbg.PTreeNode;
 import javafx.beans.Observable;
 import javafx.beans.property.ReadOnlyObjectProperty;
@@ -23,6 +24,8 @@ import javafx.scene.layout.HBox;
 import javafx.util.StringConverter;
 import lombok.Getter;
 
+import java.util.List;
+
 /**
  * Right part of the splitpane that displays the different parts of a state
  *
@@ -165,6 +168,17 @@ public class InspectionView extends BorderPane {
         return model;
     }
 
+    public void activate(PTreeNode<KeyData> node, State<KeyData> lastState) {
+        InspectionModel im = model.get();
+        im.getGoals().setAll(lastState.getGoals());
+        im.setSelectedGoalNodeToShow(lastState.getSelectedGoalNode());
+
+        //Experimental
+        List<PTreeNode<KeyData>> ctxn = node.getContextNodes();
+        frames.getItems().setAll(ctxn);
+        frames.getSelectionModel().select(node);
+    }
+
     /**
      * Cells for GoalView
      */

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java

@@ -4,6 +4,7 @@ import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
 import de.uka.ilkd.key.proof.ProofTreeEvent;
 import de.uka.ilkd.key.proof.ProofTreeListener;
+import edu.kit.iti.formal.psdbg.gui.controller.Events;
 import javafx.application.Platform;
 import javafx.beans.property.MapProperty;
 import javafx.beans.property.ObjectProperty;
@@ -11,9 +12,7 @@ import javafx.beans.property.SimpleMapProperty;
 import javafx.beans.property.SimpleObjectProperty;
 import javafx.collections.FXCollections;
 import javafx.fxml.FXML;
-import javafx.scene.control.TreeCell;
-import javafx.scene.control.TreeItem;
-import javafx.scene.control.TreeView;
+import javafx.scene.control.*;
 import javafx.scene.control.cell.TextFieldTreeCell;
 import javafx.scene.layout.BorderPane;
 import javafx.util.StringConverter;
@@ -87,6 +86,8 @@ public class ProofTree extends BorderPane {
         }
     };
 
+    private ContextMenu contextMenu;
+
     public ProofTree() {
         Utils.createWithFXML(this);
         treeProof.setCellFactory(this::cellFactory);
@@ -98,6 +99,9 @@ public class ProofTree extends BorderPane {
             if (n != null)
                 n.addProofTreeListener(proofTreeListener);
         });
+        setOnContextMenuRequested(evt -> {
+            getContextMenu().show(this, evt.getScreenX(), evt.getScreenY());
+        });
         init();
     }
 
@@ -123,6 +127,25 @@ public class ProofTree extends BorderPane {
         }
     }
 
+    public ContextMenu getContextMenu() {
+        if (contextMenu == null) {
+            MenuItem showGoal = new MenuItem("Show in Goal List");
+            showGoal.setOnAction((evt) -> {
+                TreeItem<TreeNode> item = treeProof.getSelectionModel().getSelectedItem();
+                Node n = item.getValue().getNode();
+                if (n != null) {
+                    Events.fire(new Events.SelectNodeInGoalList(n));
+                } else {
+                    Events.fire(new Events.PublishMessage("Current item does not have a node.", 2));
+                }
+            });
+            contextMenu = new ContextMenu(showGoal);
+            contextMenu.setAutoFix(true);
+            contextMenu.setAutoHide(true);
+        }
+        return contextMenu;
+    }
+
     private void init() {
         if (root.get() != null) {
             TreeItem<TreeNode> item = populate("Proof", root.get());

ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.java

@@ -3,6 +3,7 @@ package edu.kit.iti.formal.psdbg.gui.controls;
 import edu.kit.iti.formal.psdbg.examples.Examples;
 import edu.kit.iti.formal.psdbg.gui.controller.DebuggerMain;
 import javafx.event.ActionEvent;
+import javafx.fxml.FXML;
 import javafx.scene.layout.AnchorPane;
 
 /**
@@ -116,5 +117,13 @@ public class WelcomePane extends AnchorPane {
 
     }
 
+    @FXML
+    public void loadKeyProblem(ActionEvent event) {
+        proofScriptDebugger.getWelcomePaneDock().close();
+        proofScriptDebugger.showActiveInspector(event);
+        proofScriptDebugger.loadKeYFile();
+        proofScriptDebugger.getScriptController().newScript();
+    }
+
 }
 

ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/WelcomePane.fxml

 <?xml version="1.0" encoding="UTF-8"?>
 
-<?import de.jensd.fx.glyphs.materialdesignicons.*?>
+<?import de.jensd.fx.glyphs.materialdesignicons.MaterialDesignIconView?>
 <?import javafx.geometry.Insets?>
-<?import javafx.scene.control.*?>
-<?import javafx.scene.layout.*?>
+<?import javafx.scene.control.Button?>
+<?import javafx.scene.control.ComboBox?>
+<?import javafx.scene.control.Label?>
+<?import javafx.scene.layout.AnchorPane?>
+<?import javafx.scene.layout.ColumnConstraints?>
+<?import javafx.scene.layout.GridPane?>
+<?import javafx.scene.layout.HBox?>
+<?import javafx.scene.layout.RowConstraints?>
+<?import javafx.scene.layout.StackPane?>
 <?import javafx.scene.text.Font?>
-<fx:root xmlns:fx="http://javafx.com/fxml/1" prefHeight="400.0" prefWidth="600.0" type="AnchorPane"
-         xmlns="http://javafx.com/javafx/8.0.112">
+
+<fx:root prefHeight="485.0" prefWidth="716.0" type="AnchorPane" xmlns="http://javafx.com/javafx/8.0.121" xmlns:fx="http://javafx.com/fxml/1">
     <children>
         <Label layoutX="14.0" layoutY="14.0" text="Welcome to the ProofScriptDebugger">
             <font>
                 <Font size="24.0" />
             </font>
         </Label>
-        <Label alignment="TOP_LEFT" layoutX="14.0" layoutY="71.0" prefHeight="129.0" prefWidth="573.0"
-               text="This application is the Proof Script debugger for the KeY system. It allows to perform proofs using a proof scripting language on top of the KeY system."
-               wrapText="true"/>
+        <Label alignment="TOP_LEFT" layoutX="14.0" layoutY="71.0" prefHeight="129.0" prefWidth="573.0" text="This application is the Proof Script debugger for the KeY system. It allows to perform proofs using a proof scripting language on top of the KeY system." wrapText="true" />
 
         <HBox fillHeight="true" layoutX="117.0" layoutY="200.0" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308" spacing="25.0">
             <padding>
                 <Insets bottom="25.0" left="25.0" right="25.0" top="25.0" />
             </padding>
         </HBox>
-        <StackPane layoutX="142.0" layoutY="180.0" prefHeight="195.0" prefWidth="397.0" AnchorPane.bottomAnchor="10" AnchorPane.leftAnchor="10" AnchorPane.rightAnchor="10">
+        <StackPane layoutX="-31.0" layoutY="180.0" prefHeight="195.0" prefWidth="621.0" AnchorPane.bottomAnchor="10" AnchorPane.leftAnchor="-31.0" AnchorPane.rightAnchor="10">
             <children>
                 <GridPane hgap="25.0" layoutX="13.0" layoutY="155.0" vgap="25.0" StackPane.alignment="CENTER">
                     <columnConstraints>
                         <ColumnConstraints hgrow="SOMETIMES" minWidth="10.0" prefWidth="100.0" />
                         <ColumnConstraints hgrow="SOMETIMES" minWidth="10.0" prefWidth="100.0" />
                         <ColumnConstraints hgrow="SOMETIMES" minWidth="10.0" prefWidth="100.0" />
+                        <ColumnConstraints hgrow="SOMETIMES" minWidth="10.0" prefWidth="100.0" />
                     </columnConstraints>
                     <rowConstraints>
                         <RowConstraints maxHeight="1.7976931348623157E308" minHeight="50.0" prefHeight="30.0" valignment="CENTER" vgrow="ALWAYS" />
@@ -37,52 +43,63 @@
                         <RowConstraints maxHeight="1.7976931348623157E308" minHeight="50.0" prefHeight="30.0" valignment="CENTER" vgrow="ALWAYS" />
                     </rowConstraints>
                     <children>
-                        <Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" text="Open Script..."
-                                onAction="#openScript" GridPane.columnIndex="0" GridPane.rowIndex="0">
+
+                        <Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" onAction="#loadNewScript" text="New Script" GridPane.columnIndex="0" GridPane.rowIndex="0">
                             <graphic>
-                                <MaterialDesignIconView glyphName="BOOK_OPEN_VARIANT" size="24" />
+                                <MaterialDesignIconView glyphName="NEW_BOX" size="24" />
                             </graphic>
                         </Button>
-                        <Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" onAction="#loadNewScript"
-                                text="New Script" GridPane.columnIndex="1" GridPane.rowIndex="0">
+
+                        <Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" onAction="#openScript" text="Open Script..." GridPane.columnIndex="1" GridPane.rowIndex="0">
                             <graphic>
-                                <MaterialDesignIconView glyphName="NEW_BOX" size="24" />
+                                <MaterialDesignIconView glyphName="CODE" size="24" />
                             </graphic>
                         </Button>
 
-                        <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308" onAction="#loadContraPosition" text="Contraposition" GridPane.columnIndex="0" GridPane.rowIndex="1">
+                        <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308" onAction="#loadJavaProblem" text="Open Java..." GridPane.columnIndex="2" GridPane.rowIndex="0">
                             <graphic>
-                                <MaterialDesignIconView glyphName="NEW_BOX" size="24" />
+                                <MaterialDesignIconView glyphName="BOOK_OPEN_VARIANT" size="24" />
                             </graphic>
                         </Button>
 
-                        <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308" onAction="#loadJavaTest" text="Java Test Example" GridPane.columnIndex="1" GridPane.rowIndex="1">
+                        <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308" onAction="#loadKeyProblem" text="Open KeY Problem" GridPane.columnIndex="3" GridPane.rowIndex="0">
                             <graphic>
-                                <MaterialDesignIconView glyphName="NEW_BOX" size="24" />
+                                <MaterialDesignIconView glyphName="BARCODE_SCAN" size="24" />
                             </graphic>
                         </Button>
-                        <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308"
-                                maxWidth="1.7976931348623157E308" onAction="#loadJavaProblem" text="Load Java Problem"
-                                GridPane.columnIndex="2" GridPane.rowIndex="0">
+
+
+                        <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308" onAction="#loadHelpPage" text="Introduction" GridPane.columnIndex="3" GridPane.rowIndex="1">
                             <graphic>
                                 <MaterialDesignIconView glyphName="HELP_CIRCLE" size="24" />
                             </graphic>
                         </Button>
-                        <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308"
-                                maxWidth="1.7976931348623157E308" onAction="#loadHelpPage" text="Introduction"
-                                GridPane.columnIndex="2" GridPane.rowIndex="1">
+
+                        <Button contentDisplay="TOP" maxWidth="1.7976931348623157E308" onAction="#loadJavaProblemWithNewScript" text="Java File with Empty Script" GridPane.columnIndex="2" GridPane.rowIndex="1">
                             <graphic>
-                                <MaterialDesignIconView glyphName="HELP_CIRCLE" size="24"/>
+                                <MaterialDesignIconView glyphName="BOOK_OPEN" size="24" />
                             </graphic>
                         </Button>
-                        <Button contentDisplay="TOP" maxWidth="1.7976931348623157E308"
-                                text="Java File with Empty Script"
-                                onAction="#loadJavaProblemWithNewScript" GridPane.columnIndex="1" GridPane.rowIndex="2">
+
+
+
+
+
+                       <!-- <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308"
+                                onAction="#loadJavaTest" text="Java Test Example" GridPane.columnIndex="1" GridPane.rowIndex="1">
                             <graphic>
-                                <MaterialDesignIconView glyphName="BOOK_OPEN_VARIANT" size="24"/>
+                                <MaterialDesignIconView glyphName="NEW_BOX" size="24" />
                             </graphic>
                         </Button>
 
+                        <Button contentDisplay="TOP" maxHeight="1.7976931348623157E308" maxWidth="1.7976931348623157E308"
+                                onAction="#loadContraPosition" text="Contraposition"
+                                GridPane.columnIndex="0" GridPane.rowIndex="1">
+                            <graphic>
+                                <MaterialDesignIconView glyphName="NEW_BOX" size="24" />
+                            </graphic>
+                        </Button>
+                       -->
                     </children>
                     <StackPane.margin>
                         <Insets bottom="10.0" left="10.0" right="10.0" top="10.0" />