Repair and SectionPane/GoalOptionsMenu

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

@@ -4,6 +4,7 @@ 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.GoalOptionsMenu;
 import edu.kit.formal.gui.controls.JavaArea;
 import edu.kit.formal.gui.controls.ScriptArea;
 import edu.kit.formal.gui.controls.SequentView;
@@ -26,7 +27,9 @@ import javafx.concurrent.Task;
 import javafx.event.ActionEvent;
 import javafx.fxml.FXML;
 import javafx.fxml.Initializable;
+import javafx.scene.Node;
 import javafx.scene.control.*;
+import javafx.scene.input.MouseEvent;
 import javafx.scene.layout.GridPane;
 import javafx.scene.layout.Pane;
 import javafx.scene.layout.Priority;
@@ -49,10 +52,13 @@ import java.util.concurrent.Executors;
  * Controller for the Debugger MainWindow
  *
  * @author S.Grebing
+ * @author Alexander Weigl
  */
 public class DebuggerMainWindowController implements Initializable {
     private SimpleBooleanProperty debugMode = new SimpleBooleanProperty(false);
 
+    private GoalOptionsMenu goalOptionsMenu = new GoalOptionsMenu();
+
 
     @FXML
     private Pane rootPane;
@@ -171,7 +177,6 @@ public class DebuggerMainWindowController implements Initializable {
             /* TODO get lines of active statements marked lines
             javaSourceCode.getMarkedLines().clear();
             javaSourceCode.getMarkedLines().addAll(
-
             );*/
         });
 
