diff --git a/prism/src/userinterface/model/GUITextModelEditor.java b/prism/src/userinterface/model/GUITextModelEditor.java index 2f2ee19d..5bcab97c 100644 --- a/prism/src/userinterface/model/GUITextModelEditor.java +++ b/prism/src/userinterface/model/GUITextModelEditor.java @@ -448,22 +448,24 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen private void initContextMenu() { contextPopup = new JPopupMenu(); + // Edit menu stuff contextPopup.add(GUIPrism.getClipboardPlugin().getUndoAction()); contextPopup.add(GUIPrism.getClipboardPlugin().getRedoAction()); contextPopup.add(new JSeparator()); - contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getParseModel()); - contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getBuildModel()); - contextPopup.add(new JSeparator()); - contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getExportMenu()); - contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getViewMenu()); - contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getComputeMenu()); - contextPopup.add(new JSeparator()); contextPopup.add(GUIPrism.getClipboardPlugin().getCutAction()); contextPopup.add(GUIPrism.getClipboardPlugin().getCopyAction()); contextPopup.add(GUIPrism.getClipboardPlugin().getPasteAction()); contextPopup.add(GUIPrism.getClipboardPlugin().getDeleteAction()); contextPopup.add(new JSeparator()); contextPopup.add(GUIPrism.getClipboardPlugin().getSelectAllAction()); + contextPopup.add(new JSeparator()); + // Model menu stuff + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getParseModel()); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getBuildModel()); + contextPopup.add(new JSeparator()); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getExportMenu()); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getViewMenu()); + contextPopup.add(((GUIMultiModel)handler.getGUIPlugin()).getComputeMenu()); //contextPopup.add(actionJumpToError); //contextPopup.add(actionSearch);