From b31bfc685f1c7224ff3140de37086e5aba4aa48a Mon Sep 17 00:00:00 2001
From: Sarah Grebing <grebing@ira.uka.de>
Date: Fri, 6 Oct 2017 10:11:37 +0200
Subject: [PATCH] Bigfix for exception in calling proof tree tab panes

---
 DockFX/DockFX.iml                             |  2 --
 .../gui/controller/ProofTreeController.java   |  8 ++++-
 .../formal/psdbg/gui/controls/ProofTree.java  |  9 +++++-
 .../iti/formal/psdbg/gui/controls/Utils.java  | 30 +++++++++++++++++++
 .../kit/iti/formal/psdbg/gui/debugger-ui.less |  2 +-
 5 files changed, 46 insertions(+), 5 deletions(-)

diff --git a/DockFX/DockFX.iml b/DockFX/DockFX.iml
index c9466a39..a5a0c401 100644
--- a/DockFX/DockFX.iml
+++ b/DockFX/DockFX.iml
@@ -10,8 +10,6 @@
     </content>
     <orderEntry type="inheritedJdk" />
     <orderEntry type="sourceFolder" forTests="false" />
-    <orderEntry type="library" name="Maven: org.apache.logging.log4j:log4j-api:2.6" level="project" />
-    <orderEntry type="library" name="Maven: org.apache.logging.log4j:log4j-core:2.6" level="project" />
     <orderEntry type="library" scope="TEST" name="Maven: junit:junit:4.12" level="project" />
     <orderEntry type="library" scope="TEST" name="Maven: org.hamcrest:hamcrest-core:1.3" level="project" />
     <orderEntry type="library" scope="PROVIDED" name="Maven: org.projectlombok:lombok:1.16.16" level="project" />
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
index cac2e370..01cb2bdc 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controller/ProofTreeController.java
@@ -200,8 +200,14 @@ public class ProofTreeController {
         PTreeNode nextNode = stateGraphWrapper.getStepOver(currentPointer);
         //if nextnode is null ask interpreter to execute next statement and compute next state
         if (nextNode != null) {
+            State<KeyData> lastState = this.statePointer.getState();
             this.statePointer = nextNode;
-            setNewState(statePointer.getState());
+            State<KeyData> state = this.statePointer.getState();
+            if (state.getGoals().isEmpty()) {
+                setNewState(lastState);
+            } else {
+                setNewState(state);
+            }
             //  setHighlightStmt(this.statePointer.getScriptstmt().getStartPosition(), this.statePointer.getScriptstmt().getStartPosition());
         } else {
             //no next node is present yet
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
index 182cb059..9e07c4d4 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/ProofTree.java
@@ -112,7 +112,14 @@ public class ProofTree extends BorderPane {
                 } else {
                    return object.name();
                 }*/
-                return object.sequent().toString();
+                String nodeLabel;
+                if (object.getAppliedRuleApp() != null) {
+                    nodeLabel = object.getAppliedRuleApp().rule().displayName();
+                } else {
+                    nodeLabel = object.isClosed() ? "Closed Goal" : "Open Goal";
+                }
+                return nodeLabel;
+                // return object.sequent().toString();
             }
 
             @Override
diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java
index 6ad1c239..33de2ba5 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/Utils.java
@@ -235,4 +235,34 @@ public class Utils {
         return String.valueOf(t.getData().getNode().serialNr());
     }
 
+    public static void showClosedProofDialog(String scriptName) {
+        Alert alert = new Alert(Alert.AlertType.INFORMATION);
+        alert.setTitle("Proof Closed");
+        alert.setHeaderText("The proof is closed");
+        alert.setContentText("The proof using " + scriptName + " is closed");
+        /*StringWriter sw = new StringWriter();
+        PrintWriter pw = new PrintWriter(sw);
+        ex.printStackTrace(pw);
+        String exceptionText = sw.toString();
+
+        Label label = new Label("The exception stacktrace was:");
+        TextArea textArea = new TextArea(exceptionText);
+        textArea.setEditable(false);
+        textArea.setWrapText(true);
+
+        textArea.setMaxWidth(Double.MAX_VALUE);
+        textArea.setMaxHeight(Double.MAX_VALUE);
+        GridPane.setVgrow(textArea, Priority.ALWAYS);
+        GridPane.setHgrow(textArea, Priority.ALWAYS);
+
+        GridPane expContent = new GridPane();
+        expContent.setMaxWidth(Double.MAX_VALUE);
+        expContent.add(label, 0, 0);
+        expContent.add(textArea, 0, 1);
+
+        alert.getDialogPane().setExpandableContent(expContent);
+        */
+        alert.showAndWait();
+    }
+
 }
diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less
index f650d2b7..919f14ee 100644
--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/debugger-ui.less
@@ -283,7 +283,7 @@
 }
 
 .tab-pane {
-  -fx-skin: "edu.kit.iti.formal.psdb.gui.controls.CustomTabPaneSkin";
+  -fx-skin: "edu.kit.iti.formal.psdbg.gui.controls.CustomTabPaneSkin";
 }
 
 /**********************************************************************************************************************/
-- 
2.24.1