From 795b2926d47b85c26d47f777403e0f1b1243cb69 Mon Sep 17 00:00:00 2001 From: Mark Kattenbelt Date: Fri, 31 Oct 2008 10:09:33 +0000 Subject: [PATCH] disabled insert menu (in model editor contex menu) git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@815 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/src/userinterface/model/GUITextModelEditor.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/prism/src/userinterface/model/GUITextModelEditor.java b/prism/src/userinterface/model/GUITextModelEditor.java index e69cfeb1..05e30cca 100644 --- a/prism/src/userinterface/model/GUITextModelEditor.java +++ b/prism/src/userinterface/model/GUITextModelEditor.java @@ -393,7 +393,7 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen if (editor.getContentType().equals("text/prism")) { - contextPopup.add(new JSeparator()); + JMenu insertMenu = new JMenu("Insert elements"); JMenu insertModelTypeMenu = new JMenu("Model type"); insertMenu.add(insertModelTypeMenu); @@ -405,7 +405,8 @@ public class GUITextModelEditor extends GUIModelEditor implements DocumentListen insertModelTypeMenu.add(insertDTMC); insertModelTypeMenu.add(insertCTMC); insertModelTypeMenu.add(insertMDP); - contextPopup.add(insertMenu); + //contextPopup.add(new JSeparator()); + //contextPopup.add(insertMenu); } }