From 61e259a62c461845c56a36f7e7e4cba43f537c81 Mon Sep 17 00:00:00 2001 From: Alexander Weigl Date: Tue, 11 Jul 2017 18:30:12 +0200 Subject: [PATCH] Taclet apps in rule context menu --- .../DebuggerMainWindowController.java | 30 +- .../formal/gui/controls/InspectionView.java | 2 +- .../kit/formal/gui/controls/SequentView.java | 50 +- .../gui/controls/TacletContextMenu.java | 467 ++++++++++++++++++ .../edu/kit/formal/gui/controls/Utils.java | 10 +- .../kit/formal/interpreter/data/KeyData.java | 32 +- .../gui/controls/TacletContextMenu.fxml | 37 ++ .../edu/kit/formal/gui/debugger-ui.less | 24 +- 8 files changed, 603 insertions(+), 49 deletions(-) create mode 100644 src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java create mode 100644 src/main/resources/edu/kit/formal/gui/controls/TacletContextMenu.fxml diff --git a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java index 9819b5e9..4b88f109 100644 --- a/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java +++ b/src/main/java/edu/kit/formal/gui/controller/DebuggerMainWindowController.java @@ -55,8 +55,8 @@ public class DebuggerMainWindowController implements Initializable { private final ProofTreeController proofTreeController = new ProofTreeController(); private final InspectionViewsController inspectionViewsController = new InspectionViewsController(); private final ExecutorService executorService = Executors.newFixedThreadPool(2); - private final KeYProofFacade facade = new KeYProofFacade(); - private final ContractLoaderService contractLoaderService = new ContractLoaderService(); + public static final KeYProofFacade FACADE = new KeYProofFacade(); + public final ContractLoaderService contractLoaderService = new ContractLoaderService(); /** * Property: current loaded javaFile */ @@ -89,7 +89,7 @@ public class DebuggerMainWindowController implements Initializable { /** * True, iff the execution is not possible */ - private ObservableBooleanValue executeNotPossible = proofTreeController.executeNotPossibleProperty().or(facade.readyToExecuteProperty().not()); + private ObservableBooleanValue executeNotPossible = proofTreeController.executeNotPossibleProperty().or(FACADE.readyToExecuteProperty().not()); /** * @@ -117,7 +117,6 @@ public class DebuggerMainWindowController implements Initializable { //statusBar.publishMessage("File: " + (newValue != null ? newValue.getAbsolutePath() : "n/a")); - //Debugging Utils.addDebugListener(javaCode); Utils.addDebugListener(executeNotPossible, "executeNotPossible"); @@ -186,12 +185,12 @@ public class DebuggerMainWindowController implements Initializable { //region Actions: Execution @FXML public void executeScript() { - executeScript(facade.buildInterpreter(), false); + executeScript(FACADE.buildInterpreter(), false); } @FXML public void executeScriptFromCursor() { - InterpreterBuilder ib = facade.buildInterpreter(); + InterpreterBuilder ib = FACADE.buildInterpreter(); // ib.inheritState(interpreterService.interpreterProperty().get()); ///* // LineMapping lm = new LineMapping(scriptArea.getText()); @@ -204,7 +203,7 @@ public class DebuggerMainWindowController implements Initializable { @FXML public void executeInDebugMode() { - executeScript(facade.buildInterpreter(), true); + executeScript(FACADE.buildInterpreter(), true); } //endregion @@ -271,7 +270,7 @@ public class DebuggerMainWindowController implements Initializable { public void openScript(File scriptFile) { assert scriptFile != null; - setInitialDirectory(scriptFile.getParentFile() ); + setInitialDirectory(scriptFile.getParentFile()); try { String code = FileUtils.readFileToString(scriptFile, Charset.defaultCharset()); ScriptArea area = scriptController.createNewTab(scriptFile); @@ -291,10 +290,10 @@ public class DebuggerMainWindowController implements Initializable { if (keyFile != null) { setKeyFile(keyFile); setInitialDirectory(keyFile.getParentFile()); - Task task = facade.loadKeyFileTask(keyFile); + Task task = FACADE.loadKeyFileTask(keyFile); task.setOnSucceeded(event -> { statusBar.publishMessage("Loaded key sourceName: %s", keyFile); - getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(facade.getPseudoGoals()); + getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals()); }); task.setOnFailed(event -> { @@ -335,6 +334,7 @@ public class DebuggerMainWindowController implements Initializable { loadJavaFile(); showCodeDock(null); } + /** * Creates a filechooser dialog * @@ -385,7 +385,7 @@ public class DebuggerMainWindowController implements Initializable { public KeYProofFacade getFacade() { - return facade; + return FACADE; } //region Property @@ -552,7 +552,7 @@ public class DebuggerMainWindowController implements Initializable { public class ContractLoaderService extends Service> { @Override protected Task> createTask() { - return facade.getContractsForJavaFileTask(getJavaFile()); + return FACADE.getContractsForJavaFileTask(getJavaFile()); } @Override @@ -564,13 +564,13 @@ public class DebuggerMainWindowController implements Initializable { protected void succeeded() { statusBar.publishMessage("Contract loaded"); List contracts = getValue(); - ContractChooser cc = new ContractChooser(facade.getService(), contracts); + ContractChooser cc = new ContractChooser(FACADE.getService(), contracts); cc.showAndWait().ifPresent(result -> { setChosenContract(result); try { - facade.activateContract(result); - getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(facade.getPseudoGoals()); + FACADE.activateContract(result); + getInspectionViewsController().getActiveInspectionViewTab().getModel().getGoals().setAll(FACADE.getPseudoGoals()); } catch (ProofInputException e) { Utils.showExceptionDialog("", "", "", e); } diff --git a/src/main/java/edu/kit/formal/gui/controls/InspectionView.java b/src/main/java/edu/kit/formal/gui/controls/InspectionView.java index de90cc2b..cd7a0d6d 100644 --- a/src/main/java/edu/kit/formal/gui/controls/InspectionView.java +++ b/src/main/java/edu/kit/formal/gui/controls/InspectionView.java @@ -43,7 +43,7 @@ public class InspectionView extends BorderPane { (observable, oldValue, newValue) -> { goalView.getSelectionModel().select(newValue); if (newValue != null && newValue.getData() != null) { - getSequentView().setNode(newValue.getData().getNode()); + getSequentView().setNode(newValue.getData().getGoal()); // TODO weigl: get marked lines of the program, and set it model.get().highlightedJavaLinesProperty().get() .clear(); diff --git a/src/main/java/edu/kit/formal/gui/controls/SequentView.java b/src/main/java/edu/kit/formal/gui/controls/SequentView.java index 7f5b081d..5313243e 100644 --- a/src/main/java/edu/kit/formal/gui/controls/SequentView.java +++ b/src/main/java/edu/kit/formal/gui/controls/SequentView.java @@ -4,10 +4,12 @@ import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.NamespaceSet; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.pp.*; -import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import edu.kit.formal.interpreter.KeYProofFacade; import javafx.beans.Observable; import javafx.beans.property.SimpleObjectProperty; +import javafx.scene.input.MouseButton; import javafx.scene.input.MouseEvent; import javafx.scene.layout.*; import javafx.scene.paint.Color; @@ -26,7 +28,9 @@ public class SequentView extends CodeArea { private LogicPrinter lp; private IdentitySequentPrintFilter filter; private LogicPrinter.PosTableStringBackend backend; - private SimpleObjectProperty node = new SimpleObjectProperty<>(); + private SimpleObjectProperty node = new SimpleObjectProperty<>(); + private KeYProofFacade keYProofFacade; + private TacletContextMenu menu; public SequentView() { @@ -34,11 +38,11 @@ public class SequentView extends CodeArea { setEditable(false); node.addListener(this::update); setOnMouseMoved(this::hightlight); + setOnMouseClicked(this::onMouseClick); } private void hightlight(MouseEvent mouseEvent) { if (backend == null) return; - CharacterHit hit = hit(mouseEvent.getX(), mouseEvent.getY()); int insertionPoint = hit.getInsertionIndex(); PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter); @@ -51,14 +55,26 @@ public class SequentView extends CodeArea { mouseEvent.consume(); } - public void mouseClick(MouseEvent e) { + public void onMouseClick(MouseEvent e) { + if (menu != null && menu.isShowing()) { + menu.hide(); + } + if (backend == null) { return; } - CharacterHit hit = hit(e.getX(), e.getY()); - int insertionPoint = hit.getInsertionIndex(); - PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter); - + if (e.getButton() == MouseButton.SECONDARY) { + CharacterHit hit = hit(e.getX(), e.getY()); + int insertionPoint = hit.getInsertionIndex(); + PosInSequent pis = backend.getInitialPositionTable().getPosInSequent(insertionPoint, filter); + if (pis == null) return; + + menu = new TacletContextMenu(keYProofFacade, pis, node.get()); + menu.setAutoFix(true); + menu.setAutoHide(true); + menu.show(this, e.getScreenX(), e.getScreenY()); + e.consume(); + } /* Goal g = new Goal(node, null); ImmutableList rules = g.ruleAppIndex().getFindTaclet(new TacletFilter() { @@ -109,21 +125,29 @@ public class SequentView extends CodeArea { clear(); insertText(0, backend.getString()); - if (node.get().isClosed()) { + if (node.get().node().isClosed()) { this.setBorder(new Border(new BorderStroke(Color.RED, BorderStrokeStyle.SOLID, CornerRadii.EMPTY, BorderWidths.DEFAULT))); this.getStyleClass().add("closed-sequent-view"); } } - public Node getNode() { + public Goal getNode() { return node.get(); } - public void setNode(Node node) { + public SimpleObjectProperty nodeProperty() { + return node; + } + + public void setNode(Goal node) { this.node.set(node); } - public SimpleObjectProperty nodeProperty() { - return node; + public KeYProofFacade getKeYProofFacade() { + return keYProofFacade; + } + + public void setKeYProofFacade(KeYProofFacade keYProofFacade) { + this.keYProofFacade = keYProofFacade; } } diff --git a/src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java b/src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java new file mode 100644 index 00000000..523c6f38 --- /dev/null +++ b/src/main/java/edu/kit/formal/gui/controls/TacletContextMenu.java @@ -0,0 +1,467 @@ +package edu.kit.formal.gui.controls; + +import de.uka.ilkd.key.control.ProofControl; +import de.uka.ilkd.key.gui.nodeviews.TacletMenu.TacletAppComparator; +import de.uka.ilkd.key.logic.Name; +import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.logic.Term; +import de.uka.ilkd.key.pp.AbbrevMap; +import de.uka.ilkd.key.pp.NotationInfo; +import de.uka.ilkd.key.pp.PosInSequent; +import de.uka.ilkd.key.proof.Goal; +import de.uka.ilkd.key.rule.*; +import edu.kit.formal.gui.controller.DebuggerMainWindowController; +import edu.kit.formal.interpreter.KeYProofFacade; +import javafx.event.ActionEvent; +import javafx.fxml.FXML; +import javafx.scene.control.ContextMenu; +import javafx.scene.control.Menu; +import javafx.scene.control.MenuItem; +import javafx.scene.control.TextInputDialog; +import javafx.scene.input.Clipboard; +import javafx.scene.input.ClipboardContent; +import org.key_project.util.collection.ImmutableList; +import org.key_project.util.collection.ImmutableSLList; + +import java.util.*; +import java.util.stream.Collectors; + +/** + * Copied from TacletMenu and adapted to JavaFX style. This is NOT a menu + * anymore but a view controller. There is a field rootMenu to access the actual + * menu. + * + * @author Victor Schuemmer + * @author Alexander Weigl + * @version 1.0 + * @see de.uka.ilkd.key.gui.nodeviews.TacletMenu + */ +public class TacletContextMenu extends ContextMenu { + + private static final Set CLUTTER_RULESETS = new LinkedHashSet(); + + static { + CLUTTER_RULESETS.add(new Name("notHumanReadable")); + CLUTTER_RULESETS.add(new Name("obsolete")); + CLUTTER_RULESETS.add(new Name("pullOutQuantifierAll")); + CLUTTER_RULESETS.add(new Name("pullOutQuantifierEx")); + } + + private static final Set CLUTTER_RULES = new LinkedHashSet(); + + static { + CLUTTER_RULES.add(new Name("cut_direct_r")); + CLUTTER_RULES.add(new Name("cut_direct_l")); + CLUTTER_RULES.add(new Name("case_distinction_r")); + CLUTTER_RULES.add(new Name("case_distinction_l")); + CLUTTER_RULES.add(new Name("local_cut")); + CLUTTER_RULES.add(new Name("commute_and_2")); + CLUTTER_RULES.add(new Name("commute_or_2")); + CLUTTER_RULES.add(new Name("boxToDiamond")); + CLUTTER_RULES.add(new Name("pullOut")); + CLUTTER_RULES.add(new Name("typeStatic")); + CLUTTER_RULES.add(new Name("less_is_total")); + CLUTTER_RULES.add(new Name("less_zero_is_total")); + CLUTTER_RULES.add(new Name("applyEqReverse")); + + // the following are used for drag'n'drop interactions + CLUTTER_RULES.add(new Name("eqTermCut")); + CLUTTER_RULES.add(new Name("instAll")); + CLUTTER_RULES.add(new Name("instEx")); + } + + private PosInSequent pos; + + @FXML + private ContextMenu rootMenu; + @FXML + private MenuItem noRules; + @FXML + private Menu moreRules; + @FXML + private Menu insertHidden; + @FXML + private MenuItem copyToClipboard; + @FXML + private MenuItem createAbbr; + @FXML + private MenuItem enableAbbr; + @FXML + private MenuItem disableAbbr; + @FXML + private MenuItem changeAbbr; + + + private Goal goal; + private PosInOccurrence occ; + private NotationInfo notationInfo = new NotationInfo(); + + public TacletContextMenu(KeYProofFacade keYProofFacade, PosInSequent pos, Goal goal) { + Utils.createWithFXML(this); + + /*mediator = getContext().getKeYMediator(); + comp = new TacletAppComparator(); + insertHiddenController.initViewController(getMainApp(), getContext()); + */ + if (pos == null) + throw new IllegalArgumentException( + "Argument pos must not be null."); + this.pos = pos; + this.goal = goal; + + occ = pos.getPosInOccurrence(); + //MediatorProofControl c = new MediatorProofControl(new DefaultAbstractMediatorUserInterfaceControlAdapter()); + ProofControl c = DebuggerMainWindowController.FACADE.getEnvironment().getUi().getProofControl(); + + final ImmutableList builtInRules = c.getBuiltInRule(goal, occ); + createTacletMenu( + removeRewrites(c.getFindTaclet(goal, occ)) + .prepend(c.getRewriteTaclet(goal, occ)), + c.getNoFindTaclet(goal), builtInRules); + + //proofMacroMenuController.initViewController(getMainApp(), getContext()); + //proofMacroMenuController.init(occ); + } + + /** + * Removes RewriteTaclet from the list. + * + * @param list the IList from where the RewriteTaclet are removed + * @return list without RewriteTaclets + */ + private static ImmutableList removeRewrites( + ImmutableList list) { + ImmutableList result = ImmutableSLList.nil(); + Iterator it = list.iterator(); + + while (it.hasNext()) { + TacletApp tacletApp = it.next(); + Taclet taclet = tacletApp.taclet(); + result = (taclet instanceof RewriteTaclet ? result + : result.prepend(tacletApp)); + } + return result; + } + + /** + * Creates the menu by adding all submenus and items. + */ + private void createTacletMenu(ImmutableList find, + ImmutableList noFind, + ImmutableList builtInList) { + + List findTaclets = find.stream().collect(Collectors.toList()); + List noFindTaclets = noFind.stream().collect(Collectors.toList()); + + Collections.sort(findTaclets, + //compare by name + Comparator.comparing(o -> o.taclet().name()) + ); + + List toAdd = new ArrayList<>(findTaclets.size() + noFindTaclets.size()); + toAdd.addAll(findTaclets); + + boolean rulesAvailable = find.size() > 0; + + if (pos.isSequent()) { + rulesAvailable |= noFind.size() > 0; + toAdd.addAll(noFindTaclets); + } + + if (rulesAvailable) { + createMenuItems(toAdd); + } else { + noRules.setVisible(true); + } + + if (occ != null) + createAbbrevSection(pos.getPosInOccurrence().subTerm()); + + } + + /** + * Creates menu items for all given taclets. A submenu for insertion of + * hidden terms will be created if there are any, and rare rules will be in + * a 'More rules' submenu. + * + * @param taclets the list of taclets to create menu items for + */ + private void createMenuItems(List taclets) { + int idx = 0; + for (final TacletApp app : taclets) { + final Taclet taclet = app.taclet(); + + /* if (!mediator.getFilterForInteractiveProving().filter(taclet)) { + continue; + }*/ + + final MenuItem item = new MenuItem(app.taclet().name().toString()); + item.setOnAction(event -> { + handleRuleApplication(app); + }); + + + // Items for insertion of hidden terms appear in a submenu. + /*if (insertHiddenController.isResponsible(item)) { + insertHiddenController.add(item); + } else */ + { + // If one of the sets contains the rule it is considered rare + // and moved to a 'More rules' submenu. + boolean rareRule = false; + for (RuleSet rs : taclet.getRuleSets()) { + if (CLUTTER_RULESETS.contains(rs.name())) + rareRule = true; + } + if (CLUTTER_RULES.contains(taclet.name())) + rareRule = true; + + if (rareRule) + moreRules.getItems().add(item); + else + rootMenu.getItems().add(idx++, item); + } + } + // Make submenus visible iff they are not empty. + if (moreRules.getItems().size() > 0) + moreRules.setVisible(true); + /*if (!insertHiddenController.isEmpty()) + insertHiddenController.setVisible(true); + */ + + } + + /** + public TacletFilter getFilterForInteractiveProving() { + if(this.filterForInteractiveProving == null) { + this.filterForInteractiveProving = new TacletFilter() { + protected boolean filter(Taclet taclet) { + String[] var2 = JoinProcessor.SIMPLIFY_UPDATE; + int var3 = var2.length; + + for(int var4 = 0; var4 < var3; ++var4) { + String name = var2[var4]; + if(name.equals(taclet.name().toString())) { + return false; + } + } + + return true; + } + }; + } + + return this.filterForInteractiveProving; + }*/ + + /** + * Manages the visibility of all menu items dealing with abbreviations based + * on if the given term already is abbreviated and if the abbreviation is + * enabled. + * + * @param t the term to check if there already is an abbreviation of + */ + + private void createAbbrevSection(Term t) { + AbbrevMap scm = notationInfo.getAbbrevMap(); + if (scm.containsTerm(t)) { + changeAbbr.setVisible(true); + if (scm.isEnabled(t)) { + disableAbbr.setVisible(true); + } else { + enableAbbr.setVisible(true); + } + } else { + createAbbr.setVisible(true); + } + } + + /** + * Handles the application of an 'ordinary' rule. + * + * @param event + */ + private void handleRuleApplication(TacletApp event) { + // Synchronization for StaticSequentView + /* parentController.setLastTacletActionID(parentController.getOwnID()); + mediator.getUI().getProofControl().selectedTaclet( + ((TacletMenuItem) event.getSource()).getTaclet(), goal, + pos.getPosInOccurrence());*/ + } + + /** + * Handles rule application for automode. + * + * @param event + */ + @FXML + private void handleFocussedRuleApplication(ActionEvent event) { + // Synchronization for StaticSequentView + // parentController.setLastTacletActionID(parentController.getOwnID()); + //mediator.getUI().getProofControl() +// .startFocussedAutoMode(pos.getPosInOccurrence(), goal); + } + + /** + * Handles action of the 'Copy to clipboard' menu item. + * + * @param event + */ + @FXML + 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); + } + + /** + * Checks whether a string is a valid term abbreviation (is not empty and + * only contains 0-9, a-z, A-Z and underscore (_)). + * + * @param s the string to check + * @return true iff the string is a valid term abbreviation + */ + private boolean validateAbbreviation(String s) { + if (s == null || s.length() == 0) + return false; + for (int i = 0; i < s.length(); i++) { + if (!((s.charAt(i) <= '9' && s.charAt(i) >= '0') + || (s.charAt(i) <= 'z' && s.charAt(i) >= 'a') + || (s.charAt(i) <= 'Z' && s.charAt(i) >= 'A') + || s.charAt(i) == '_')) + return false; + } + return true; + } + + /** + * Handles the creation of a term abbreviation. + * + * @param event + */ + @FXML + private void handleCreateAbbreviation(ActionEvent event) { + if (occ.posInTerm() != null) { + final String oldTerm = occ.subTerm().toString(); + final String term = oldTerm.length() > 200 + ? oldTerm.substring(0, 200) : oldTerm; + abbreviationDialog("Create Abbreviation", + "Enter abbreviation for term: \n" + term + "\n", null); + } + } + + /** + * Handles the change of a term abbreviation. + * + * @param event + */ + @FXML + private void handleChangeAbbreviation(ActionEvent event) { + if (occ.posInTerm() != null) { + abbreviationDialog("Change Abbreviation", + "Enter abbreviation for term: \n" + + occ.subTerm().toString(), + notationInfo.getAbbrevMap().getAbbrev(occ.subTerm()).substring(1)); + } + } + + /** + * Opens a dialog that requires the input of a term abbreviation and iff a + * valid abbreviation is given applies it. + * + * @param header the header text for the dialog + * @param message the message of the dialog + * @param inputText preset text for the input line. Can be used to pass an already + * existing abbreviation to change. + */ + private void abbreviationDialog(String header, String message, + String inputText) { + TextInputDialog dialog = new TextInputDialog(inputText); + + // Get the Stage and add KeY Icon. + /* Stage stage = (Stage) dialog.getDialogPane().getScene().getWindow(); + stage.getIcons() + .add(new Image(NUIConstants.KEY_APPLICATION_WINDOW_ICON_PATH)); + dialog.setTitle("Abbreviation Dialog"); + dialog.setHeaderText(header); + dialog.setContentText(message); + Optional result = dialog.showAndWait(); + result.ifPresent(abbreviation -> { + if (abbreviation != null) { + if (!validateAbbreviation(abbreviation)) { + getMainApp().showAlert("Sorry", null, + "Only letters, numbers and '_' are allowed for Abbreviations", + AlertType.INFORMATION); + } else { + try { + AbbrevMap abbrevMap = mediator.getNotationInfo() + .getAbbrevMap(); + if (abbrevMap.containsTerm(occ.subTerm())) + abbrevMap.changeAbbrev(occ.subTerm(), abbreviation); + else + abbrevMap.put(occ.subTerm(), abbreviation, true); + parentController.forceRefresh(); + } catch (Exception e) { + getMainApp().showAlert("Sorry", + "Something has gone wrong.", e.getMessage(), + AlertType.ERROR); + } + } + } + });*/ + } + + /** + * Handles the enable of a term abbreviation. + * + * @param event + */ + @FXML + private void handleEnableAbbreviation(ActionEvent event) { + if (occ.posInTerm() != null) { + notationInfo.getAbbrevMap().setEnabled(occ.subTerm(), true); + // parentController.forceRefresh(); + } + } + + /** + * Handles the disable of a term abbreviation. + * + * @param event + */ + @FXML + private void handleDisableAbbreviation(ActionEvent event) { + if (occ.posInTerm() != null) { + notationInfo.getAbbrevMap().setEnabled(occ.subTerm(), false); + // parentController.forceRefresh(); + } + } + + /** + * Sorts the TacletApps with the given TacletAppComparator. + * + * @param finds the list to sort (will not be changed) + * @param comp the comparator + * @return the sorted list + */ + public static ImmutableList sort(ImmutableList finds, + TacletAppComparator comp) { + ImmutableList result = ImmutableSLList.nil(); + + List list = new ArrayList(finds.size()); + + for (final TacletApp app : finds) { + list.add(app); + } + + Collections.sort(list, comp); + + for (final TacletApp app : list) { + result = result.prepend(app); + } + + return result; + } +} diff --git a/src/main/java/edu/kit/formal/gui/controls/Utils.java b/src/main/java/edu/kit/formal/gui/controls/Utils.java index b23b60f8..e3c12760 100644 --- a/src/main/java/edu/kit/formal/gui/controls/Utils.java +++ b/src/main/java/edu/kit/formal/gui/controls/Utils.java @@ -21,6 +21,7 @@ import org.apache.logging.log4j.Logger; import java.io.IOException; import java.io.PrintWriter; import java.io.StringWriter; +import java.net.URL; import java.util.Random; /** @@ -121,9 +122,12 @@ public class Utils { } public static void createWithFXML(Object node) { - FXMLLoader loader = new FXMLLoader( - node.getClass().getResource(node.getClass().getSimpleName() + ".fxml") - ); + URL resource = node.getClass().getResource(node.getClass().getSimpleName() + ".fxml"); + if (resource == null) { + throw new IllegalArgumentException("Could not find FXML resource: " + node.getClass().getSimpleName() + ".fxml"); + } + + FXMLLoader loader = new FXMLLoader(resource); loader.setController(node); loader.setRoot(node); try { diff --git a/src/main/java/edu/kit/formal/interpreter/data/KeyData.java b/src/main/java/edu/kit/formal/interpreter/data/KeyData.java index e1b0f3f7..9d44bd1e 100644 --- a/src/main/java/edu/kit/formal/interpreter/data/KeyData.java +++ b/src/main/java/edu/kit/formal/interpreter/data/KeyData.java @@ -1,6 +1,7 @@ package edu.kit.formal.interpreter.data; import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import lombok.*; @@ -18,7 +19,6 @@ import java.util.function.Function; @RequiredArgsConstructor public class KeyData { private static final String SEPARATOR = " // "; - private final Node node; private final KeYEnvironment env; private final Proof proof; @@ -27,13 +27,28 @@ public class KeyData { programLinesLabel, programStatementsLabel, nameLabel; + private Goal goal; - public KeyData(KeyData data, Node node) { + public KeyData(KeyData data, Goal node) { env = data.env; //proofApi = data.proofApi; //scriptApi = data.scriptApi; this.proof = data.proof; - this.node = node; + this.goal = node; + } + + public KeyData(Goal g, KeYEnvironment environment, Proof proof) { + goal = g; + env = environment; + this.proof = proof; + } + + public KeyData(Node root, KeYEnvironment environment, Proof proof) { + this(proof.getGoal(root), environment, proof); + } + + public KeyData(KeyData kd, Node node) { + this(kd, kd.getProof().getGoal(node)); } public String getRuleLabel() { @@ -45,10 +60,10 @@ public class KeyData { private String constructLabel(Function projection) { StringBuilder sb = new StringBuilder(); - Node cur = node; + Node cur = getNode(); do { try { - String section = projection.apply(node); + String section = projection.apply(getNode()); if (section != null) { sb.append(section); sb.append(SEPARATOR); @@ -93,4 +108,11 @@ public class KeyData { } + public Goal getGoal() { + return goal; + } + + public Node getNode() { + return getGoal().node(); + } } diff --git a/src/main/resources/edu/kit/formal/gui/controls/TacletContextMenu.fxml b/src/main/resources/edu/kit/formal/gui/controls/TacletContextMenu.fxml new file mode 100644 index 00000000..84a8be1e --- /dev/null +++ b/src/main/resources/edu/kit/formal/gui/controls/TacletContextMenu.fxml @@ -0,0 +1,37 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/src/main/resources/edu/kit/formal/gui/debugger-ui.less b/src/main/resources/edu/kit/formal/gui/debugger-ui.less index f1a1099e..c77fd77a 100644 --- a/src/main/resources/edu/kit/formal/gui/debugger-ui.less +++ b/src/main/resources/edu/kit/formal/gui/debugger-ui.less @@ -118,14 +118,6 @@ /**********************************************************************************************************************/ - -.context-menu { - -fx-skin: "com.sun.javafx.scene.control.skin.ContextMenuSkin"; - -fx-font-family: sans-serif; - -fx-font-size: 9pt; -} - - .breakpoint-menu { -fx-skin: "com.sun.javafx.scene.control.skin.ContextMenuSkin"; -fx-font-family: sans-serif; @@ -223,11 +215,12 @@ .sequent-view { -fx-font-size: 14pt; - -fx-background-color: @base01; + -fx-background-color: @base2; + -fx-fill: black; .sequent-highlight { - -rtfx-background-color: @base1; - -fx-fill: @violet + -rtfx-background-color: @base0; + -fx-fill: black; } } @@ -287,4 +280,11 @@ &.POSTMORTEM { -fx-background-color: blueviolet; } -} \ No newline at end of file +} +/**********************************************************************************************************************/ + +.context-menu { + -fx-skin: "com.sun.javafx.scene.control.skin.ContextMenuSkin"; + -fx-font-family: sans-serif; + -fx-font-size: 9pt; +} -- GitLab