From bd128f5ff7a004511ab97e481cc81816fc373c6f Mon Sep 17 00:00:00 2001
From: Sarah Grebing <grebing@ira.uka.de>
Date: Mon, 22 Jan 2018 12:28:10 +0100
Subject: [PATCH] TacletContextMenu angepasst

---
 .../psdbg/gui/controls/TacletContextMenu.java   | 17 ++++++++++++++++-
 .../psdbg/examples/contraposition/script.kps    | 10 ----------
 .../psdbg/gui/controls/TacletContextMenu.fxml   |  6 +++---
 3 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java
index 37e3d589..baff5894 100644
--- a/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java
+++ b/ui/src/main/java/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.java
@@ -21,6 +21,8 @@ import javafx.scene.control.MenuItem;
 import javafx.scene.control.TextInputDialog;
 import javafx.scene.input.Clipboard;
 import javafx.scene.input.ClipboardContent;
+import javafx.scene.paint.Color;
+import javafx.scene.text.Text;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 
@@ -123,7 +125,7 @@ public class TacletContextMenu extends ContextMenu {
                             .prepend(c.getRewriteTaclet(goal, occ)),
                     c.getNoFindTaclet(goal), builtInRules);
         } catch (NullPointerException e) {
-
+            createDummyMenuItem();
         }
 
         //proofMacroMenuController.initViewController(getMainApp(), getContext());
@@ -185,6 +187,7 @@ public class TacletContextMenu extends ContextMenu {
                                   ImmutableList<TacletApp> noFind,
                                   ImmutableList<BuiltInRule> builtInList) {
 
+
         List<TacletApp> findTaclets = find.stream().collect(Collectors.toList());
         List<TacletApp> noFindTaclets = noFind.stream().collect(Collectors.toList());
 
@@ -212,6 +215,17 @@ public class TacletContextMenu extends ContextMenu {
         if (occ != null)
             createAbbrevSection(pos.getPosInOccurrence().subTerm());
 
+
+    }
+
+    private void createDummyMenuItem() {
+        Text t = new Text("This is not a goal state.\nSelect a goal state from the list.");
+        t.setFill(Color.RED);
+
+        MenuItem item = new MenuItem();
+        item.setGraphic(t);
+        rootMenu.getItems().add(0, item);
+
     }
 
     /**
@@ -350,6 +364,7 @@ public class TacletContextMenu extends ContextMenu {
     private void handleCopyToClipboard(ActionEvent event) {
         final Clipboard clipboard = Clipboard.getSystemClipboard();
         final ClipboardContent content = new ClipboardContent();
+
         //content.putString(parentController.getProofString()
         //        .substring(pos.getBounds().start(), pos.getBounds().end()));
         clipboard.setContent(content);
diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
index ff96166c..f118e47b 100644
--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/examples/contraposition/script.kps
@@ -9,16 +9,6 @@ script interactive(){
   impRight;
   impRight;
   impLeft;
-  cases {
-  	case match '#0 // .*':
-  		notRight formula=`(!p)`;
-  		close formula=`p`;
-
-  	case match '#1 // .*':
-  		notRight formula=`(!p)`;
-  		notLeft formula=`(!q)`;
-  		close formula=`q`;
-  }
 }
 
 script interactive_with_match(){
diff --git a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.fxml b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.fxml
index e834b1da..1146ff7f 100644
--- a/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.fxml
+++ b/ui/src/main/resources/edu/kit/iti/formal/psdbg/gui/controls/TacletContextMenu.fxml
@@ -11,10 +11,10 @@
         <!--        <fx:include fx:id="insertHidden" visible="false" source="InsertHiddenMenuView.fxml"/>-->
         <Menu fx:id="moreRules" visible="false" text="More rules"/>
 
-        <SeparatorMenuItem/>
+        <!-- <SeparatorMenuItem/> -->
 
-        <MenuItem mnemonicParsing="false" onAction="#handleFocussedRuleApplication"
-                  text="Apply rules automatically here"/>
+        <!--  <MenuItem mnemonicParsing="false" onAction="#handleFocussedRuleApplication"
+                    text="Apply rules automatically here"/>-->
 
         <!--
         <fx:include fx:id="proofMacroMenu" source="ProofMacroMenuView.fxml"/>
-- 
GitLab