001: //Copyright (c) Hans-Joachim Daniels 2005
002: //
003: //This program is free software; you can redistribute it and/or modify
004: //it under the terms of the GNU General Public License as published by
005: //the Free Software Foundation; either version 2 of the License, or
006: //(at your option) any later version.
007: //
008: //You can either finde the file LICENSE or LICENSE.TXT in the source
009: //distribution or in the .jar file of this applicationpackage de.uka.ilkd.key.ocl.gf;
010:
011: package de.uka.ilkd.key.ocl.gf;
012:
013: import java.awt.Color;
014: import java.awt.Font;
015: import java.awt.event.*;
016: import java.util.*;
017: import java.util.logging.Level;
018: import java.util.logging.Logger;
019:
020: import javax.swing.*;
021:
022: /**
023: * Takes care of managing the commands, that GF sent,
024: * including subcategories and their menus.
025: * Manages the graphical lists. To display them, they are reachable
026: * via getRefinementListsContainer().
027: * @author hdaniels
028: */
029: class RefinementMenu {
030: /**
031: * logs things like selections and key events
032: */
033: private static Logger logger = Logger
034: .getLogger(RefinementMenu.class.getName());
035:
036: /**
037: * the editor of which this menu is part of
038: */
039: final private GFEditor2 editor;
040: /**
041: * the content of the refinementMenu
042: */
043: public DefaultListModel listModel = new DefaultListModel();
044: /**
045: * The list of current refinement options
046: */
047: private JList refinementList = new JList(this .listModel);
048: /**
049: * to store the Vectors which contain the display names for the
050: * ListModel for refinementSubcatList for the different
051: * subcategory menus.
052: * The key is the shortname String, the value the Vector with the
053: * display Strings
054: */
055: private Hashtable subcatListModelHashtable = new Hashtable();
056: /**
057: * this ListModel gets refilled every time a %WHATEVER command,
058: * which stands for a shortname for a subcategory of commands
059: * in the ListModel of refinementList, is selected there
060: */
061: private DefaultListModel refinementSubcatListModel = new DefaultListModel();
062: /**
063: * The list of current refinement options in the subcategory menu
064: */
065: private JList refinementSubcatList = new JList(
066: this .refinementSubcatListModel);
067: /**
068: * the scrollpane containing the refinement subcategory
069: */
070: private JScrollPane refinementSubcatPanel = new JScrollPane(
071: this .refinementSubcatList);
072: /**
073: * store what the shorthand name for the current subcat is
074: */
075: private String whichSubcat;
076: /**
077: * stores the two refinement JLists
078: */
079: private JSplitPane refinementListsContainer;
080: /**
081: * the scrollpane containing the refinements
082: */
083: private JScrollPane refinementPanel = new JScrollPane(
084: this .refinementList);
085: /**
086: * here the GFCommand objects are stored
087: */
088: private Vector gfcommands = new Vector();
089: /**
090: * The cached popup menu containing the same stuff as the refinement list
091: */
092: public JPopupMenu popup2 = new JPopupMenu();
093:
094: /**
095: * Creates the panels for the refinement (subcat) menu
096: * @param editor the editor, that the refinement menu is part of
097: */
098: protected RefinementMenu(GFEditor2 editor) {
099: this .editor = editor;
100: refinementListsContainer = new JSplitPane(
101: JSplitPane.HORIZONTAL_SPLIT, refinementPanel,
102: refinementSubcatPanel);
103: refinementList
104: .setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
105:
106: final MouseListener mlRefinementList = new MouseAdapter() {
107: public void mouseClicked(MouseEvent e) {
108: refinementList
109: .setSelectionBackground(refinementSubcatList
110: .getSelectionBackground());
111: boolean doubleClick = (e.getClickCount() == 2);
112: listAction(refinementList, refinementList
113: .locationToIndex(e.getPoint()), doubleClick);
114: }
115: };
116: refinementList.addMouseListener(mlRefinementList);
117: refinementList.addKeyListener(new KeyListener() {
118: /** Handle the key pressed event for the refinement list. */
119: public void keyPressed(KeyEvent e) {
120: int keyCode = e.getKeyCode();
121: if (logger.isLoggable(Level.FINER)) {
122: logger.finer("Key pressed: " + e.toString());
123: }
124:
125: int index = refinementList.getSelectedIndex();
126: if (index == -1) {
127: //nothing selected, so nothing to be seen here, please move along
128: } else if (keyCode == KeyEvent.VK_ENTER) {
129: listAction(refinementList, refinementList
130: .getSelectedIndex(), true);
131: } else if (keyCode == KeyEvent.VK_DOWN
132: && index < listModel.getSize() - 1) {
133: listAction(refinementList, index + 1, false);
134: } else if (keyCode == KeyEvent.VK_UP && index > 0) {
135: listAction(refinementList, index - 1, false);
136: } else if (keyCode == KeyEvent.VK_RIGHT) {
137: if (refinementSubcatList.getModel().getSize() > 0) {
138: refinementSubcatList.requestFocusInWindow();
139: refinementSubcatList.setSelectedIndex(0);
140: refinementList
141: .setSelectionBackground(Color.GRAY);
142: }
143: }
144: }
145:
146: /**
147: * Handle the key typed event.
148: * We are not really interested in typed characters, thus empty
149: */
150: public void keyTyped(KeyEvent e) {
151: //needed for KeyListener, but not used
152: }
153:
154: /** Handle the key released event. */
155: public void keyReleased(KeyEvent e) {
156: //needed for KeyListener, but not used
157: }
158: });
159:
160: refinementSubcatList
161: .setSelectionMode(ListSelectionModel.SINGLE_SELECTION);
162:
163: final MouseListener mlRefinementSubcatList = new MouseAdapter() {
164: public void mouseClicked(MouseEvent e) {
165: boolean doubleClick = (e.getClickCount() == 2);
166: listAction(refinementSubcatList, refinementSubcatList
167: .locationToIndex(e.getPoint()), doubleClick);
168: refinementList.setSelectionBackground(Color.GRAY);
169: }
170: };
171: refinementSubcatList.addMouseListener(mlRefinementSubcatList);
172: refinementSubcatList.addKeyListener(new KeyListener() {
173: /** Handle the key pressed event. */
174: public void keyPressed(KeyEvent e) {
175: int keyCode = e.getKeyCode();
176: if (logger.isLoggable(Level.FINER)) {
177: logger.finer("Key pressed: " + e.toString());
178: }
179: if (keyCode == KeyEvent.VK_ENTER) {
180: listAction(refinementSubcatList,
181: refinementSubcatList.getSelectedIndex(),
182: true);
183: } else if (keyCode == KeyEvent.VK_LEFT) {
184: refinementList.requestFocusInWindow();
185: refinementSubcatList.clearSelection();
186: refinementList
187: .setSelectionBackground(refinementSubcatList
188: .getSelectionBackground());
189: }
190: }
191:
192: /**
193: * Handle the key typed event.
194: * We are not really interested in typed characters, thus empty
195: */
196: public void keyTyped(KeyEvent e) {
197: //needed for KeyListener, but not used
198: }
199:
200: /** Handle the key released event. */
201: public void keyReleased(KeyEvent e) {
202: //needed for KeyListener, but not used
203: }
204: });
205: refinementList
206: .setToolTipText("The list of current refinement options");
207: refinementList.setCellRenderer(new ToolTipCellRenderer());
208: refinementSubcatList
209: .setToolTipText("The list of current refinement options");
210: refinementSubcatList.setCellRenderer(new ToolTipCellRenderer());
211:
212: }
213:
214: /**
215: * @return Returns the refinementListsContainer,
216: * which will contain both JLists.
217: */
218: protected JSplitPane getRefinementListsContainer() {
219: return refinementListsContainer;
220: }
221:
222: /**
223: * handling the event of choosing the action at index from the list.
224: * That is either giving commands to GF or displaying the subcat menus
225: * @param list The list that generated this action
226: * @param index the index of the selected element in list
227: * @param doubleClick true iff a command should be sent to GF,
228: * false if only a new subcat menu should be opened.
229: */
230: private void listAction(JList list, int index, boolean doubleClick) {
231: if (index == -1) {
232: if (logger.isLoggable(Level.FINER))
233: logger.finer("no selection");
234: } else {
235: Object o;
236: if (list == refinementList) {
237: o = listModel.elementAt(index);
238: } else {
239: if (whichSubcat == null) {
240: //this is probably the case when no fitting properties of self
241: //are available and only a string is displayed in the submenu.
242: //clicking that string should do exactly nothing.
243: return;
244: }
245: Vector cmdvector = (Vector) this .subcatListModelHashtable
246: .get(this .whichSubcat);
247: o = (cmdvector.get(index));
248: }
249: GFCommand command = null;
250: if (o instanceof GFCommand) {
251: command = (GFCommand) o;
252: } else {
253: return;
254: }
255: if (command instanceof SelfPropertiesCommand) {
256: SelfPropertiesCommand spc = (SelfPropertiesCommand) command;
257: Vector selfs = spc.produceSubmenu();
258: if (selfs.size() == 0) {
259: listModel.remove(index);
260: refinementSubcatListModel.clear();
261: refinementSubcatListModel
262: .addElement("No properties fit here");
263: return;
264: } else {
265: this .subcatListModelHashtable.put(command
266: .getSubcat(), selfs);
267: listModel.remove(index);
268: LinkCommand newLink = new LinkCommand(
269: PrintnameManager.SELF_SUBCAT, editor
270: .getPrintnameManager());
271: listModel.add(index, newLink);
272: command = newLink;
273: }
274: }
275: if (command instanceof LinkCommand) { //includes SelfPropertiesCommand, which is intended
276: this .whichSubcat = command.getSubcat();
277: refinementSubcatListModel.clear();
278: Vector currentCommands = (Vector) this .subcatListModelHashtable
279: .get(this .whichSubcat);
280: for (Iterator it = currentCommands.iterator(); it
281: .hasNext();) {
282: this .refinementSubcatListModel
283: .addElement(it.next());
284: }
285: } else if (doubleClick && command instanceof InputCommand) {
286: InputCommand ic = (InputCommand) command;
287: editor.executeInputCommand(ic);
288:
289: } else if (doubleClick) {
290: refinementSubcatListModel.clear();
291: if (command instanceof RealCommand) {
292: editor.send("[t] " + command.getCommand(), true,
293: ((RealCommand) command).undoSteps);
294: } else {
295: //that shouldn't be the case ...
296: editor.send("[t] " + command.getCommand());
297: }
298: } else if (list == refinementList) {
299: refinementSubcatListModel.clear();
300: }
301: }
302: }
303:
304: /**
305: * Produces the popup menu that represents the current refinements.
306: * An alternative to the refinement list.
307: * @return s.a.
308: */
309: protected JPopupMenu producePopup() {
310: if (popup2.getComponentCount() > 0) {
311: return popup2;
312: }
313: for (int i = 0; i < this .listModel.size(); i++) {
314: GFCommand gfcmd = (GFCommand) this .listModel.get(i);
315: if (gfcmd instanceof LinkCommand) {
316: LinkCommand lc = (LinkCommand) gfcmd;
317: Vector subcatMenu = (Vector) this .subcatListModelHashtable
318: .get(lc.getSubcat());
319: JMenu tempMenu = new JMenu(lc.getDisplayText());
320: tempMenu.setToolTipText(lc.getTooltipText());
321: tempMenu.setFont(popup2.getFont());
322: JMenuItem tempMenuItem;
323: for (Iterator it = subcatMenu.iterator(); it.hasNext();) {
324: GFCommand subgfcmd = (GFCommand) it.next();
325: tempMenuItem = menuForCommand(subgfcmd);
326: if (tempMenuItem != null) {
327: tempMenu.add(tempMenuItem);
328: }
329: }
330: popup2.add(tempMenu);
331: } else {
332: JMenuItem tempMenu = menuForCommand(gfcmd);
333: if (tempMenu != null) {
334: popup2.add(tempMenu);
335: }
336: }
337: }
338: return popup2;
339: }
340:
341: /**
342: * takes a GFCommand and "transforms" it in a JMenuItem.
343: * These JMenuItems have their own listeners that take care of
344: * doing what is right ...
345: * @param gfcmd a RealCommand or an InputCommand
346: * (LinkCommand is ignored and produces null as the result)
347: * @return either the correspondend JMenuItem or null.
348: */
349: private JMenuItem menuForCommand(GFCommand gfcmd) {
350: JMenuItem tempMenu = null;
351: if (gfcmd instanceof RealCommand) {
352: tempMenu = new JMenuItem(gfcmd.getDisplayText());
353: tempMenu.setFont(popup2.getFont());
354: tempMenu.setActionCommand(gfcmd.getCommand());
355: tempMenu.setToolTipText(gfcmd.getTooltipText());
356: tempMenu.addActionListener(new ActionListener() {
357: public void actionPerformed(ActionEvent ae) {
358: JMenuItem mi = (JMenuItem) ae.getSource();
359: refinementSubcatListModel.clear();
360: String command = "[t] " + mi.getActionCommand();
361: editor.send(command);
362: }
363: });
364: } else if (gfcmd instanceof InputCommand) {
365: tempMenu = new JMenuItem(gfcmd.getDisplayText());
366: tempMenu.setFont(popup2.getFont());
367: tempMenu.setActionCommand(gfcmd.getCommand());
368: tempMenu.setToolTipText(gfcmd.getTooltipText());
369: tempMenu.addActionListener(new ActionListener() {
370: public void actionPerformed(ActionEvent ae) {
371: JMenuItem mi = (JMenuItem) ae.getSource();
372: String command = mi.getActionCommand();
373: InputCommand ic = InputCommand.forTypeName(command);
374: if (ic != null) {
375: editor.executeInputCommand(ic);
376: }
377: }
378: });
379:
380: }
381: return tempMenu;
382: }
383:
384: /**
385: * Takes the StringTuples in gfCommandVector, creates the RealCommand
386: * objects for them.
387: * Goes through this list and groups the RealCommands
388: * according to their subcategory tag (which starts with %)
389: * If there is a "(" afterwards, everything until the before last
390: * character in the printname will be used as the display name
391: * for this subcategory. If this displayname is defined a second time,
392: * it will get overwritten.
393: * Sorting is also done here.
394: * Adding additional special commands like InputCommand happens here too.
395: * @param gfCommandVector contains all RealCommands, that are available
396: * at the moment
397: * @param toAppend will be appended to every command, that is sent to GF.
398: * Normally, toAppend will be the empty String "".
399: * But it can be a chain command's second part.
400: * @param isAbstract If the selected menu language is abstract or not
401: * @param easyAttributes if true, attributes of self will be added.
402: * @param focusPosition The current position of the focus in the AST.
403: * Needed for easy access to properties of self.
404: * @param gfCapsule The read/write encapsulation of the GF process.
405: * Needed for easy access to properties of self.
406: */
407: protected void formRefinementMenu(final Vector gfCommandVector,
408: final String toAppend, GfAstNode currentNode,
409: final boolean isAbstract, boolean easyAttributes,
410: LinPosition focusPosition, GfCapsule gfCapsule) {
411: this .listModel.clear();
412: this .refinementSubcatListModel.clear();
413: this .gfcommands.clear();
414: this .subcatListModelHashtable.clear();
415: this .whichSubcat = null;
416: this .popup2.removeAll();
417: Vector prelListModel = new Vector();
418: /** to keep track of subcats and their names */
419: HashSet processedSubcats = new HashSet();
420: //at the moment, we don't know yet, which subcats are
421: //nearly empty
422: for (Iterator it = gfCommandVector.iterator(); it.hasNext();) {
423: final StringTuple st = (StringTuple) it.next();
424: GFCommand gfcommand;
425: if (st instanceof ChainCommandTuple) {
426: ChainCommandTuple cct = (ChainCommandTuple) st;
427: gfcommand = new RealCommand(st.first, processedSubcats,
428: editor.getPrintnameManager(), st.second,
429: isAbstract, toAppend, cct.undoSteps, cct.fun,
430: cct.subcat);
431: } else {
432: gfcommand = new RealCommand(st.first, processedSubcats,
433: editor.getPrintnameManager(), st.second,
434: isAbstract, toAppend);
435: }
436: if ((!editor.isGroupSubcat())
437: || (gfcommand.getSubcat() == null)) {
438: prelListModel.addElement(gfcommand);
439: } else {
440: //put stuff in the correct Vector for the refinementSubcatListModel
441: Vector lm;
442: if (subcatListModelHashtable.containsKey(gfcommand
443: .getSubcat())) {
444: lm = (Vector) this .subcatListModelHashtable
445: .get(gfcommand.getSubcat());
446: } else {
447: lm = new Vector();
448: this .subcatListModelHashtable.put(gfcommand
449: .getSubcat(), lm);
450: }
451: lm.addElement(gfcommand);
452: if (gfcommand.isNewSubcat()) {
453: GFCommand linkCmd = new LinkCommand(gfcommand
454: .getSubcat(), editor.getPrintnameManager());
455: prelListModel.addElement(linkCmd);
456: }
457: }
458: }
459:
460: //so we remove empty subcats now and replace them by their RealCommand
461: for (int i = 0; i < prelListModel.size(); i++) {
462: if (prelListModel.get(i) instanceof LinkCommand) {
463: LinkCommand lc = (LinkCommand) prelListModel.get(i);
464: Vector subcatMenu = (Vector) this .subcatListModelHashtable
465: .get(lc.getSubcat());
466: if (subcatMenu.size() == 1) {
467: RealCommand rc = (RealCommand) subcatMenu.get(0);
468: prelListModel.set(i, rc);
469: }
470: }
471: }
472:
473: // Some types invite special treatment, like Int and String
474: // which can be read from the user.
475: if (currentNode.isMeta()) {
476: InputCommand usedInputCommand = null;
477: if (currentNode.getType().equals("Int")) {
478: usedInputCommand = InputCommand.intInputCommand;
479: prelListModel.addElement(usedInputCommand);
480: }
481: if (currentNode.getType().equals("String")) {
482: usedInputCommand = InputCommand.stringInputCommand;
483: prelListModel.addElement(usedInputCommand);
484: }
485: if (usedInputCommand != null) {
486: for (Iterator it = usedInputCommand.enteredValues
487: .iterator(); it.hasNext();) {
488: Object o = it.next();
489: //for GF it seems to make no difference,
490: //if we use 'g' or 'r' as the command to send
491: //Int and String. 'r' is already supported
492: //by RealCommand, so I chose that.
493: RealCommand rc = new RealCommand("r " + o,
494: processedSubcats, editor
495: .getPrintnameManager(), "r " + o,
496: isAbstract, toAppend);
497: prelListModel.addElement(rc);
498: }
499: }
500: }
501:
502: //add the special entry for the properties of self
503: if (easyAttributes) {
504: final SelfPropertiesCommand spc = new SelfPropertiesCommand(
505: editor.getPrintnameManager(), gfCapsule,
506: focusPosition, isAbstract, toAppend,
507: processedSubcats);
508: prelListModel.add(spc);
509: }
510:
511: //now sort the preliminary listmodels
512: if (editor.isSortRefinements()) {
513: Collections.sort(prelListModel);
514: for (Iterator it = subcatListModelHashtable.values()
515: .iterator(); it.hasNext();) {
516: Vector slm = (Vector) it.next();
517: Collections.sort(slm);
518: }
519: }
520: //now fill this.listModel
521: for (Iterator it = prelListModel.iterator(); it.hasNext();) {
522: Object next = it.next();
523: this .listModel.addElement(next);
524: }
525: //select the first command in the refinement menu, if available
526: if (this .listModel.size() > 0) {
527: this .refinementList.setSelectedIndex(0);
528: } else {
529: this .refinementList.setSelectedIndex(-1);
530: }
531: this .refinementList.setSelectionBackground(refinementSubcatList
532: .getSelectionBackground());
533: }
534:
535: /**
536: * Requests the focus for the refinement list
537: */
538: protected void requestFocus() {
539: refinementList.requestFocusInWindow();
540: }
541:
542: /**
543: * clears the list model
544: */
545: protected void reset() {
546: listModel.clear();
547: }
548:
549: /**
550: * Applies newFont to the visible elements
551: * @param newFont The new font, what else?
552: */
553: protected void setFont(Font newFont) {
554: refinementList.setFont(newFont);
555: refinementSubcatList.setFont(newFont);
556: popup2.setFont(newFont);
557: }
558: }
|