Commit bd128f5f authored by Sarah Grebing's avatar Sarah Grebing

TacletContextMenu angepasst

parent bd1e6bc5
Pipeline #17150 passed with stages
in 9 minutes and 2 seconds
...@@ -21,6 +21,8 @@ import javafx.scene.control.MenuItem; ...@@ -21,6 +21,8 @@ import javafx.scene.control.MenuItem;
import javafx.scene.control.TextInputDialog; import javafx.scene.control.TextInputDialog;
import javafx.scene.input.Clipboard; import javafx.scene.input.Clipboard;
import javafx.scene.input.ClipboardContent; 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.ImmutableList;
import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.ImmutableSLList;
...@@ -123,7 +125,7 @@ public class TacletContextMenu extends ContextMenu { ...@@ -123,7 +125,7 @@ public class TacletContextMenu extends ContextMenu {
.prepend(c.getRewriteTaclet(goal, occ)), .prepend(c.getRewriteTaclet(goal, occ)),
c.getNoFindTaclet(goal), builtInRules); c.getNoFindTaclet(goal), builtInRules);
} catch (NullPointerException e) { } catch (NullPointerException e) {
createDummyMenuItem();
} }
//proofMacroMenuController.initViewController(getMainApp(), getContext()); //proofMacroMenuController.initViewController(getMainApp(), getContext());
...@@ -185,6 +187,7 @@ public class TacletContextMenu extends ContextMenu { ...@@ -185,6 +187,7 @@ public class TacletContextMenu extends ContextMenu {
ImmutableList<TacletApp> noFind, ImmutableList<TacletApp> noFind,
ImmutableList<BuiltInRule> builtInList) { ImmutableList<BuiltInRule> builtInList) {
List<TacletApp> findTaclets = find.stream().collect(Collectors.toList()); List<TacletApp> findTaclets = find.stream().collect(Collectors.toList());
List<TacletApp> noFindTaclets = noFind.stream().collect(Collectors.toList()); List<TacletApp> noFindTaclets = noFind.stream().collect(Collectors.toList());
...@@ -212,6 +215,17 @@ public class TacletContextMenu extends ContextMenu { ...@@ -212,6 +215,17 @@ public class TacletContextMenu extends ContextMenu {
if (occ != null) if (occ != null)
createAbbrevSection(pos.getPosInOccurrence().subTerm()); 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 { ...@@ -350,6 +364,7 @@ public class TacletContextMenu extends ContextMenu {
private void handleCopyToClipboard(ActionEvent event) { private void handleCopyToClipboard(ActionEvent event) {
final Clipboard clipboard = Clipboard.getSystemClipboard(); final Clipboard clipboard = Clipboard.getSystemClipboard();
final ClipboardContent content = new ClipboardContent(); final ClipboardContent content = new ClipboardContent();
//content.putString(parentController.getProofString() //content.putString(parentController.getProofString()
// .substring(pos.getBounds().start(), pos.getBounds().end())); // .substring(pos.getBounds().start(), pos.getBounds().end()));
clipboard.setContent(content); clipboard.setContent(content);
......
...@@ -9,16 +9,6 @@ script interactive(){ ...@@ -9,16 +9,6 @@ script interactive(){
impRight; impRight;
impRight; impRight;
impLeft; 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(){ script interactive_with_match(){
......
...@@ -11,10 +11,10 @@ ...@@ -11,10 +11,10 @@
<!-- <fx:include fx:id="insertHidden" visible="false" source="InsertHiddenMenuView.fxml"/>--> <!-- <fx:include fx:id="insertHidden" visible="false" source="InsertHiddenMenuView.fxml"/>-->
<Menu fx:id="moreRules" visible="false" text="More rules"/> <Menu fx:id="moreRules" visible="false" text="More rules"/>
<SeparatorMenuItem/> <!-- <SeparatorMenuItem/> -->
<MenuItem mnemonicParsing="false" onAction="#handleFocussedRuleApplication" <!-- <MenuItem mnemonicParsing="false" onAction="#handleFocussedRuleApplication"
text="Apply rules automatically here"/> text="Apply rules automatically here"/>-->
<!-- <!--
<fx:include fx:id="proofMacroMenu" source="ProofMacroMenuView.fxml"/> <fx:include fx:id="proofMacroMenu" source="ProofMacroMenuView.fxml"/>
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment