Source Code Cross Referenced for KeyMenuExtension.java in  » Testing » KeY » de » uka » ilkd » key » casetool » together » scripts » menuextension » Java Source Code / Java DocumentationJava Source Code and Java Documentation

Java Source Code / Java Documentation
1. 6.0 JDK Core
2. 6.0 JDK Modules
3. 6.0 JDK Modules com.sun
4. 6.0 JDK Modules com.sun.java
5. 6.0 JDK Modules sun
6. 6.0 JDK Platform
7. Ajax
8. Apache Harmony Java SE
9. Aspect oriented
10. Authentication Authorization
11. Blogger System
12. Build
13. Byte Code
14. Cache
15. Chart
16. Chat
17. Code Analyzer
18. Collaboration
19. Content Management System
20. Database Client
21. Database DBMS
22. Database JDBC Connection Pool
23. Database ORM
24. Development
25. EJB Server geronimo
26. EJB Server GlassFish
27. EJB Server JBoss 4.2.1
28. EJB Server resin 3.1.5
29. ERP CRM Financial
30. ESB
31. Forum
32. GIS
33. Graphic Library
34. Groupware
35. HTML Parser
36. IDE
37. IDE Eclipse
38. IDE Netbeans
39. Installer
40. Internationalization Localization
41. Inversion of Control
42. Issue Tracking
43. J2EE
44. JBoss
45. JMS
46. JMX
47. Library
48. Mail Clients
49. Net
50. Parser
51. PDF
52. Portal
53. Profiler
54. Project Management
55. Report
56. RSS RDF
57. Rule Engine
58. Science
59. Scripting
60. Search Engine
61. Security
62. Sevlet Container
63. Source Control
64. Swing Library
65. Template Engine
66. Test Coverage
67. Testing
68. UML
69. Web Crawler
70. Web Framework
71. Web Mail
72. Web Server
73. Web Services
74. Web Services apache cxf 2.0.1
75. Web Services AXIS2
76. Wiki Engine
77. Workflow Engines
78. XML
79. XML UI
Java
Java Tutorial
Java Open Source
Jar File Download
Java Articles
Java Products
Java by API
Photoshop Tutorials
Maya Tutorials
Flash Tutorials
3ds-Max Tutorials
Illustrator Tutorials
GIMP Tutorials
C# / C Sharp
C# / CSharp Tutorial
C# / CSharp Open Source
ASP.Net
ASP.NET Tutorial
JavaScript DHTML
JavaScript Tutorial
JavaScript Reference
HTML / CSS
HTML CSS Reference
C / ANSI-C
C Tutorial
C++
C++ Tutorial
Ruby
PHP
Python
Python Tutorial
Python Open Source
SQL Server / T-SQL
SQL Server / T-SQL Tutorial
Oracle PL / SQL
Oracle PL/SQL Tutorial
PostgreSQL
SQL / MySQL
MySQL Tutorial
VB.Net
VB.Net Tutorial
Flash / Flex / ActionScript
VBA / Excel / Access / Word
XML
XML Tutorial
Microsoft Office PowerPoint 2007 Tutorial
Microsoft Office Excel 2007 Tutorial
Microsoft Office Word 2007 Tutorial
Java Source Code / Java Documentation » Testing » KeY » de.uka.ilkd.key.casetool.together.scripts.menuextension 
Source Cross Referenced  Class Diagram Java Document (Java Doc) 


001:        // This file is part of KeY - Integrated Deductive Software Design
002:        // Copyright (C) 2001-2007 Universitaet Karlsruhe, Germany
003:        //                         Universitaet Koblenz-Landau, Germany
004:        //                         Chalmers University of Technology, Sweden
005:        //
006:        // The KeY system is protected by the GNU General Public License. 
007:        // See LICENSE.TXT for details.
008:        //
009:        //
010:
011:        /**
012:         * Creates the KeY-menus to be used in the Together-Tool.
013:         * Assumes, that classes of form GlobalMenu<No>, ClassMenu<No>, OpMenu<No>
014:         * reside in the same package.
015:         */package de.uka.ilkd.key.casetool.together.scripts.menuextension;
016:
017:        import java.util.ResourceBundle;
018:
019:        import javax.swing.ImageIcon;
020:        import javax.swing.JOptionPane;
021:
022:        import com.togethersoft.openapi.ide.IdeContext;
023:        import com.togethersoft.openapi.ide.command.*;
024:        import com.togethersoft.openapi.ide.message.IdeMessageManagerAccess;
025:        import com.togethersoft.openapi.ide.message.IdeMessageType;
026:        import com.togethersoft.openapi.ide.window.IdeWindowManager;
027:        import com.togethersoft.openapi.ide.window.IdeWindowManagerAccess;
028:
029:        import de.uka.ilkd.key.casetool.together.keydebugclassloader.KeyScript;
030:        import de.uka.ilkd.key.util.Debug;
031:        import de.uka.ilkd.key.util.KeYResourceManager;
032:
033:        public class KeyMenuExtension extends KeyScript {
034:
035:            /**
036:             * Program resources.
037:             */
038:            protected static final ResourceBundle resources;
039:            static {
040:                try {
041:                    resources = ResourceBundle.getBundle(KeyMenuExtension.class
042:                            .getName());
043:                } catch (ExceptionInInitializerError e) {
044:                    JOptionPane
045:                            .showMessageDialog(
046:                                    null,
047:                                    "An error occured initializing "
048:                                            + KeyMenuExtension.class.getName()
049:                                            + ".\nThe package seems corrupt or a resource is missing, aborting\n"
050:                                            + e, "Error",
051:                                    JOptionPane.ERROR_MESSAGE);
052:                    throw new InternalError(e.getMessage())/*.initCause(e)*/;
053:                } catch (LinkageError le) {
054:                    JOptionPane
055:                            .showMessageDialog(
056:                                    null,
057:                                    "An error occured in linking class "
058:                                            + KeyMenuExtension.class.getName()
059:                                            + ".\nThe package seems corrupt or a resource is missing, aborting\n"
060:                                            + le, "Error",
061:                                    JOptionPane.ERROR_MESSAGE);
062:                    throw new InternalError(le.getMessage())/*.initCause(e)*/;
063:                }
064:            }
065:
066:            // auxiliary variables
067:            IdeCommandManager comMan = IdeCommandManagerAccess
068:                    .getCommandManager();
069:            IdeWindowManager winMan = IdeWindowManagerAccess.getWindowManager();
070:            String myPackageName = this .getClass().getPackage().getName();
071:
072:            /** Reactivate the script */
073:            public void run1(IdeContext context) {
074:                autorun1();
075:            }
076:
077:            /**
078:             * Activate the script (cmp. KeyScript)
079:             */
080:            public void autorun1() {
081:                de.uka.ilkd.key.gui.Main.configureLogger();
082:                IdeMessageManagerAccess.printMessage(
083:                        IdeMessageType.INFORMATION,
084:                        "KeyMenuExtension new script: started");
085:                createAllMenus();
086:                de.uka.ilkd.key.proof.init.OCLProofOblInput
087:                        .setModelManager(de.uka.ilkd.key.casetool.together.TogetherModelManager.INSTANCE);
088:                IdeMessageManagerAccess.printMessage(
089:                        IdeMessageType.INFORMATION,
090:                        "KeyMenuExtension script: finished");
091:            }
092:
093:            private void createAllMenus() {
094:                //XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
095:                //xxx to re-activate the KeY menu group uncomment the following line
096:                //XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX
097:                //       	createGlobalMenus();
098:                // instead of the XMI transform menu point we create  "about" and "license" menue points
099:                createGlobalMenus2();
100:                createClassContextMenus();
101:                createOperationContextMenus();
102:            }
103:
104:            //control variables for global menus
105:            static int NUMGLOBALMENUTYPES = 2;
106:            static int NUMGLOBALMENUGROUPS = 1;
107:            public IdeCommandGroup[][] myGlobalMenuGroups = new IdeCommandGroup[NUMGLOBALMENUTYPES][NUMGLOBALMENUGROUPS];
108:            IdeCommandGroup myMainMenuGroup;
109:            IdeCommandGroup myMainToolbarGroup;
110:
111:            private void createGlobalMenus() {
112:                String[] globalMenuLocation = new String[] { "mainToolbar",
113:                        "mainMenu" };
114:
115:                //creates the group-item in the global menu
116:                myMainMenuGroup = comMan.createGroup("IDOf"
117:                        + globalMenuLocation[1], new IdeCommandConstraints(
118:                        "location=" + globalMenuLocation[1]),
119:                        new IdeCommandCheckListener() {
120:                            public void checkStatus(IdeCommandEvent event) {
121:                                myMainMenuGroup.setText("KeY");
122:                            }
123:                        });
124:
125:                // The main toolbar is extended with our own icon (KeY-button)
126:                //	String tjextpath = System.getProperty("KeyPathTjext");
127:                //	final ImageIcon icon = new ImageIcon(tjextpath + "/de/uka/ilkd/key/casetool/together/scripts/menuextension/key-color-icon-small.gif");
128:
129:                final ImageIcon icon = KeYResourceManager.getManager()
130:                        .createImageIcon(this , "key-color-icon-small.gif");
131:                myMainToolbarGroup = comMan.createGroup("IDOf"
132:                        + globalMenuLocation[0], new IdeCommandConstraints(
133:                        "location=" + globalMenuLocation[0]),
134:                        new IdeCommandCheckListener() {
135:                            // we have to mention checkStatus because of IdeCommandCheckListener is
136:                            // an interface, not a class where you can create instances of
137:                            public void checkStatus(IdeCommandEvent event) {
138:                            }
139:                        });
140:
141:                //The icon is set to the new ToolbarGroup
142:                myMainToolbarGroup.setIcon(IdeCommandIconType.PRESSED, icon);
143:                myMainToolbarGroup.setIcon(IdeCommandIconType.DEFAULT, icon);
144:
145:                // All used Items in the global menu have a name of form "GlobalMenu.."
146:                // That classes are in the same package as that class.
147:                String globalMenuRootCN = myPackageName + "." + "GlobalMenu";
148:                for (int typeI = 0; typeI < NUMGLOBALMENUTYPES; typeI++) {
149:                    for (int group = 1; group < (NUMGLOBALMENUGROUPS + 1); group++) {
150:                        myGlobalMenuGroups[typeI][(group - 1)] = comMan
151:                                .createGroup("IDOfTheMainMenuSubGroup"
152:                                        + globalMenuLocation[typeI] + group,
153:                                        new IdeCommandConstraints("parent=IDOf"
154:                                                + globalMenuLocation[typeI]
155:                                                + ", location="
156:                                                + globalMenuLocation[typeI]),
157:                                        // 				new IdeCommandCheckListener() {
158:                                        // 					public void checkStatus(IdeCommandEvent event) {
159:                                        // 					    // here we create an instance of classes like GlobalMenueGroup1
160:                                        // 					    ( myGlobalMenuGroups[typeI][(group-1)]).setText(((GlobalMenue) Class.forName(globalMenueRootCN + "Group" + group).newInstance()).getMenueEntry());               
161:                                        // 					}
162:                                        // 				    }
163:                                        //				 new KeyMenuIdeCmdListener(this, typeI, (group-1), globalMenuRootCN) 	   
164:                                        new GlobalMenuIdeAdapter(this , null,
165:                                                typeI, group, 0,
166:                                                globalMenuRootCN));
167:
168:                        // how many entries have the groups
169:                        int groupElemNum;
170:                        if (group == 1) {
171:                            groupElemNum = 1;
172:                        } else if (group == 2) {
173:                            groupElemNum = 0;
174:                        } else if (group == 3) {
175:                            groupElemNum = 0;
176:                        } else {
177:                            groupElemNum = 0;
178:                        }
179:
180:                        for (int groupItem = 1; groupItem < (groupElemNum + 1); groupItem++) {
181:                            // generating the elements of the groups
182:
183:                            // at first we generate an adapter to cover the functionality
184:
185:                            // 		    IdeCommandAdapter actAdapter = new IdeCommandAdapter() {
186:                            // 			    public void actionPerformed(IdeCommandEvent event) { 
187:                            // 				// here we create an instance of classes like GlobalMenuePoint1_1
188:                            // 				try{
189:                            // 				    ((GlobalMenue) Class.forName(globalMenueRootCN + "Point" + group + "_" + groupItem).newInstance()).run(winMan);
190:                            // 				}catch(Exception e){
191:                            // 				    System.err.println("KeYError: " + e);
192:                            //                                  e.printStackTrace();
193:                            // 				}
194:                            // 			    }
195:                            // 			};
196:
197:                            GlobalMenuIdeAdapter actAdapter = new GlobalMenuIdeAdapter(
198:                                    this , winMan, 0, group, groupItem,
199:                                    globalMenuRootCN);
200:
201:                            // now the menuentry of the actual group
202:                            String optionalPlaceAfterString = "";
203:                            if (groupItem > 1) {
204:                                optionalPlaceAfterString = ", placeAfter = IDOfItem"
205:                                        + globalMenuLocation[typeI]
206:                                        + group
207:                                        + "_" + (groupItem - 1);
208:                            }
209:
210:                            IdeCommandItem groupElement = comMan
211:                                    .createItem(
212:                                            "IDOfItem"
213:                                                    + globalMenuLocation[typeI]
214:                                                    + group + "_" + groupItem,
215:                                            new IdeCommandConstraints(
216:                                                    "parent=IDOfTheMainMenuSubGroup"
217:                                                            + globalMenuLocation[typeI]
218:                                                            + group
219:                                                            + optionalPlaceAfterString
220:                                                            + ", location="
221:                                                            + globalMenuLocation[typeI]),
222:                                            actAdapter);
223:
224:                            // here we create an instance of classes like GlobalMenuPoint1_1
225:                            try {
226:                                groupElement.setText(((GlobalMenu) Class
227:                                        .forName(
228:                                                globalMenuRootCN + "Point"
229:                                                        + group + "_"
230:                                                        + groupItem)
231:                                        .newInstance()).getMenuEntry());
232:
233:                            } catch (ClassNotFoundException cnfe) {
234:                                System.err
235:                                        .println("keymenuextension: class cannot be located");
236:                                System.err
237:                                        .println("The exception was: " + cnfe);
238:                                cnfe.printStackTrace();
239:                            } catch (ExceptionInInitializerError ei) {
240:                                System.err
241:                                        .println("keymenuextension: the initialization provoked "
242:                                                + "by this method fails.");
243:                                System.err.println("The exception was: " + ei);
244:                                ei.printStackTrace();
245:                            } catch (IllegalAccessException iae) {
246:                                System.err
247:                                        .println("keymenuextension: class or "
248:                                                + "initializer is not accessible.");
249:                                System.err.println("The exception was: " + iae);
250:                                iae.printStackTrace();
251:                            } catch (InstantiationException ie) {
252:                                System.err
253:                                        .println("keymenuextension: class tried to\n"
254:                                                + "instantiate represents an abstract class, an interface,"
255:                                                + "an array class, a primitive type, or void; or if the"
256:                                                + "instantiation fails for some other reason.");
257:                                System.err.println("The exception was: " + ie);
258:                                ie.printStackTrace();
259:                            } catch (SecurityException se) {
260:                                System.err
261:                                        .println("keymenuextension: no permission to create"
262:                                                + "a new instance");
263:                                System.err.println("The exception was: " + se);
264:                                se.printStackTrace();
265:                            } catch (LinkageError le) {
266:                                System.err
267:                                        .println("keymenuextension: linkage failed");
268:                                System.err.println("The exception was: " + le);
269:                                le.printStackTrace();
270:                            }
271:
272:                            groupElement.setEnabled(true);
273:                            groupElement.setVisible(true);
274:                            groupElement.setSeparatorAfter(true);
275:                        }
276:                    }
277:                }
278:            }
279:
280:            private void createGlobalMenus2() {
281:                String[] globalMenuLocation = new String[] { "mainToolbar",
282:                        "mainMenu" };
283:
284:                //creates the group-item in the global menu
285:                myMainMenuGroup = comMan.createGroup("IDOf"
286:                        + globalMenuLocation[1], new IdeCommandConstraints(
287:                        "location=" + globalMenuLocation[1]),
288:                        new IdeCommandCheckListener() {
289:                            public void checkStatus(IdeCommandEvent event) {
290:                                myMainMenuGroup.setText("KeY");
291:                            }
292:                        });
293:
294:                final ImageIcon icon = KeYResourceManager.getManager()
295:                        .createImageIcon(this , "key-color-icon-small.gif");
296:                myMainToolbarGroup = comMan.createGroup("IDOf"
297:                        + globalMenuLocation[0], new IdeCommandConstraints(
298:                        "location=" + globalMenuLocation[0]),
299:                        new IdeCommandCheckListener() {
300:                            public void checkStatus(IdeCommandEvent event) {
301:                            }
302:                        });
303:
304:                //The icon is set to the new ToolbarGroup
305:                myMainToolbarGroup.setIcon(IdeCommandIconType.PRESSED, icon);
306:                myMainToolbarGroup.setIcon(IdeCommandIconType.DEFAULT, icon);
307:
308:                // All used Items in the global menu have a name of form "GlobalMenu.."
309:                // That classes are in the same package as that class.
310:                String globalMenuRootCN = myPackageName + "." + "GlobalMenu";
311:                for (int typeI = 0; typeI < NUMGLOBALMENUTYPES; typeI++) {
312:                    int group = 1;
313:
314:                    // now the menuentry of the actual group	
315:
316:                    IdeCommandItem groupElement1 = comMan.createItem(
317:                            "IDOfMenuPoint1" + globalMenuLocation[typeI]
318:                                    + group, new IdeCommandConstraints(
319:                                    "parent=IDOf" + globalMenuLocation[typeI]
320:                                            + ", location="
321:                                            + globalMenuLocation[typeI]),
322:                            new GlobalMenuIdeAdapter(this , winMan, typeI,
323:                                    group, 2, globalMenuRootCN));
324:                    IdeCommandItem groupElement2 = comMan
325:                            .createItem("IDOfMeuPoint2"
326:                                    + globalMenuLocation[typeI] + group,
327:                                    new IdeCommandConstraints("parent=IDOf"
328:                                            + globalMenuLocation[typeI]
329:                                            + ", location="
330:                                            + globalMenuLocation[typeI]),
331:                                    new GlobalMenuIdeAdapter(this , winMan,
332:                                            typeI, group, 3, globalMenuRootCN));
333:                    IdeCommandItem groupElement4 = comMan
334:                            .createItem("IDOfMeuPoint4"
335:                                    + globalMenuLocation[typeI] + group,
336:                                    new IdeCommandConstraints("parent=IDOf"
337:                                            + globalMenuLocation[typeI]
338:                                            + ", location="
339:                                            + globalMenuLocation[typeI]),
340:                                    new GlobalMenuIdeAdapter(this , winMan,
341:                                            typeI, group, 4, globalMenuRootCN));
342:                    IdeCommandItem groupElement5 = comMan
343:                            .createItem("IDOfMeuPoint5"
344:                                    + globalMenuLocation[typeI] + group,
345:                                    new IdeCommandConstraints("parent=IDOf"
346:                                            + globalMenuLocation[typeI]
347:                                            + ", location="
348:                                            + globalMenuLocation[typeI]),
349:                                    new GlobalMenuIdeAdapter(this , winMan,
350:                                            typeI, group, 5, globalMenuRootCN));
351:                    IdeCommandItem groupElement6 = comMan
352:                            .createItem("IDOfMeuPoint6"
353:                                    + globalMenuLocation[typeI] + group,
354:                                    new IdeCommandConstraints("parent=IDOf"
355:                                            + globalMenuLocation[typeI]
356:                                            + ", location="
357:                                            + globalMenuLocation[typeI]),
358:                                    new GlobalMenuIdeAdapter(this , winMan,
359:                                            typeI, group, 6, globalMenuRootCN));
360:
361:                    try {
362:                        groupElement1.setText(((GlobalMenu) Class.forName(
363:                                globalMenuRootCN + "Point1_2").newInstance())
364:                                .getMenuEntry());
365:                        groupElement2.setText(((GlobalMenu) Class.forName(
366:                                globalMenuRootCN + "Point1_3").newInstance())
367:                                .getMenuEntry());
368:                        groupElement4.setText(((GlobalMenu) Class.forName(
369:                                globalMenuRootCN + "Point1_4").newInstance())
370:                                .getMenuEntry());
371:                        groupElement5.setText(((GlobalMenu) Class.forName(
372:                                globalMenuRootCN + "Point1_5").newInstance())
373:                                .getMenuEntry());
374:                        groupElement6.setText(((GlobalMenu) Class.forName(
375:                                globalMenuRootCN + "Point1_6").newInstance())
376:                                .getMenuEntry());
377:                    } catch (ClassNotFoundException cnfe) {
378:                        System.err
379:                                .println("keymenuextension: class cannot be located");
380:                        System.err.println("The exception was: " + cnfe);
381:                        cnfe.printStackTrace();
382:                    } catch (ExceptionInInitializerError ei) {
383:                        System.err
384:                                .println("keymenuextension: the initialization provoked "
385:                                        + "by this method fails.");
386:                        System.err.println("The exception was: " + ei);
387:                        ei.printStackTrace();
388:                    } catch (IllegalAccessException iae) {
389:                        System.err.println("keymenuextension: class or "
390:                                + "initializer is not accessible.");
391:                        System.err.println("The exception was: " + iae);
392:                        iae.printStackTrace();
393:                    } catch (InstantiationException ie) {
394:                        System.err
395:                                .println("keymenuextension: class tried to\n"
396:                                        + "instantiate represents an abstract class, an interface,"
397:                                        + "an array class, a primitive type, or void; or if the"
398:                                        + "instantiation fails for some other reason.");
399:                        System.err.println("The exception was: " + ie);
400:                        ie.printStackTrace();
401:                    } catch (SecurityException se) {
402:                        System.err
403:                                .println("keymenuextension: no permission to create"
404:                                        + "a new instance");
405:                        System.err.println("The exception was: " + se);
406:                        se.printStackTrace();
407:                    } catch (LinkageError le) {
408:                        System.err.println("keymenuextension: linkage failed");
409:                        System.err.println("The exception was: " + le);
410:                        le.printStackTrace();
411:                    }
412:
413:                    groupElement1.setEnabled(true);
414:                    groupElement1.setVisible(true);
415:                    groupElement1.setSeparatorAfter(false);
416:                    groupElement2.setEnabled(true);
417:                    groupElement2.setVisible(true);
418:                    groupElement2.setSeparatorAfter(true);
419:                    groupElement4.setEnabled(true);
420:                    groupElement4.setVisible(true);
421:                    groupElement4.setSeparatorAfter(false);
422:                    groupElement5.setVisible(true);
423:                    groupElement5.setSeparatorAfter(true);
424:                    groupElement6.setVisible(true);
425:                    groupElement6.setSeparatorAfter(false);
426:                }
427:            }
428:
429:            // menus for the context of a class symbol
430:
431:            IdeCommandGroup myClassGroup;
432:
433:            // how many classmenuitems do we have?
434:            static int NUMCLASSMENUITEMS = Integer.parseInt(resources
435:                    .getString("key.menu.class.menuitem-count"));
436:            static {
437:                Debug.out("MenuExtension uses " + NUMCLASSMENUITEMS
438:                        + " class menu items");
439:            }
440:
441:            // IdeCommandItem is used in class ClassMenuIdeAdapter
442:            public IdeCommandItem[] myClassItem = new IdeCommandItem[NUMCLASSMENUITEMS];
443:
444:            private void createClassContextMenus() {
445:
446:                //creates the group-item in the context-menu
447:                myClassGroup = comMan
448:                        .createGroup(
449:                                "IDOfTheClassGroup",
450:                                new IdeCommandConstraints(
451:                                        "context = element, shapeType=Class, location=popupMenu"),
452:                                new IdeCommandCheckListener() {
453:                                    public void checkStatus(
454:                                            IdeCommandEvent event) {
455:                                        // here we can look if we have a class or interface, ... omitted
456:                                        myClassGroup.setText("KeY");
457:
458:                                    }
459:                                });
460:
461:                // All used Items in the class menu have a name 
462:                // starting with the following
463:                String classMenuRootCN = myPackageName + "." + "ClassMenu";
464:
465:                for (int groupElementNo = 1; groupElementNo < (NUMCLASSMENUITEMS + 1); groupElementNo++) {
466:                    String optionalPlaceAfterString = "";
467:                    if (groupElementNo > 1) {
468:                        optionalPlaceAfterString = ", placeAfter = IDOfClassItem"
469:                                + (groupElementNo - 1);
470:                    }
471:
472:                    // adding the elements to the class menu
473:
474:                    ClassMenuIdeAdapter actClassAdapter = new ClassMenuIdeAdapter(
475:                            this , winMan, groupElementNo, classMenuRootCN);
476:
477:                    myClassItem[groupElementNo - 1] = comMan.createItem(
478:                            "IDOfClassItem" + groupElementNo,
479:                            new IdeCommandConstraints("context = element, "
480:                                    + "parent=IDOfTheClassGroup"
481:                                    + optionalPlaceAfterString
482:                                    + ", location=popupMenu"), actClassAdapter);
483:                }
484:            }
485:
486:            // menus for the context of a operation
487:
488:            IdeCommandGroup myOpGroup;
489:            IdeCommandGroup[] myOpSubGroups;
490:            // how many opmenuitems do we have?
491:            static int NUMOPMENUITEMS = Integer.parseInt(resources
492:                    .getString("key.menu.op.menuitem-count"));
493:            static {
494:                Debug.out("MenuExtension uses " + NUMOPMENUITEMS
495:                        + " op menu items");
496:            }
497:
498:            // IdeCommandItem is used in class OpMenuIdeAdapter
499:            public IdeCommandItem[] myOpItem = new IdeCommandItem[NUMOPMENUITEMS];
500:
501:            private void createOperationContextMenus() {
502:                //creates the group-item in the context-menu
503:                myOpGroup = comMan
504:                        .createGroup(
505:                                "IDOfTheOpGroup",
506:                                new IdeCommandConstraints(
507:                                        "context = element, shapeType=Operation, location=popupMenu"),
508:                                new IdeCommandCheckListener() {
509:                                    public void checkStatus(
510:                                            IdeCommandEvent event) {
511:                                        // here we can look if we have a class or interface, ... omitted
512:                                        myOpGroup.setText("KeY");
513:                                    }
514:                                });
515:
516:                // All used Items in the class menu have a name 
517:                // starting with the following
518:                String opMenuRootCN = myPackageName + "." + "OpMenu";
519:                String subMenuIDs[] = new String[NUMOPMENUITEMS];
520:                //	String optionalPlaceAfterString = "";
521:
522:                for (int groupElementNo = 1; groupElementNo < (NUMOPMENUITEMS + 1); groupElementNo++) {
523:                    try {
524:                        subMenuIDs[groupElementNo - 1] = ((OpMenu) Class
525:                                .forName(
526:                                        opMenuRootCN + "Point" + groupElementNo)
527:                                .newInstance()).getSubMenuName();
528:                    } catch (Exception ie) {
529:                        Debug.fail("Class " + opMenuRootCN + "Point"
530:                                + groupElementNo + " could not be loaded");
531:                    }
532:                    if (subMenuIDs[groupElementNo - 1] != null)
533:                        subMenuIDs[groupElementNo - 1] = "IDOf"
534:                                + subMenuIDs[groupElementNo - 1];
535:
536:                }
537:
538:                for (int groupElementNo = 1; groupElementNo < (NUMOPMENUITEMS + 1); groupElementNo++) {
539:                    // adding the elements to the class menu
540:
541:                    //	    optionalPlaceAfterString = "";
542:
543:                    // NOT NECESSARY - items are created in order 
544:                    //	    if ( groupElementNo > 1 ) {
545:                    //		optionalPlaceAfterString = ", placeAfter = IDOfOpItem" + 
546:                    //		    (groupElementNo-1 );
547:                    //	    }
548:
549:                    // adding the elements to the op menu (only those not in any submenu)
550:                    if (subMenuIDs[groupElementNo - 1] == null) {
551:                        OpMenuIdeAdapter actOpAdapter = new OpMenuIdeAdapter(
552:                                this , winMan, groupElementNo, opMenuRootCN);
553:
554:                        myOpItem[groupElementNo - 1] = comMan.createItem(
555:                                "IDOfOpItem" + groupElementNo,
556:                                new IdeCommandConstraints(
557:                                        "context = element, parent=IDOfTheOpGroup"
558:                                                +
559:                                                //		      optionalPlaceAfterString +
560:                                                ", location=popupMenu"),
561:                                actOpAdapter);
562:
563:                    }
564:                }
565:
566:                String[] opGroupIDs = new String[] { "horizontal", "vertical" };
567:                String[] opGroupNames = new String[] {
568:                        "Horizontal Proof Obligations",
569:                        "Vertical Proof Obligations" };
570:                myOpSubGroups = new IdeCommandGroup[opGroupIDs.length];
571:
572:                for (int i = 0; i < opGroupIDs.length; i++) {
573:                    myOpSubGroups[i] = comMan
574:                            .createGroup(
575:                                    "IDOf" + opGroupIDs[i],
576:                                    new IdeCommandConstraints(
577:                                            "context = element, parent=IDOfTheOpGroup, location=popupMenu"),
578:                                    new IdeCommandCheckListener() {
579:                                        public void checkStatus(
580:                                                IdeCommandEvent event) {
581:                                            IdeCommandItem item = event
582:                                                    .getCommandItem();
583:                                            item.setVisible(true);
584:                                        }
585:                                    });
586:                    myOpSubGroups[i].setText(opGroupNames[i]);
587:                }
588:
589:                for (int groupElementNo = 1; groupElementNo < (NUMOPMENUITEMS + 1); groupElementNo++) {
590:
591:                    //	    optionalPlaceAfterString = "";
592:
593:                    // NOT NECESSARY - items are created in order 
594:                    //	    if ( groupElementNo > 1 ) {
595:                    //		optionalPlaceAfterString = ", placeAfter = IDOfOpItem" + 
596:                    //		    (groupElementNo-1 );
597:                    //	    }
598:
599:                    // adding the elements to the op menu (only those in submenus)
600:
601:                    if (subMenuIDs[groupElementNo - 1] != null) {
602:                        OpMenuIdeAdapter actOpAdapter = new OpMenuIdeAdapter(
603:                                this , winMan, groupElementNo, opMenuRootCN);
604:
605:                        myOpItem[groupElementNo - 1] = comMan
606:                                .createItem(
607:                                        "IDOfOpItem" + groupElementNo,
608:                                        new IdeCommandConstraints(
609:                                                "context = element, parent="
610:                                                        + subMenuIDs[groupElementNo - 1]
611:                                                        +
612:                                                        //		      optionalPlaceAfterString +
613:                                                        ", location=popupMenu"),
614:                                        actOpAdapter);
615:
616:                    }
617:                }
618:
619:            }
620:        }
w___w__w___._j__a_v_a_2s._c__om___ | Contact Us
Copyright 2009 - 12 Demo Source and Support. All rights reserved.
All other trademarks are property of their respective owners.