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 37e3d58926671634e6c399ee95b29ad05d9dc329..baff58949abc22dcf757a50044fa5076c8d217f8 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 noFind, ImmutableList builtInList) { + List findTaclets = find.stream().collect(Collectors.toList()); List 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 ff96166c3c663bc3bb94f29a263e6a1c0e0e4897..f118e47b544127634bb9ec18b3636b61502b5947 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 e834b1daed61513335d9e479d6b5a1107cc1ff52..1146ff7f2cad38ffcfa8928cb9c25ebd7bee9152 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 @@ - + - +