From 52bb6f33dede545b242a841af4975a3321183211 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 23 Dec 2008 10:59:51 +0000 Subject: [PATCH] Changed order in model context menu. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@912 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- .../userinterface/model/GUITextModelEditor.java | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) 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);