@@ -216,8 +221,7 @@ public class DebuggerMainWindowController implements Initializable {
         try {
             List<ProofScript> scripts = Facade.getAST(scriptArea.getText());
             lblStatusMessage.setText("Creating new Interpreter instance ...");
-            ib.inheritState(interpreterService.interpreter.get())
-                    .setScripts(scripts);
+            ib.setScripts(scripts);
             Interpreter<KeyData> currentInterpreter = ib.build();
 
             if (debugMode) {
@@ -225,6 +229,7 @@ public class DebuggerMainWindowController implements Initializable {
                 blocker.install(currentInterpreter);
             }
             interpreterService.interpreter.set(currentInterpreter);
+            interpreterService.mainScript.set(scripts.get(0));
             interpreterService.start();
         } catch (RecognitionException e) {
             showExceptionDialog("Antlr Exception", "", "Could not parse scripts.", e);
@@ -372,6 +377,11 @@ public class DebuggerMainWindowController implements Initializable {
         blocker.unlock();
     }
 
+    public void showGoalOptions(MouseEvent actionEvent) {
+        Node n = (Node) actionEvent.getTarget();
+        goalOptionsMenu.show(n, actionEvent.getScreenX(), actionEvent.getScreenY());
+    }
+
     public class ContractLoaderService extends Service<List<Contract>> {
         @Override
         protected Task<List<Contract>> createTask() {
@@ -454,6 +464,7 @@ public class DebuggerMainWindowController implements Initializable {
 
         public GoalNodeListCell(ListView<GoalNode<KeyData>> goalNodeListView) {
             itemProperty().addListener(this::update);
+            goalOptionsMenu.selectedViewOptionProperty().addListener(this::update);
         }
 
         private void update(Observable observable) {
@@ -462,7 +473,11 @@ public class DebuggerMainWindowController implements Initializable {
                 return;
             }
             KeyData item = getItem().getData();
-            setText(item.getNode().name());
+            String text = "n/a";
+            if (goalOptionsMenu.getSelectedViewOption() != null) {
+                text = goalOptionsMenu.getSelectedViewOption().getText(item);
+            }
+            setText(text);
         }
     }
 
@@ -478,6 +493,27 @@ public class DebuggerMainWindowController implements Initializable {
         private final SimpleObjectProperty<Interpreter<KeyData>> interpreter = new SimpleObjectProperty<>();
         private final SimpleObjectProperty<ProofScript> mainScript = new SimpleObjectProperty<>();
 
+        @Override
+        protected void succeeded() {
+            updateView();
+        }
+
+        @Override
+        protected void cancelled() {
+            updateView();
+        }
+
+        @Override
+        protected void failed() {
+            getException().printStackTrace();
+            showExceptionDialog("Execution failed", "", "", getException());
+            updateView();
+        }
+
+        private void updateView() {
+            blocker.publishState();
+        }
+
         @Override
         protected Task<edu.kit.formal.interpreter.data.State<KeyData>> createTask() {
             return new Task<edu.kit.formal.interpreter.data.State<KeyData>>() {

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

@@ -51,9 +51,11 @@ public class PuppetMaster {
     }
 
     public void deinstall(Interpreter<KeyData> interpreter) {
+        if (interpreter != null) {
             interpreter.getEntryListeners().remove(entryListener);
             interpreter.getEntryListeners().remove(exitListener);
         }
+    }
 
     public Void checkForHalt(ASTNode node) {
         if (stepUntilBlock.get() > 0)
@@ -72,7 +74,7 @@ public class PuppetMaster {
         return null;
     }
 
-    private void publishState() {
+    public void publishState() {
         System.out.println("PuppetMaster.publishState");
         final State<KeyData> state = puppet.getCurrentState().copy();
         Platform.runLater(() -> {

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

+package edu.kit.formal.gui.controls;
+
+import com.google.common.collect.BiMap;
+import com.google.common.collect.HashBiMap;
+import edu.kit.formal.interpreter.data.KeyData;
+import javafx.beans.property.ObjectProperty;
+import javafx.beans.property.SimpleObjectProperty;
+import javafx.fxml.FXML;
+import javafx.scene.control.ContextMenu;
+import javafx.scene.control.RadioMenuItem;
+import javafx.scene.control.Toggle;
+import javafx.scene.control.ToggleGroup;
+
+import java.util.function.Function;
+
+public class GoalOptionsMenu extends ContextMenu {
+    @FXML
+    private ToggleGroup toggleProjection;
+
+    @FXML
+    private RadioMenuItem rmiShowSequent, rmiCFL, rmiCFS, rmiBranchLabels, rmiNodeNames, rmiRuleNames;
+
+    private ObjectProperty<ViewOption> selectedViewOption = new SimpleObjectProperty<>();
+
+    private BiMap<Toggle, ViewOption> optionMap = HashBiMap.create(6);
+
+    public GoalOptionsMenu() {
+        Utils.createWithFXML(this);
+
+        optionMap.put(rmiShowSequent, ViewOption.SEQUENT);
+        optionMap.put(rmiCFS, ViewOption.STATEMENTS);
+        optionMap.put(rmiCFL, ViewOption.PROGRAM_LINES);
+        optionMap.put(rmiBranchLabels, ViewOption.BRANCHING);
+        optionMap.put(rmiNodeNames, ViewOption.NAME);
+        optionMap.put(rmiRuleNames, ViewOption.RULES);
+
+        toggleProjection.selectedToggleProperty().addListener((observable, oldValue, newValue) -> {
+            selectedViewOption.setValue(optionMap.get(newValue));
+        });
+
+        selectedViewOption.addListener(o -> {
+            if (selectedViewOption.get() != null)
+                optionMap.inverse().get(selectedViewOption.get()).setSelected(true);
+        });
+
+        selectedViewOption.setValue(ViewOption.SEQUENT);
+    }
+
+
+    public ViewOption getSelectedViewOption() {
+        return selectedViewOption.get();
+    }
+
+    public ObjectProperty<ViewOption> selectedViewOptionProperty() {
+        return selectedViewOption;
+    }
+
+    public void setSelectedViewOption(ViewOption selectedViewOption) {
+        this.selectedViewOption.set(selectedViewOption);
+    }
+
+    public enum ViewOption {
+        BRANCHING(KeyData::getBranchingLabel),
+        RULES(KeyData::getRuleLabel),
+        PROGRAM_LINES(KeyData::getProgramLinesLabel),
+        STATEMENTS(KeyData::getProgramStatementsLabel),
+        NAME(KeyData::getNameLabel),
+        SEQUENT(item -> item.getNode().sequent().toString());
+
+        private final Function<KeyData, String> projection;
+
+        ViewOption(Function<KeyData, String> toString) {
+            projection = toString;
+        }
+
+        public String getText(KeyData item) {
+            return projection.apply(item);
+        }
+    }
+}
\ No newline at end of file

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

@@ -220,6 +220,9 @@ public class ScriptArea extends CodeArea {
             lineNo.setTextFill(defaultTextFill);
             hbox.setPadding(defaultInsets);
             hbox.getStyleClass().add("lineno");
+
+            hbox.setStyle("-fx-cursor: hand");
+
             return hbox;
         }
 

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

+package edu.kit.formal.gui.controls;
+
+import javafx.beans.property.StringProperty;
+import javafx.collections.ObservableList;
+import javafx.fxml.FXML;
+import javafx.fxml.FXMLLoader;
+import javafx.scene.Node;
+import javafx.scene.control.Label;
+import javafx.scene.layout.BorderPane;
+import javafx.scene.layout.HBox;
+
+import java.io.IOException;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (05.06.17)
+ */
+public class SectionPane extends BorderPane {
+    private StringProperty title;
+
+    @FXML
+    private Label titleLabel;
+
+    @FXML
+    private HBox northBox;
+
+    @FXML
+    private HBox buttons;
+
+    public SectionPane() {
+        super();
+        FXMLLoader loader = new FXMLLoader(getClass().getResource("SectionPane.fxml"));
+        loader.setRoot(this);
+        loader.setController(this);
+        try {
+            loader.load();
+        } catch (IOException e) {
+            e.printStackTrace();
+        }
+
+        title = titleLabel.textProperty();
+    }
+
+    public SectionPane(Node center) {
+        this();
+        setCenter(center);
+    }
+
+
+    public String getTitle() {
+        return title.get();
+    }
+
+    public StringProperty titleProperty() {
+        return title;
+    }
+
+    public void setTitle(String title) {
+        this.title.set(title);
+    }
+
+
+    public ObservableList<Node> getHeaderRight() {
+        return buttons.getChildren();
+    }
+}

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

@@ -72,8 +72,11 @@ public class SequentView extends CodeArea {
     }
 
     private void hightlightRange(int start, int end) {
+        try {
             clearHighlight();
             setStyleClass(start, end, "sequent-highlight");
+        } catch (IllegalStateException e) {
+        }
     }
 
     private void clearHighlight() {

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

+package edu.kit.formal.gui.controls;
+
+import javafx.fxml.FXMLLoader;
+
+import java.io.IOException;
+
+/**
+ * @author Alexander Weigl
+ * @version 1 (05.06.17)
+ */
+public class Utils {
+    private Utils() {
+    }
+
+    public static void createWithFXML(Object node) {
+        FXMLLoader loader = new FXMLLoader(
+                node.getClass().getResource(node.getClass().getSimpleName() + ".fxml")
+        );
+        loader.setController(node);
+        loader.setRoot(node);
+        try {
+            loader.load();
+        } catch (IOException e) {
+            throw new RuntimeException("Could not load fxml", e);
+        }
+    }
+}

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

 package edu.kit.formal.interpreter;
 
 import de.uka.ilkd.key.api.KeYApi;
+import de.uka.ilkd.key.api.ProjectedNode;
 import de.uka.ilkd.key.api.ProofApi;
 import de.uka.ilkd.key.api.ScriptApi;
 import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.macros.ProofMacro;
 import de.uka.ilkd.key.macros.scripts.ProofScriptCommand;
 import de.uka.ilkd.key.proof.Proof;
+import edu.kit.formal.interpreter.data.GoalNode;
 import edu.kit.formal.interpreter.data.KeyData;
 import edu.kit.formal.interpreter.data.VariableAssignment;
 import edu.kit.formal.interpreter.funchdl.*;
@@ -75,9 +77,9 @@ public class InterpreterBuilder {
     }
 
     public InterpreterBuilder proof(KeYEnvironment env, Proof proof) {
-        //TODO relax constructor of proofapi
-        //return proof(new ProofApi(proof, env));
-        return this;
+        this.keyEnvironment = env;
+        this.proof = proof;
+        return proof(new ProofApi(proof, env));
     }
 
     public InterpreterBuilder scriptCommands() {
@@ -181,4 +183,20 @@ public class InterpreterBuilder {
         lookup.getBuilders().add(0, ignoreHandler);
         return this;
     }
+
+    public InterpreterBuilder startState() {
+        if (proof == null || keyEnvironment == null)
+            throw new IllegalStateException("Call proof(..) before startState");
+
+        final ProofApi pa = new ProofApi(proof, keyEnvironment);
+        final ProjectedNode root = pa.getFirstOpenGoal();
+        final KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
+        final GoalNode<KeyData> startGoal = new GoalNode<>(null, keyData);
+        return startState(startGoal);
+    }
+
+    private InterpreterBuilder startState(GoalNode<KeyData> startGoal) {
+        interpreter.newState(startGoal);
+        return this;
+    }
 }

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

@@ -89,17 +89,14 @@ public class KeYProofFacade {
         assert readyToExecute.getValue();
 
         InterpreterBuilder interpreterBuilder = new InterpreterBuilder();
-        interpreterBuilder.proof(environment.get(), proof.get())
+        interpreterBuilder
+                .proof(environment.get(), proof.get())
+                .startState()
                 .macros()
                 .scriptCommands()
                 .scriptSearchPath(new File("."));
         getProof().getProofIndependentSettings().getGeneralSettings().setOneStepSimplification(false);
 
-        // Set first state
-        final ProofApi pa = new ProofApi(getProof(), getEnvironment());
-        final ProjectedNode root = pa.getFirstOpenGoal();
-        final KeyData keyData = new KeyData(root.getProofNode(), pa.getEnv(), pa.getProof());
-        final GoalNode<KeyData> startGoal = new GoalNode<>(null, keyData);
         return interpreterBuilder;
     }
 

src/main/java/edu/kit/formal/interpreter/data/KeyData.java

@@ -3,10 +3,9 @@ package edu.kit.formal.interpreter.data;
 import de.uka.ilkd.key.control.KeYEnvironment;
 import de.uka.ilkd.key.proof.Node;
 import de.uka.ilkd.key.proof.Proof;
-import lombok.AllArgsConstructor;
-import lombok.Data;
-import lombok.EqualsAndHashCode;
-import lombok.ToString;
+import lombok.*;
+
+import java.util.function.Function;
 
 /**
  * @author Alexander Weigl
@@ -16,10 +15,18 @@ import lombok.ToString;
 @AllArgsConstructor
 @ToString
 @EqualsAndHashCode
+@RequiredArgsConstructor
 public class KeyData {
-    private Node node;
-    private KeYEnvironment env;
-    private Proof proof;
+    private static final String SEPARATOR = " // ";
+    private final Node node;
+    private final KeYEnvironment env;
+    private final Proof proof;
+
+    private String branchingLabel,
+            ruleLabel,
+            programLinesLabel,
+            programStatementsLabel,
+            nameLabel;
 
     public KeyData(KeyData data, Node node) {
         env = data.env;
@@ -29,5 +36,61 @@ public class KeyData {
         this.node = node;
     }
 
+    public String getRuleLabel() {
+        if (ruleLabel == null) {
+            ruleLabel = constructLabel((Node n) -> n.getAppliedRuleApp().rule().name().toString());
+        }
+        return ruleLabel;
+    }
+
+    private String constructLabel(Function<Node, String> projection) {
+        StringBuilder sb = new StringBuilder();
+        Node cur = node;
+        do {
+            try {
+                String section = projection.apply(node);
+                if (section != null) {
+                    sb.append(section);
+                    sb.append(SEPARATOR);
+                }
+            } catch (Exception e) {
+            }
+            cur = cur.parent();
+        } while (cur != null);
+        sb.append("$$");
+        return sb.toString();
+    }
+
+    public String getBranchingLabel() {
+        if (branchingLabel == null) {
+            branchingLabel = constructLabel(n -> n.getNodeInfo().getBranchLabel());
+        }
+        return branchingLabel;
+    }
+
+    public String getNameLabel() {
+        if (nameLabel == null) {
+            nameLabel = constructLabel(Node::name);
+        }
+        return nameLabel;
+    }
+
+
+    public String getProgramLinesLabel() {
+        if (programLinesLabel == null) {
+            programLinesLabel = constructLabel(n ->
+                    Integer.toString(n.getNodeInfo().getExecStatementPosition().getLine()));
+        }
+        return programLinesLabel;
+    }
+
+    public String getProgramStatementsLabel() {
+        if (programStatementsLabel == null) {
+            programStatementsLabel = constructLabel(n ->
+                    n.getNodeInfo().getFirstStatementString());
+        }
+        return programStatementsLabel;
+    }
+
 
 }

src/main/resources/DebuggerMain.fxml

@@ -2,9 +2,7 @@
 
 
 <?import de.jensd.fx.glyphs.materialdesignicons.*?>
-<?import edu.kit.formal.gui.controls.JavaArea?>
-<?import edu.kit.formal.gui.controls.ScriptArea?>
-<?import edu.kit.formal.gui.controls.SequentView?>
+<?import edu.kit.formal.gui.controls.*?>
 <?import javafx.geometry.Insets?>
 <?import javafx.scene.control.*?>
 <?import javafx.scene.layout.*?>
@@ -81,36 +79,41 @@
                 </VBox>
                 <SplitPane orientation="VERTICAL" dividerPositions="0.25,0.75">
                     <items>
-                        <BorderPane>
-                            <top>
-                                <Label text="Current Goals:" styleClass="header"/>
-                            </top>
+                        <SectionPane title="Current Goals">
+                            <headerRight>
+                                <Button onMouseClicked="#showGoalOptions">
+                                    <graphic>
+                                        <MaterialDesignIconView glyphName="WRENCH"/>
+                                    </graphic>
+                                </Button>
+                            </headerRight>
                             <center>
                                 <ListView fx:id="goalView"/>
                             </center>
-                        </BorderPane>
+                        </SectionPane>
 
                         <SplitPane>
                             <padding>
                                 <Insets top="5" left="5" right="5" bottom="5"/>
                             </padding>
                             <items>
-                                <BorderPane SplitPane.resizableWithParent="true">
-                                    <top>
-                                        <Label styleClass="header" text="Sequent"/>
-                                    </top>
+                                <SectionPane title="Sequent">
+                                    <headerRight>
+                                        <Button>
+                                            <graphic>
+                                                <MaterialDesignIconView glyphName="WRENCH"/>
+                                            </graphic>
+                                        </Button>
+                                    </headerRight>
                                     <center>
                                         <SequentView fx:id="sequentView"/>
                                     </center>
-                                </BorderPane>
-                                <BorderPane>
-                                    <top>
-                                        <Label text="Source Code" styleClass="header"/>
-                                    </top>
+                                </SectionPane>
+                                <SectionPane title="Source Code">
                                     <center>
                                         <JavaArea fx:id="javaSourceCode"/>
                                     </center>
-                                </BorderPane>
+                                </SectionPane>
                             </items>
                         </SplitPane>
                     </items>

src/main/resources/GoalView.fxml

-<?import javafx.scene.control.ListView?>
-<?import javafx.scene.control.TextArea?>
-<?import javafx.scene.layout.VBox?>
-<fx:root xmlns:fx="http://javafx.com/fxml" type="javafx.scene.layout.VBox"
-         prefHeight="369.0" prefWidth="295.0">
+<?xml version="1.0" encoding="UTF-8"?>
+
+<?import javafx.scene.control.Button?>
+<?import javafx.scene.control.Label?>
+<?import javafx.scene.layout.HBox?>
+
+<fx:root alignment="BASELINE_CENTER" prefHeight="369.0" prefWidth="295.0" type="javafx.scene.layout.HBox" xmlns:fx="http://javafx.com/fxml/1" xmlns="http://javafx.com/javafx/8.0.112">
    <children>
-        <ListView fx:id="listOfGoalsView" prefHeight="200.0" prefWidth="200.0"/>
-        <TextArea fx:id="goalNodeView" prefHeight="200.0" prefWidth="200.0"/>
+      <Label text="Label" />
+      <Button mnemonicParsing="false" text="Button" />
    </children>