0001: //Copyright (c) Janna Khegai 2004, Kristofer Johanisson 2004,
0002: // Hans-Joachim Daniels 2005
0003: //
0004: //This program is free software; you can redistribute it and/or modify
0005: //it under the terms of the GNU General Public License as publisrhed by
0006: //the Free Software Foundation; either version 2 of the License, or
0007: //(at your option) any later version.
0008: //
0009: //This program is distributed in the hope that it will be useful,
0010: //but WITHOUT ANY WARRANTY; without even the implied warranty of
0011: //MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
0012: //GNU General Public License for more details.
0013: //
0014: //You can either finde the file LICENSE or LICENSE.TXT in the source
0015: //distribution or in the .jar file of this application
0016:
0017: package de.uka.ilkd.key.ocl.gf;
0018:
0019: import jargs.gnu.CmdLineParser;
0020:
0021: import java.awt.*;
0022: import java.awt.event.*;
0023: import java.io.*;
0024: import java.net.MalformedURLException;
0025: import java.net.URL;
0026: import java.util.*;
0027: import java.util.logging.Level;
0028: import java.util.logging.Logger;
0029:
0030: import javax.swing.*;
0031: import javax.swing.event.CaretEvent;
0032: import javax.swing.event.CaretListener;
0033: import javax.swing.text.BadLocationException;
0034: import javax.swing.text.DefaultHighlighter;
0035: import javax.swing.text.JTextComponent;
0036: import javax.swing.text.html.HTMLDocument;
0037: import javax.swing.tree.DefaultMutableTreeNode;
0038: import javax.swing.tree.DefaultTreeModel;
0039: import javax.swing.tree.TreePath;
0040:
0041: public class GFEditor2 extends JFrame {
0042: /**
0043: * the main logger for this class
0044: */
0045: private static Logger logger = Logger.getLogger(GFEditor2.class
0046: .getName());
0047: /**
0048: * debug stuff for the tree
0049: */
0050: private static Logger treeLogger = Logger
0051: .getLogger(DynamicTree2.class.getName());
0052: /**
0053: * red mark-up && html debug messages
0054: */
0055: private static Logger redLogger = Logger.getLogger(GFEditor2.class
0056: .getName()
0057: + "_Red");
0058: /**
0059: * pop-up/mouse handling debug messages
0060: */
0061: private static Logger popUpLogger = Logger
0062: .getLogger(GFEditor2.class.getName() + "_PopUp");
0063: /**
0064: * linearization marking debug messages
0065: */
0066: private static Logger linMarkingLogger = Logger
0067: .getLogger(GFEditor2.class.getName() + "_LinMarking");
0068: /**
0069: * keyPressedEvents & Co.
0070: */
0071: private static Logger keyLogger = Logger.getLogger(GFEditor2.class
0072: .getName()
0073: + "_key");
0074: /**
0075: * everything that is sent to GF
0076: */
0077: private static Logger sendLogger = Logger.getLogger(GFEditor2.class
0078: .getName()
0079: + ".send");
0080: /**
0081: * the first part of the name of the GF grammar file
0082: */
0083: public final static String modelModulName = "FromUMLTypes";
0084: /**
0085: * Does the saving of constraints in Together.
0086: * Or to be more precise, itself knows nothing about Together.
0087: * Only its subclasses. That way it can be compiled without KeY.
0088: */
0089: final private ConstraintCallback callback;
0090: /**
0091: * if the OCL features should be switched on
0092: */
0093: final private boolean oclMode;
0094:
0095: /**
0096: * does all direct interaction with GF
0097: * (except for the probers)
0098: */
0099: private GfCapsule gfCapsule = null;
0100: /**
0101: * current Font
0102: */
0103: private Font font;
0104: /**
0105: * contains the offered fonts by name
0106: */
0107: private JMenu fontMenu;
0108: /**
0109: * offers a list of font sizes
0110: */
0111: private JMenu sizeMenu;
0112:
0113: /**
0114: * what is written here is parsed and the result inserted instead of tbe selection.
0115: * No idea how this element is displayed
0116: */
0117: private JTextField parseField = new JTextField("textField!");
0118:
0119: /**
0120: * The position of the focus, that is, the currently selected node in the AST
0121: */
0122: private LinPosition focusPosition;
0123: /**
0124: * When a new category is chosen, it is set to true.
0125: * In the reset or a completely new state it is falsed.
0126: * The structure of the GF output is different then and this must be taken
0127: * care of.
0128: */
0129: private boolean newObject = false;
0130: /**
0131: * if the user enters text for the alpha conversion, he perhaps wants to input the same text again.
0132: * Therefore it is saved.
0133: */
0134: private String alphaInput = "";
0135: /**
0136: * if a user sends a custom command to GF, he might want to do this
0137: * again with the same command.
0138: * Therefore it is saved.
0139: */
0140: private String commandInput = "";
0141:
0142: /**
0143: * default status text, just status
0144: */
0145: private final static String status = "status";
0146: /**
0147: * the language the possible actions are displayed
0148: */
0149: private String selectedMenuLanguage = "Abstract";
0150: /**
0151: * write-only variable, stores the current import paths
0152: * reset after each reset.
0153: */
0154: private String fileString = "";
0155: /**
0156: * The mapping between Java tree pathes and GF AST positions
0157: * is stored here.
0158: */
0159: private Hashtable nodeTable = new Hashtable();
0160:
0161: /**
0162: * This is necessary to map clicks in the tree, where in the event handler
0163: * only the selection path is availble, to AST positions which can be
0164: * sent to GF.
0165: * @param key The TreeSelectionPath, that identifies the wanted node
0166: * @return The AST position string of the given TreePath in the table
0167: * of stored nodes.
0168: */
0169: protected String getNodePosition(Object key) {
0170: return nodeTable.get(key).toString();
0171: }
0172:
0173: /**
0174: * this FileChooser gets enriched with the Term/Text option
0175: */
0176: private JFileChooser saveFc = new JFileChooser("./");
0177: /** used for new Topic, Import and Browse (readDialog) */
0178: private JFileChooser fc = new JFileChooser("./");
0179: private final static String[] modifyMenu = { "Modify", "identity",
0180: "transfer", "compute", "paraphrase", "generate",
0181: "typecheck", "solve", "context" };
0182: private static final String[] newMenu = { "New" };
0183:
0184: /**
0185: * Linearizations' display area
0186: */
0187: private JTextArea linearizationArea = new JTextArea();
0188: /**
0189: * The abstract syntax tree representation of the current editing object
0190: */
0191: private DynamicTree2 tree = new DynamicTree2(this );
0192:
0193: /**
0194: * Current Topic
0195: */
0196: private JLabel grammar = new JLabel("No topic ");
0197: /**
0198: * Writing the current editing object to file in the term or text
0199: * format
0200: */
0201: private JButton save = new JButton("Save");
0202: /**
0203: * Reading both a new environment and an editing object from file.
0204: * Current editing will be discarded
0205: */
0206: private JButton open = new JButton("Open");
0207: /**
0208: * Reading a new environment from file. Current editing will be
0209: * discarded.
0210: */
0211: private JButton newTopic;
0212: /** Sending a command to GF */
0213: private JButton gfCommand;
0214:
0215: /** Moving the focus to the previous metavariable */
0216: private JButton leftMeta = new JButton("?<");
0217: /** Moving the focus to the previous term */
0218: private JButton left = new JButton("<");
0219: /** Moving the focus to the top term */
0220: private JButton top = new JButton("Top");
0221: /** Moving the focus to the next term */
0222: private JButton right = new JButton(">");
0223: /** Moving the focus to the next metavariable */
0224: private JButton rightMeta = new JButton(">?");
0225: private final static String actionOnSubtermString = "Select Action on Subterm";
0226: private JLabel subtermNameLabel = new JLabel();
0227: private JLabel subtermDescLabel = new JLabel();
0228: /** Refining with term or linearization from typed string or file */
0229: private JButton read = new JButton("Read");
0230: /** Performing alpha-conversion of bound variables */
0231: private JButton alpha;
0232: /** Generating random refinement */
0233: private JButton random;
0234: /** Going back to the previous state */
0235: private JButton undo;
0236: /** The main panel on which the others are put */
0237: private JPanel coverPanel = new JPanel();
0238: /** the dialog to read in Strings or Terms */
0239: private ReadDialog readDialog;
0240:
0241: /** The list of available categories to start editing */
0242: private JComboBox newCategoryMenu = new JComboBox(newMenu);
0243: /** Choosing a linearization method */
0244: private JComboBox modify = new JComboBox(modifyMenu);
0245: /** the panel with the more general command buttons */
0246: private JPanel downPanel = new JPanel();
0247: /** the splitpane containing tree on the left and linearization area on the right*/
0248: private JSplitPane treePanel;
0249: /** the upper button bar for New, Save */
0250: private JPanel upPanel = new JPanel();
0251: /** the panel that contains the navigation buttons and some explanatory text */
0252: private JPanel middlePanel = new JPanel();
0253: /** the panel that contains only the navigation buttons */
0254: private JPanel middlePanelUp = new JPanel();
0255: /** the panel that vontains the the explanatory text for the refinement menu */
0256: private JPanel middlePanelDown = new JPanel(new BorderLayout());
0257: /** splits between tree and lin above and nav buttons and refinements below */
0258: private JSplitPane centerPanel;
0259: /** the window that contains the refinements when in split mode */
0260: private JFrame gui2 = new JFrame();
0261: /** the main window with tree, lin and buttons when in split mode */
0262: private JPanel centerPanel2 = new JPanel();
0263: /** contains refinment list and navigation buttons */
0264: private JPanel centerPanelDown = new JPanel();
0265: /** only contains the linearization area */
0266: private JScrollPane outputPanelText = new JScrollPane(
0267: this .linearizationArea);
0268: /** HTML Linearizations' display area */
0269: private JTextPane htmlLinPane = new JTextPane();
0270: /** only contains the HTML linearization area */
0271: private JScrollPane outputPanelHtml = new JScrollPane(
0272: this .htmlLinPane);
0273: /** contains both pure text and HTML areas */
0274: private JSplitPane linSplitPane;
0275: /** contains the linSplitPane and the status field below it */
0276: private JPanel outputPanelUp = new JPanel(new BorderLayout());
0277: /** contains statusLabel */
0278: private JPanel statusPanel = new JPanel();
0279: /** The type the currently focused term has */
0280: private JLabel statusLabel = new JLabel(status);
0281: /** the main menu in the top */
0282: private JMenuBar menuBar = new JMenuBar();
0283: /** View settings */
0284: private JMenu viewMenu = new JMenu("View");
0285: /**
0286: * stores a list of all languages + abstract to select the language,
0287: * in which the selectMenu will be filled.
0288: */
0289: private JMenu mlMenu = new JMenu("language");
0290: /** Choosing the refinement options' representation */
0291: private JMenu modeMenu = new JMenu("Menus");
0292: /** Language settings */
0293: private JMenu langMenu = new JMenu("Languages");
0294: /** Main operations */
0295: private JMenu fileMenu = new JMenu("File");
0296: /** stores whether the refinement list should be in 'long' format */
0297: private JRadioButtonMenuItem rbMenuItemLong;
0298: /** stores whether the refinement list should be in 'short' format */
0299: private JRadioButtonMenuItem rbMenuItemShort;
0300: /** stores whether the refinement list should be in 'untyped' format */
0301: private JRadioButtonMenuItem rbMenuItemUnTyped;
0302: /**
0303: * linked to rbMenuItemUnTyped.
0304: * Is true if type information should be appended in the refinement menu
0305: */
0306: private boolean typedMenuItems = false;
0307: /** stores whether the AST is visible or not */
0308: private JCheckBoxMenuItem treeCbMenuItem;
0309: /** in the save dialog whether to save as a Term or as linearized Text */
0310: private ButtonGroup saveTypeGroup = new ButtonGroup();
0311: /** the entries of the filter menu */
0312: private final static String[] filterMenuContents = { "identity",
0313: "erase", "take100", "text", "code", "latexfile",
0314: "structured", "unstructured" };
0315: /** Choosing the linearization representation format */
0316: private JMenu filterMenu = new JMenu("Filter");
0317: /** for managing the filter menu entries*/
0318: private ButtonGroup filterButtonGroup = new ButtonGroup();
0319:
0320: /** Some usability things can be switched off here for testing */
0321: private JMenu usabilityMenu = new JMenu("Usability");
0322: /**
0323: * stores whether self and result should only be made visible
0324: * if applicable
0325: */
0326: private JCheckBoxMenuItem selfresultCbMenuItem;
0327: /** to switch grouping of entries in the refinement menu on and off */
0328: private JCheckBoxMenuItem subcatCbMenuItem;
0329: /** to switch sorting of entries in the refinement menu on and off */
0330: private JCheckBoxMenuItem sortCbMenuItem;
0331: /** to switch autocoercing */
0332: private JCheckBoxMenuItem coerceCbMenuItem;
0333: /** to switch reducing the argument 3 refinement menu of coerce on or off */
0334: private JCheckBoxMenuItem coerceReduceCbMenuItem;
0335: /** to switch highlighting subtyping errors on or off */
0336: private JCheckBoxMenuItem highlightSubtypingErrorsCbMenuItem;
0337: /** to switch hiding coerce on or off */
0338: private JCheckBoxMenuItem hideCoerceCbMenuItem;
0339: /** to switch hiding coerce even if parts are unrefined on or off */
0340: private JCheckBoxMenuItem hideCoerceAggressiveCbMenuItem;
0341: /** to switch the attributes of self in the refinement menu on or off */
0342: private JCheckBoxMenuItem easyAttributesCbMenuItem;
0343:
0344: /**
0345: * if true, self and result are only shown if applicable,
0346: * tied to @see selfresultCbMenuItem
0347: */
0348: private boolean showSelfResult = true;
0349: /**
0350: * if true, refinements are grouped by subcat
0351: * tied to @see subcatCbMenuItem.
0352: */
0353: private boolean groupSubcat = true;
0354:
0355: /**
0356: * @return Returns whether subcategories should be grouped or not
0357: */
0358: protected boolean isGroupSubcat() {
0359: return groupSubcat;
0360: }
0361:
0362: /**
0363: * if true, refinements are grouped by subcat.
0364: * tied to @see subcatCbMenuItem.
0365: */
0366: private boolean sortRefinements = true;
0367:
0368: /**
0369: * @return Returns if the refinements should get sorted.
0370: */
0371: protected boolean isSortRefinements() {
0372: return sortRefinements;
0373: }
0374:
0375: /**
0376: * if true, then Instances will automatically get wrapped with a coerce
0377: * if encountered as meta in the active node
0378: */
0379: private boolean autoCoerce = false;
0380: /**
0381: * If this is true, the refinementmenu for argument 3 of coerce
0382: * will be populated only with suiting refinements.
0383: */
0384: private boolean coerceReduceRM = false;
0385: /**
0386: * If true, then the AST will be checked for missing subtyping witnesses
0387: */
0388: private boolean highlightSubtypingErrors = false;
0389: /**
0390: * if true, filled in coercions will be hidden from the user
0391: */
0392: private boolean hideCoerce = false;
0393: /**
0394: * if true, filled in coercions will be hidden from the user
0395: * even if they lack filled in type arguments
0396: */
0397: private boolean hideCoerceAggressive = false;
0398: /**
0399: * offer the attributes of self directly in the refinement menu
0400: */
0401: private boolean easyAttributes = false;
0402:
0403: /**
0404: * handles all the Printname naming and so on.
0405: */
0406: private PrintnameManager printnameManager;
0407:
0408: /**
0409: * @return Returns the printnameManager.
0410: */
0411: protected PrintnameManager getPrintnameManager() {
0412: return printnameManager;
0413: }
0414:
0415: /**
0416: * stores the current type. Since the parsing often fails, this is
0417: * most often null, except for Int and String, which can be parsed.
0418: */
0419: private GfAstNode currentNode = null;
0420: /** stores the displayed parts of the linearization */
0421: private Display display = new Display(3);
0422:
0423: /** takes care of the menus that display the available languages */
0424: private LangMenuModel langMenuModel = new LangMenuModel();
0425:
0426: //Now the stuff for choosing the wanted output type (pure text or HTML)
0427: /**
0428: * 1 for text, 2 for HTML, 3 for both
0429: */
0430: private int displayType = 1;
0431: /**
0432: * rbText, rbHtml and rbTextHtml are grouped here.
0433: */
0434: private ButtonGroup bgDisplayType = new ButtonGroup();
0435: /**
0436: * The button that switches the linearization view to text only
0437: */
0438: private JRadioButtonMenuItem rbText = new JRadioButtonMenuItem(
0439: new AbstractAction("pure text") {
0440: public void actionPerformed(ActionEvent ae) {
0441: int oldDisplayType = displayType;
0442: displayType = 1;
0443: display.setDisplayType(displayType);
0444: outputPanelUp.removeAll();
0445: outputPanelUp.add(outputPanelText,
0446: BorderLayout.CENTER);
0447: outputPanelUp.add(statusPanel, BorderLayout.SOUTH);
0448: if (ae != null && oldDisplayType == 2) { //not manually called in the beginning and only HTML
0449: formLin();
0450: }
0451: outputPanelUp.validate();
0452: }
0453: });
0454: /**
0455: * The button that switches the linearization view to HTML only
0456: */
0457: private JRadioButtonMenuItem rbHtml = new JRadioButtonMenuItem(
0458: new AbstractAction("HTML") {
0459: public void actionPerformed(ActionEvent ae) {
0460: int oldDisplayType = displayType;
0461: displayType = 2;
0462: display.setDisplayType(displayType);
0463: outputPanelUp.removeAll();
0464: outputPanelUp.add(outputPanelHtml,
0465: BorderLayout.CENTER);
0466: outputPanelUp.add(statusPanel, BorderLayout.SOUTH);
0467: if (ae != null && oldDisplayType == 1) { //not manually called in the beginning and only text
0468: formLin();
0469: }
0470: outputPanelUp.validate();
0471: }
0472: });
0473: /**
0474: * The button that switches the linearization view to both text and
0475: * HTML separated with a JSplitpane
0476: */
0477: private JRadioButtonMenuItem rbTextHtml = new JRadioButtonMenuItem(
0478: new AbstractAction("text and HTML") {
0479: public void actionPerformed(ActionEvent ae) {
0480: int oldDisplayType = displayType;
0481: displayType = 3;
0482: display.setDisplayType(displayType);
0483: linSplitPane.setLeftComponent(outputPanelText);
0484: linSplitPane.setRightComponent(outputPanelHtml);
0485: outputPanelUp.removeAll();
0486: outputPanelUp
0487: .add(linSplitPane, BorderLayout.CENTER);
0488: outputPanelUp.add(statusPanel, BorderLayout.SOUTH);
0489: if (ae != null && oldDisplayType != 3) { //not manually called in the beginning and not both (the latter should always be true)
0490: formLin();
0491: }
0492: outputPanelUp.validate();
0493: }
0494: });
0495:
0496: /**
0497: * Since the user will be able to send chain commands to GF,
0498: * the editor has to keep track of them, since GF does not undo
0499: * all parts with one undo, instead 'u n' with n as the number of
0500: * individual commands, has to be sent.
0501: */
0502: private final Stack undoStack = new Stack();
0503:
0504: /**
0505: * for starting a SubtypingProber run
0506: */
0507: private JButton checkSubtyping;
0508:
0509: /**
0510: * handles the commands and how they are presented to the user
0511: */
0512: private RefinementMenu refinementMenu;
0513: /**
0514: * handles parsing and preparing for display
0515: * of the linearization XML from GF.
0516: * Also takes care of the click-in functionality.
0517: */
0518: private Linearization linearization;
0519:
0520: /**
0521: * Initializes GF with the given command, sets up the GUI
0522: * and reads the first GF output
0523: * @param gfcmd The command with all parameters, including -java
0524: * that is to be executed. Will set up the GF side of this session.
0525: * @param isHtml true iff the editor should start in HTML mode.
0526: * @param baseURL the URL that is the base for all relative links in HTML
0527: * @param isOcl if the OCL special features should be available
0528: */
0529: public GFEditor2(String[] gfcmd, boolean isHtml, URL baseURL,
0530: boolean isOcl) {
0531: this .callback = null;
0532: this .oclMode = isOcl;
0533: Image icon = null;
0534: try {
0535: final URL iconURL = ClassLoader
0536: .getSystemResource("gf-icon.gif");
0537: icon = Toolkit.getDefaultToolkit().getImage(iconURL);
0538: } catch (NullPointerException npe) {
0539: logger.info("gf-icon.gif could not be found.\n"
0540: + npe.getLocalizedMessage());
0541: }
0542: initializeGUI(baseURL, isHtml, icon);
0543: initializeGF(gfcmd, null);
0544: }
0545:
0546: /**
0547: * a specialized constructor for OCL comstraints
0548: * Starts with a new Constraint and an initial syntax tree
0549: * @param gfcmd The command with all parameters, including -java
0550: * that is to be executed. Will set up the GF side of this session.
0551: * @param callback The class responsible for saving the OCL constraint
0552: * as a JavaDoc comment
0553: * @param initAbs the initial abstract syntax tree
0554: * @param pm to monitor the loading progress. May be null
0555: */
0556: public GFEditor2(String[] gfcmd, ConstraintCallback callback,
0557: String initAbs, ProgressMonitor pm) {
0558: this .oclMode = true;
0559: this .callback = callback;
0560:
0561: Utils.tickProgress(pm, 5220, "Loading grammars");
0562: initializeGF(gfcmd, pm);
0563: Utils.tickProgress(pm, 9350, "Initializing GUI");
0564: initializeGUI(null, true, null);
0565:
0566: // send correct term (syntax tree)
0567: //The initial GF constraint has until now always been
0568: //automatically solvable. So don't startle the user
0569: //with painting everything red.
0570: send(initAbs + " ;; c solve ", false, 2);
0571: processGfedit();
0572: Utils.tickProgress(pm, 9700, "Loading finished");
0573: pm.close();
0574: logger.finer("GFEditor2 constructor finished");
0575: }
0576:
0577: /**
0578: * Starts GF and sets up the reading facilities.
0579: * Shouldn't be called twice.
0580: * @param gfcmd The command for GF to be executed.
0581: * expects the -java parameters and all grammar modules
0582: * to be specified. Simply executes this command without any
0583: * modifications.
0584: * @param pm to monitor the loading progress. May be null
0585: */
0586: private void initializeGF(String[] gfcmd, ProgressMonitor pm) {
0587: Utils.tickProgress(pm, 5250, "Starting GF");
0588: logger.fine("Trying: " + gfcmd);
0589: gfCapsule = new GfCapsule(gfcmd);
0590: processInit(pm, true);
0591: resetPrintnames(false);
0592: }
0593:
0594: /**
0595: * (re-)initializes this.printnameManager and loads the printnames from
0596: * GF.
0597: * @param replayState If GF should be called to give the same state as before,
0598: * but without the message. Is needed, when this function is started by the user.
0599: * If sth. else is sent to GF automatically, this is not needed.
0600: */
0601: private void resetPrintnames(boolean replayState) {
0602: this .printnameManager = new PrintnameManager();
0603: PrintnameLoader pl = new PrintnameLoader(gfCapsule,
0604: this .printnameManager, this .typedMenuItems);
0605: if (!selectedMenuLanguage.equals("Abstract")) {
0606: String sendString = selectedMenuLanguage;
0607: pl.readPrintnames(sendString);
0608: //empty GF command, clears the message, so that the printnames
0609: //are not printed again when for example a 'ml' command comes
0610: //next
0611: if (replayState) {
0612: send("gf ", true, 0);
0613: }
0614: }
0615: }
0616:
0617: /**
0618: * reliefs the constructor from setting up the GUI stuff
0619: * @param baseURL the base URL for relative links in the HTML view
0620: * @param showHtml if the linearization area for HTML should be active
0621: * instead of the pure text version
0622: * @param icon The icon in the title bar of the main window.
0623: * For KeY-usage, no icon is given and the Swing default is chosen
0624: * instead.
0625: */
0626: private void initializeGUI(URL baseURL, boolean showHtml, Image icon) {
0627: refinementMenu = new RefinementMenu(this );
0628: this .setDefaultCloseOperation(DO_NOTHING_ON_CLOSE);
0629: this .addWindowListener(new WindowAdapter() {
0630: public void windowClosing(WindowEvent e) {
0631: endProgram();
0632: }
0633: });
0634: setIconImage(icon);
0635: this .readDialog = new ReadDialog(this );
0636:
0637: //Add listener to components that can bring up popup menus.
0638: MouseListener popupListener2 = new PopupListener();
0639: linearizationArea.addMouseListener(popupListener2);
0640: htmlLinPane.addMouseListener(popupListener2);
0641:
0642: //now for the menus
0643:
0644: setJMenuBar(menuBar);
0645: setTitle("GF Syntax Editor");
0646: viewMenu.setToolTipText("View settings");
0647: fileMenu.setToolTipText("Main operations");
0648: langMenu.setToolTipText("Language settings");
0649: usabilityMenu.setToolTipText("Usability settings");
0650: menuBar.add(fileMenu);
0651: menuBar.add(langMenu);
0652: menuBar.add(viewMenu);
0653: menuBar.add(modeMenu);
0654: menuBar.add(usabilityMenu);
0655: modeMenu
0656: .setToolTipText("Choosing the refinement options' representation");
0657:
0658: /**
0659: * listens to the showTree JCheckBoxMenuItem and
0660: * switches displaying the AST on or off
0661: */
0662: final ActionListener showTreeListener = new ActionListener() {
0663: public void actionPerformed(ActionEvent e) {
0664: if (!((JCheckBoxMenuItem) e.getSource()).isSelected()) {
0665: if (logger.isLoggable(Level.FINER))
0666: logger.finer("showTree was selected");
0667: treeCbMenuItem.setSelected(false);
0668: if (((JRadioButtonMenuItem) viewMenu.getItem(2))
0669: .isSelected()) {
0670: centerPanel.remove(treePanel);
0671: centerPanel.setLeftComponent(outputPanelUp);
0672: } else {
0673: centerPanel2.remove(treePanel);
0674: centerPanel2.add(outputPanelUp,
0675: BorderLayout.CENTER);
0676: }
0677: } else {
0678: if (logger.isLoggable(Level.FINER))
0679: logger.finer("showTree was not selected");
0680: treeCbMenuItem.setSelected(true);
0681: if (((JRadioButtonMenuItem) viewMenu.getItem(2))
0682: .isSelected()) {
0683: centerPanel.remove(outputPanelUp);
0684: treePanel.setRightComponent(outputPanelUp);
0685: centerPanel.setLeftComponent(treePanel);
0686: } else {
0687: centerPanel2.remove(outputPanelUp);
0688: treePanel.setRightComponent(outputPanelUp);
0689: centerPanel2
0690: .add(treePanel, BorderLayout.CENTER);
0691: }
0692: }
0693: pack();
0694: repaint();
0695: }
0696:
0697: };
0698:
0699: treeCbMenuItem = new JCheckBoxMenuItem("Tree");
0700: treeCbMenuItem.setActionCommand("showTree");
0701: treeCbMenuItem.addActionListener(showTreeListener);
0702: treeCbMenuItem.setSelected(true);
0703:
0704: viewMenu.add(treeCbMenuItem);
0705: viewMenu.addSeparator();
0706:
0707: final Action saveAction = new SaveAction();
0708: final Action openAction = new OpenAction();
0709: final Action newTopicAction = new NewTopicAction();
0710: final Action resetAction = new ResetAction();
0711: final Action quitAction = new QuitAction();
0712: final Action undoAction = new UndoAction();
0713: final Action randomAction = new RandomAction();
0714: final Action alphaAction = new AlphaAction();
0715: final Action gfCommandAction = new GfCommandAction();
0716: final Action readAction = new ReadAction();
0717: final Action splitAction = new SplitAction();
0718: final Action combineAction = new CombineAction();
0719:
0720: JMenuItem fileMenuItem = new JMenuItem(openAction);
0721: fileMenu.add(fileMenuItem);
0722: fileMenuItem = new JMenuItem(newTopicAction);
0723: fileMenu.add(fileMenuItem);
0724: fileMenuItem = new JMenuItem(resetAction);
0725: fileMenu.add(fileMenuItem);
0726: fileMenuItem = new JMenuItem(saveAction);
0727: fileMenu.add(fileMenuItem);
0728: fileMenu.addSeparator();
0729: fileMenuItem = new JMenuItem(quitAction);
0730: fileMenu.add(fileMenuItem);
0731:
0732: JRadioButtonMenuItem rbMenuItem = new JRadioButtonMenuItem(
0733: combineAction);
0734: rbMenuItem.setSelected(true);
0735: /* rbMenuItem.setMnemonic(KeyEvent.VK_R);
0736: rbMenuItem.setAccelerator(KeyStroke.getKeyStroke(
0737: KeyEvent.VK_1, ActionEvent.ALT_MASK));
0738: rbMenuItem.getAccessibleContext().setAccessibleDescription(
0739: "This doesn't really do anything");
0740: */
0741: ButtonGroup menuGroup = new ButtonGroup();
0742: menuGroup.add(rbMenuItem);
0743: viewMenu.add(rbMenuItem);
0744:
0745: rbMenuItem = new JRadioButtonMenuItem(splitAction);
0746: menuGroup.add(rbMenuItem);
0747: viewMenu.add(rbMenuItem);
0748:
0749: //Font stuff
0750: final int DEFAULT_FONT_SIZE = 14;
0751: GraphicsEnvironment gEnv = GraphicsEnvironment
0752: .getLocalGraphicsEnvironment();
0753: /** The list of font names our environment offers us */
0754: String[] envfonts = gEnv.getAvailableFontFamilyNames();
0755:
0756: /** the list of fonts the environment offers us */
0757: Font[] fontObjs = new Font[envfonts.length];
0758: for (int fi = 0; fi < envfonts.length; fi++) {
0759: fontObjs[fi] = new Font(envfonts[fi], Font.PLAIN,
0760: DEFAULT_FONT_SIZE);
0761: }
0762: font = new Font(null, Font.PLAIN, DEFAULT_FONT_SIZE);
0763: //font menus
0764: viewMenu.addSeparator();
0765: fontMenu = new JMenu("Font");
0766: fontMenu.setToolTipText("Change font");
0767: sizeMenu = new JMenu("Font Size");
0768: sizeMenu.setToolTipText("Change font size");
0769: viewMenu.add(sizeMenu);
0770: viewMenu.add(fontMenu);
0771:
0772: {
0773: JMenuItem fontItem;
0774: ActionListener fontListener = new ActionListener() {
0775: public void actionPerformed(ActionEvent ae) {
0776: try {
0777: JMenuItem source = (JMenuItem) ae.getSource();
0778: font = new Font(source.getText(), Font.PLAIN,
0779: font.getSize());
0780: fontEveryWhere(font);
0781: } catch (ClassCastException e) {
0782: logger
0783: .warning("Font change started on strange object\n"
0784: + e.getLocalizedMessage());
0785: }
0786: }
0787: };
0788: for (int i = 0; i < envfonts.length; i++) {
0789: fontItem = new JMenuItem(envfonts[i]);
0790: fontItem.addActionListener(fontListener);
0791: fontItem.setFont(new Font(envfonts[i], Font.PLAIN, font
0792: .getSize()));
0793: fontMenu.add(fontItem);
0794: }
0795: }
0796: {
0797: JMenuItem sizeItem;
0798: ActionListener sizeListener = new ActionListener() {
0799: public void actionPerformed(ActionEvent ae) {
0800: try {
0801: JMenuItem source = (JMenuItem) ae.getSource();
0802: font = new Font(font.getFontName(), Font.PLAIN,
0803: Integer.parseInt(source.getText()));
0804: fontEveryWhere(font);
0805: } catch (ClassCastException e) {
0806: logger
0807: .warning("Font change started on strange object\n"
0808: + e.getLocalizedMessage());
0809: } catch (NumberFormatException e) {
0810: logger.warning("strange size entry\n"
0811: + e.getLocalizedMessage());
0812: }
0813: }
0814: };
0815: /** The list of offered font sizes */
0816: int[] sizes = { 14, 18, 22, 26, 30 };
0817: for (int i = 0; i < sizes.length; i++) {
0818: sizeItem = new JMenuItem("" + sizes[i]);
0819: sizeItem.addActionListener(sizeListener);
0820: sizeMenu.add(sizeItem);
0821: }
0822: }
0823: //font stuff over
0824:
0825: filterMenu
0826: .setToolTipText("Choosing the linearization representation format");
0827: {
0828: ActionListener filterActionListener = new ActionListener() {
0829: public void actionPerformed(ActionEvent ae) {
0830: JMenuItem jmi = (JMenuItem) ae.getSource();
0831: final String sendString = "f "
0832: + jmi.getActionCommand();
0833: send(sendString);
0834: }
0835: };
0836: JRadioButtonMenuItem jrbmi;
0837: for (int i = 0; i < filterMenuContents.length; i++) {
0838: jrbmi = new JRadioButtonMenuItem(filterMenuContents[i]);
0839: jrbmi.setActionCommand(filterMenuContents[i]);
0840: jrbmi.addActionListener(filterActionListener);
0841: filterButtonGroup.add(jrbmi);
0842: filterMenu.add(jrbmi);
0843: }
0844: }
0845: viewMenu.addSeparator();
0846: viewMenu.add(filterMenu);
0847:
0848: mlMenu
0849: .setToolTipText("the language of the entries in the refinement menu");
0850: modeMenu.add(mlMenu);
0851: /**
0852: * switches GF to either display the refinement menu commands
0853: * either in long or short format
0854: */
0855: final ActionListener longShortListener = new ActionListener() {
0856: public void actionPerformed(ActionEvent e) {
0857: String action = e.getActionCommand();
0858: if ((action.equals("long")) || (action.equals("short"))) {
0859: send("ms " + action);
0860: return;
0861: } else {
0862: logger.warning("RadioListener on wrong object: "
0863: + action
0864: + "should either be 'typed' or 'untyped'");
0865: }
0866: }
0867: };
0868:
0869: modeMenu.addSeparator();
0870: menuGroup = new ButtonGroup();
0871: rbMenuItemLong = new JRadioButtonMenuItem("long");
0872: rbMenuItemLong
0873: .setToolTipText("long format in the refinement menu, e.g. 'refine' instead of 'r'");
0874: rbMenuItemLong.setActionCommand("long");
0875: rbMenuItemLong.addActionListener(longShortListener);
0876: menuGroup.add(rbMenuItemLong);
0877: modeMenu.add(rbMenuItemLong);
0878: rbMenuItemShort = new JRadioButtonMenuItem("short");
0879: rbMenuItemShort
0880: .setToolTipText("short format in the refinement menu, e.g. 'r' instead of 'refine'");
0881: rbMenuItemShort.setActionCommand("short");
0882: rbMenuItemShort.setSelected(true);
0883: rbMenuItemShort.addActionListener(longShortListener);
0884: menuGroup.add(rbMenuItemShort);
0885: modeMenu.add(rbMenuItemShort);
0886: modeMenu.addSeparator();
0887:
0888: /**
0889: * switches GF to either display the refinement menu with or
0890: * without type annotation ala " : Type"
0891: */
0892: final ActionListener unTypedListener = new ActionListener() {
0893: public void actionPerformed(ActionEvent e) {
0894: String action = e.getActionCommand();
0895: if ((action.equals("typed"))
0896: || (action.equals("untyped"))) {
0897: send("mt " + action);
0898: if ((action.equals("typed"))) {
0899: typedMenuItems = true;
0900: } else {
0901: typedMenuItems = false;
0902: }
0903: resetPrintnames(true);
0904: return;
0905: } else {
0906: logger.warning("RadioListener on wrong object: "
0907: + action
0908: + "should either be 'typed' or 'untyped'");
0909: }
0910: }
0911: };
0912: menuGroup = new ButtonGroup();
0913: rbMenuItem = new JRadioButtonMenuItem("typed");
0914: rbMenuItem
0915: .setToolTipText("append the respective types to the entries of the refinement menu");
0916: rbMenuItem.setActionCommand("typed");
0917: rbMenuItem.addActionListener(unTypedListener);
0918: rbMenuItem.setSelected(false);
0919: menuGroup.add(rbMenuItem);
0920: modeMenu.add(rbMenuItem);
0921: rbMenuItemUnTyped = new JRadioButtonMenuItem("untyped");
0922: rbMenuItemUnTyped
0923: .setToolTipText("omit the types of the entries of the refinement menu");
0924: rbMenuItemUnTyped.setSelected(true);
0925: rbMenuItemUnTyped.setActionCommand("untyped");
0926: rbMenuItemUnTyped.addActionListener(unTypedListener);
0927: menuGroup.add(rbMenuItemUnTyped);
0928: modeMenu.add(rbMenuItemUnTyped);
0929:
0930: //usability menu
0931: subcatCbMenuItem = new JCheckBoxMenuItem(
0932: "group possible refinements");
0933: subcatCbMenuItem.setActionCommand("subcat");
0934: subcatCbMenuItem
0935: .setToolTipText("group the entries of the refinement menus as defined in the printnames for the selected menu language");
0936: subcatCbMenuItem.addActionListener(new ActionListener() {
0937: public void actionPerformed(ActionEvent e) {
0938: groupSubcat = subcatCbMenuItem.isSelected();
0939: send("gf");
0940: }
0941: });
0942: subcatCbMenuItem.setSelected(groupSubcat);
0943: usabilityMenu.add(subcatCbMenuItem);
0944:
0945: sortCbMenuItem = new JCheckBoxMenuItem("sort refinements");
0946: sortCbMenuItem.setActionCommand("sortRefinements");
0947: sortCbMenuItem
0948: .setToolTipText("sort the entries of the refinement menu");
0949: sortCbMenuItem.addActionListener(new ActionListener() {
0950: public void actionPerformed(ActionEvent e) {
0951: sortRefinements = sortCbMenuItem.isSelected();
0952: send("gf");
0953: }
0954: });
0955: sortCbMenuItem.setSelected(sortRefinements);
0956: usabilityMenu.add(sortCbMenuItem);
0957:
0958: //OCL specific stuff
0959:
0960: if (oclMode) {
0961: usabilityMenu.addSeparator();
0962: }
0963: selfresultCbMenuItem = new JCheckBoxMenuItem(
0964: "skip self&result if possible");
0965: selfresultCbMenuItem
0966: .setToolTipText("do not display self and result in the refinement menu, if they don't fit");
0967: selfresultCbMenuItem.setActionCommand("selfresult");
0968: selfresultCbMenuItem.addActionListener(new ActionListener() {
0969: public void actionPerformed(ActionEvent e) {
0970: showSelfResult = selfresultCbMenuItem.isSelected();
0971: send("gf");
0972: }
0973: });
0974: selfresultCbMenuItem.setSelected(showSelfResult);
0975: if (oclMode) {
0976: // only visible, if we really do OCL constraints
0977: usabilityMenu.add(selfresultCbMenuItem);
0978: }
0979:
0980: coerceReduceCbMenuItem = new JCheckBoxMenuItem(
0981: "only suiting subtype instances for coerce");
0982: coerceReduceCbMenuItem
0983: .setToolTipText("For coerce, where the target type is already known, show only the functions that return a subtype of this type.");
0984: coerceReduceCbMenuItem.setActionCommand("coercereduce");
0985: coerceReduceCbMenuItem.addActionListener(new ActionListener() {
0986: public void actionPerformed(ActionEvent e) {
0987: coerceReduceRM = coerceReduceCbMenuItem.isSelected();
0988: }
0989: });
0990: if (oclMode) {
0991: // only visible, if we really do OCL constraints
0992: usabilityMenu.add(coerceReduceCbMenuItem);
0993: coerceReduceRM = true;
0994: }
0995: coerceReduceCbMenuItem.setSelected(coerceReduceRM);
0996:
0997: coerceCbMenuItem = new JCheckBoxMenuItem("coerce automatically");
0998: coerceCbMenuItem
0999: .setToolTipText("Fill in coerce automatically where applicable");
1000: coerceCbMenuItem.setActionCommand("autocoerce");
1001: coerceCbMenuItem.addActionListener(new ActionListener() {
1002: public void actionPerformed(ActionEvent e) {
1003: autoCoerce = coerceCbMenuItem.isSelected();
1004: }
1005: });
1006: if (oclMode) {
1007: // only visible, if we really do OCL constraints
1008: usabilityMenu.add(coerceCbMenuItem);
1009: autoCoerce = true;
1010: }
1011: coerceCbMenuItem.setSelected(autoCoerce);
1012:
1013: highlightSubtypingErrorsCbMenuItem = new JCheckBoxMenuItem(
1014: "highlight suptyping errors");
1015: highlightSubtypingErrorsCbMenuItem
1016: .setToolTipText("Mark nodes in situations, if where a non-existing subtyping is expected.");
1017: highlightSubtypingErrorsCbMenuItem
1018: .setActionCommand("highlightsubtypingerrors");
1019: highlightSubtypingErrorsCbMenuItem
1020: .addActionListener(new ActionListener() {
1021: public void actionPerformed(ActionEvent e) {
1022: highlightSubtypingErrors = highlightSubtypingErrorsCbMenuItem
1023: .isSelected();
1024: send("[t] gf");
1025: }
1026: });
1027: if (oclMode) {
1028: // only visible, if we really do OCL constraints
1029: usabilityMenu.add(highlightSubtypingErrorsCbMenuItem);
1030: highlightSubtypingErrors = true;
1031: }
1032: highlightSubtypingErrorsCbMenuItem
1033: .setSelected(highlightSubtypingErrors);
1034:
1035: hideCoerceCbMenuItem = new JCheckBoxMenuItem(
1036: "hide coerce if completely refined");
1037: hideCoerceCbMenuItem
1038: .setToolTipText("<html>Hide coerce functions when all arguments are filled in.<br>Note that, when a subtyping error is introduced, they will be shown.</html>");
1039: hideCoerceCbMenuItem.setActionCommand("hideCoerce");
1040: hideCoerceCbMenuItem.addActionListener(new ActionListener() {
1041: public void actionPerformed(ActionEvent e) {
1042: hideCoerce = hideCoerceCbMenuItem.isSelected();
1043: //hideCoerceAggressiveCbMenuItem can only be used,
1044: //if hideCoerce is active. But its state should survive.
1045: hideCoerceAggressiveCbMenuItem.setEnabled(hideCoerce);
1046: if (hideCoerce) {
1047: hideCoerceAggressive = hideCoerceAggressiveCbMenuItem
1048: .isSelected();
1049: } else {
1050: hideCoerceAggressive = false;
1051: }
1052: send("[t] gf ", true, 0);
1053: }
1054: });
1055: if (oclMode) {
1056: // only visible, if we really do OCL constraints
1057: usabilityMenu.add(hideCoerceCbMenuItem);
1058: hideCoerce = true;
1059: }
1060: hideCoerceCbMenuItem.setSelected(hideCoerce);
1061:
1062: hideCoerceAggressiveCbMenuItem = new JCheckBoxMenuItem(
1063: "hide coerce always");
1064: hideCoerceAggressiveCbMenuItem
1065: .setActionCommand("hideCoerceAggressive");
1066: hideCoerceAggressiveCbMenuItem
1067: .setToolTipText("<html>Hide coerce functions even if the type arguments are incomplete.<br>Note that, when a subtyping error is introduced, they will be shown.</html>");
1068: hideCoerceAggressiveCbMenuItem
1069: .addActionListener(new ActionListener() {
1070: public void actionPerformed(ActionEvent e) {
1071: hideCoerceAggressive = hideCoerceAggressiveCbMenuItem
1072: .isSelected();
1073: send("[t] gf ", true, 0);
1074: }
1075: });
1076: if (oclMode) {
1077: // only visible, if we really do OCL constraints
1078: usabilityMenu.add(hideCoerceAggressiveCbMenuItem);
1079: hideCoerceAggressive = true;
1080: }
1081: hideCoerceAggressiveCbMenuItem
1082: .setSelected(hideCoerceAggressive);
1083:
1084: easyAttributesCbMenuItem = new JCheckBoxMenuItem(
1085: "directly offer attributes of 'self'");
1086: easyAttributesCbMenuItem.setActionCommand("easyAttributes");
1087: easyAttributesCbMenuItem
1088: .setToolTipText("list suiting attributes of self directly in the refinement menu");
1089: easyAttributesCbMenuItem
1090: .addActionListener(new ActionListener() {
1091: public void actionPerformed(ActionEvent e) {
1092: easyAttributes = easyAttributesCbMenuItem
1093: .isSelected();
1094: send("[t] gf ", true, 0);
1095: }
1096: });
1097: if (oclMode) {
1098: // only visible, if we really do OCL constraints
1099: usabilityMenu.add(easyAttributesCbMenuItem);
1100: easyAttributes = true;
1101: }
1102: easyAttributesCbMenuItem.setSelected(easyAttributes);
1103:
1104: //now for the other elements
1105:
1106: //HTML components
1107: this .htmlLinPane.setContentType("text/html");
1108: this .htmlLinPane.setEditable(false);
1109: if (this .htmlLinPane.getStyledDocument() instanceof HTMLDocument) {
1110: try {
1111: URL base;
1112: if (baseURL == null) {
1113: base = (new File("./")).toURL();
1114: } else {
1115: base = baseURL;
1116: }
1117: if (logger.isLoggable(Level.FINER)) {
1118: logger.finer("base for HTML: " + base);
1119: }
1120: ((HTMLDocument) this .htmlLinPane.getDocument())
1121: .setBase(base);
1122: } catch (MalformedURLException me) {
1123: logger.severe(me.getLocalizedMessage());
1124: }
1125: } else {
1126: logger.warning("No HTMLDocument: "
1127: + this .htmlLinPane.getDocument().getClass()
1128: .getName());
1129: }
1130: this .htmlLinPane.addCaretListener(new CaretListener() {
1131: /**
1132: * One can either click on a leaf in the lin area, or select a larger subtree.
1133: * The corresponding tree node is selected.
1134: */
1135: public void caretUpdate(CaretEvent e) {
1136: int start = htmlLinPane.getSelectionStart();
1137: int end = htmlLinPane.getSelectionEnd();
1138: if (popUpLogger.isLoggable(Level.FINER)) {
1139: popUpLogger.finer("CARET POSITION: "
1140: + htmlLinPane.getCaretPosition()
1141: + "\n-> SELECTION START POSITION: " + start
1142: + "\n-> SELECTION END POSITION: " + end);
1143: }
1144: if (linMarkingLogger.isLoggable(Level.FINER)) {
1145: if (end > 0
1146: && (end < htmlLinPane.getDocument()
1147: .getLength())) {
1148: try {
1149: linMarkingLogger.finer("CHAR: "
1150: + htmlLinPane.getDocument()
1151: .getText(end, 1));
1152: } catch (BadLocationException ble) {
1153: linMarkingLogger.warning(ble
1154: .getLocalizedMessage());
1155: }
1156: }
1157: }
1158: // not null selection:
1159: if (start < htmlLinPane.getDocument().getLength()) {
1160: String position = linearization
1161: .markedAreaForPosHtml(start, end);
1162: if (position != null) {
1163: send("[t] mp " + position);
1164: }
1165: }//not null selection
1166: }
1167:
1168: });
1169: this .linSplitPane = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT,
1170: this .outputPanelText, outputPanelHtml);
1171:
1172: //cp = getContentPane();
1173: JScrollPane cpPanelScroll = new JScrollPane(coverPanel);
1174: this .getContentPane().add(cpPanelScroll);
1175: coverPanel.setLayout(new BorderLayout());
1176: linearizationArea
1177: .setToolTipText("Linearizations' display area");
1178: linearizationArea.addCaretListener(new CaretListener() {
1179: /**
1180: * One can either click on a leaf in the lin area, or select a larger subtree.
1181: * The corresponding tree node is selected.
1182: */
1183: public void caretUpdate(CaretEvent e) {
1184: int start = linearizationArea.getSelectionStart();
1185: int end = linearizationArea.getSelectionEnd();
1186: if (popUpLogger.isLoggable(Level.FINER)) {
1187: popUpLogger.finer("CARET POSITION: "
1188: + linearizationArea.getCaretPosition()
1189: + "\n-> SELECTION START POSITION: " + start
1190: + "\n-> SELECTION END POSITION: " + end);
1191: }
1192: final int displayedTextLength = linearizationArea
1193: .getText().length();
1194: if (linMarkingLogger.isLoggable(Level.FINER)) {
1195: if (end > 0 && (end < displayedTextLength)) {
1196: linMarkingLogger.finer("CHAR: "
1197: + linearizationArea.getText().charAt(
1198: end));
1199: }
1200: }
1201: // not null selection:
1202: if (start < displayedTextLength) { //TODO was -1 before, why?
1203: String position = linearization
1204: .markedAreaForPosPureText(start, end);
1205: if (position != null) {
1206: send("[t] mp " + position);
1207: }
1208: }//not null selection
1209: }
1210:
1211: });
1212: linearizationArea.setEditable(false);
1213: linearizationArea.setLineWrap(true);
1214: linearizationArea.setWrapStyleWord(true);
1215:
1216: parseField.setFocusable(true);
1217: parseField.addKeyListener(new KeyListener() {
1218: /** Handle the key pressed event. */
1219: public void keyPressed(KeyEvent e) {
1220: int keyCode = e.getKeyCode();
1221: if (keyLogger.isLoggable(Level.FINER)) {
1222: keyLogger.finer("Key pressed: " + e.toString());
1223: }
1224:
1225: if (keyCode == KeyEvent.VK_ENTER) {
1226: getLayeredPane().remove(parseField);
1227: send("[t] p " + parseField.getText());
1228: if (logger.isLoggable(Level.FINE))
1229: logger.fine("sending parse string: "
1230: + parseField.getText());
1231: repaint();
1232: } else if (keyCode == KeyEvent.VK_ESCAPE) {
1233: getLayeredPane().remove(parseField);
1234: repaint();
1235: }
1236: }
1237:
1238: /**
1239: * Handle the key typed event.
1240: * We are not really interested in typed characters, thus empty
1241: */
1242: public void keyTyped(KeyEvent e) {
1243: //needed for KeyListener, but not used
1244: }
1245:
1246: /** Handle the key released event. */
1247: public void keyReleased(KeyEvent e) {
1248: //needed for KeyListener, but not used
1249: }
1250: });
1251: parseField.addFocusListener(new FocusListener() {
1252: public void focusGained(FocusEvent e) {
1253: //do nothing
1254: }
1255:
1256: public void focusLost(FocusEvent e) {
1257: getLayeredPane().remove(parseField);
1258: repaint();
1259: }
1260: });
1261: // System.out.println(output.getFont().getFontName());
1262:
1263: //Now for the command buttons in the lower part
1264: gfCommand = new JButton(gfCommandAction);
1265: read = new JButton(readAction);
1266: modify.setToolTipText("Choosing a linearization method");
1267: alpha = new JButton(alphaAction);
1268: random = new JButton(randomAction);
1269: undo = new JButton(undoAction);
1270: checkSubtyping = new JButton(new SubtypeAction());
1271: downPanel.add(gfCommand);
1272: downPanel.add(read);
1273: downPanel.add(modify);
1274: downPanel.add(alpha);
1275: downPanel.add(random);
1276: downPanel.add(undo);
1277: if (oclMode) {
1278: // only visible, if we really do OCL constraints
1279: downPanel.add(checkSubtyping);
1280: }
1281:
1282: //now for the navigation buttons
1283: leftMeta
1284: .setToolTipText("Moving the focus to the previous metavariable");
1285: rightMeta
1286: .setToolTipText("Moving the focus to the next metavariable");
1287: left.setToolTipText("Moving the focus to the previous term");
1288: right.setToolTipText("Moving the focus to the next term");
1289: top.setToolTipText("Moving the focus to the top term");
1290: middlePanelUp.add(leftMeta);
1291: middlePanelUp.add(left);
1292: middlePanelUp.add(top);
1293: middlePanelUp.add(right);
1294: middlePanelUp.add(rightMeta);
1295: middlePanelDown.add(subtermNameLabel, BorderLayout.WEST);
1296: middlePanelDown.add(subtermDescLabel, BorderLayout.CENTER);
1297: middlePanel.setLayout(new BorderLayout());
1298: middlePanel.add(middlePanelUp, BorderLayout.NORTH);
1299: middlePanel.add(middlePanelDown, BorderLayout.CENTER);
1300:
1301: //now for the upper button bar
1302: newTopic = new JButton(newTopicAction);
1303: newCategoryMenu
1304: .setToolTipText("The list of available categories to start editing");
1305: open
1306: .setToolTipText("Reading both a new environment and an editing object from file. Current editing will be discarded");
1307: save
1308: .setToolTipText("Writing the current editing object to file in the term or text format");
1309: grammar.setToolTipText("Current Topic");
1310: newTopic
1311: .setToolTipText("Reading a new environment from file. Current editing will be discarded.");
1312: upPanel.add(grammar);
1313: upPanel.add(newCategoryMenu);
1314: upPanel.add(open);
1315: upPanel.add(save);
1316: upPanel.add(newTopic);
1317:
1318: statusLabel.setToolTipText("The current focus type");
1319:
1320: tree
1321: .setToolTipText("The abstract syntax tree representation of the current editing object");
1322: tree.resetTree();
1323:
1324: bgDisplayType.add(rbText);
1325: bgDisplayType.add(rbHtml);
1326: bgDisplayType.add(rbTextHtml);
1327: if (showHtml) {
1328: rbHtml.setSelected(true);
1329: rbHtml.getAction().actionPerformed(null);
1330: } else {
1331: rbText.setSelected(true);
1332: rbText.getAction().actionPerformed(null);
1333: }
1334:
1335: viewMenu.addSeparator();
1336: viewMenu.add(rbText);
1337: viewMenu.add(rbHtml);
1338: viewMenu.add(rbTextHtml);
1339: display = new Display(displayType);
1340: linearization = new Linearization(display);
1341:
1342: statusPanel.setLayout(new GridLayout(1, 1));
1343: statusPanel.add(statusLabel);
1344: treePanel = new JSplitPane(JSplitPane.HORIZONTAL_SPLIT, tree,
1345: outputPanelUp);
1346: treePanel.setDividerSize(5);
1347: treePanel.setDividerLocation(100);
1348: centerPanel2.setLayout(new BorderLayout());
1349: gui2.setSize(350, 100);
1350: gui2.setTitle("Select Action on Subterm");
1351: gui2.setLocationRelativeTo(treePanel);
1352: centerPanelDown.setLayout(new BorderLayout());
1353: centerPanel = new JSplitPane(JSplitPane.VERTICAL_SPLIT,
1354: treePanel, centerPanelDown);
1355: centerPanel.setDividerSize(5);
1356: centerPanel.setDividerLocation(250);
1357: centerPanel.addKeyListener(tree);
1358: centerPanel.setOneTouchExpandable(true);
1359:
1360: centerPanelDown.add(middlePanel, BorderLayout.NORTH);
1361: centerPanelDown.add(refinementMenu
1362: .getRefinementListsContainer(), BorderLayout.CENTER);
1363: coverPanel.add(centerPanel, BorderLayout.CENTER);
1364: coverPanel.add(upPanel, BorderLayout.NORTH);
1365: coverPanel.add(downPanel, BorderLayout.SOUTH);
1366:
1367: newCategoryMenu.addActionListener(new ActionListener() {
1368: public void actionPerformed(ActionEvent ae) {
1369: if (!newCategoryMenu.getSelectedItem().equals("New")) {
1370: send("[nt] n " + newCategoryMenu.getSelectedItem());
1371: newCategoryMenu.setSelectedIndex(0);
1372: }
1373: }
1374:
1375: });
1376: save.setAction(saveAction);
1377: open.setAction(openAction);
1378:
1379: newCategoryMenu.setFocusable(false);
1380: save.setFocusable(false);
1381: open.setFocusable(false);
1382: newTopic.setFocusable(false);
1383: gfCommand.setFocusable(false);
1384:
1385: leftMeta.setFocusable(false);
1386: left.setFocusable(false);
1387:
1388: /** handles the clicking of the navigation buttons */
1389: ActionListener naviActionListener = new ActionListener() {
1390: /**
1391: * convenience method instead of 5 single ones
1392: */
1393: public void actionPerformed(ActionEvent ae) {
1394: Object obj = ae.getSource();
1395: if (obj == leftMeta) {
1396: send("[t] <<");
1397: }
1398: if (obj == left) {
1399: send("[t] <");
1400: }
1401: if (obj == top) {
1402: send("[t] '");
1403: }
1404: if (obj == right) {
1405: send("[t] >");
1406: }
1407: if (obj == rightMeta) {
1408: send("[t] >>");
1409: }
1410: }
1411: };
1412:
1413: top.addActionListener(naviActionListener);
1414: right.addActionListener(naviActionListener);
1415: rightMeta.addActionListener(naviActionListener);
1416: leftMeta.addActionListener(naviActionListener);
1417: left.addActionListener(naviActionListener);
1418: modify.addActionListener(new ActionListener() {
1419: public void actionPerformed(ActionEvent ae) {
1420: if (!modify.getSelectedItem().equals("Modify")) {
1421: send("[t] c " + modify.getSelectedItem());
1422: modify.setSelectedIndex(0);
1423: }
1424: }
1425: });
1426:
1427: top.setFocusable(false);
1428: right.setFocusable(false);
1429: rightMeta.setFocusable(false);
1430: read.setFocusable(false);
1431: modify.setFocusable(false);
1432: alpha.setFocusable(false);
1433: random.setFocusable(false);
1434: undo.setFocusable(false);
1435:
1436: linearizationArea.addKeyListener(tree);
1437: this .setSize(800, 600);
1438: outputPanelUp.setPreferredSize(new Dimension(400, 230));
1439: treePanel.setDividerLocation(0.3);
1440: //nodeTable.put(new TreePath(tree.rootNode.getPath()), "");
1441:
1442: JRadioButton termButton = new JRadioButton("Term");
1443: termButton.setActionCommand("term");
1444: termButton.setSelected(true);
1445: JRadioButton linButton = new JRadioButton("Text");
1446: linButton.setActionCommand("lin");
1447: // Group the radio buttons.
1448: saveTypeGroup.add(linButton);
1449: saveTypeGroup.add(termButton);
1450: JPanel buttonPanel = new JPanel();
1451: buttonPanel.setPreferredSize(new Dimension(70, 70));
1452: buttonPanel.add(new JLabel("Format:"));
1453: buttonPanel.add(linButton);
1454: buttonPanel.add(termButton);
1455: saveFc.setAccessory(buttonPanel);
1456:
1457: fontEveryWhere(font);
1458: this .setVisible(true);
1459:
1460: }
1461:
1462: /**
1463: * send a command to GF and reads the returned XML
1464: * @param text the command, exacltly the string that is going to be sent
1465: */
1466: protected void send(String text) {
1467: send(text, true, 1);
1468: }
1469:
1470: /**
1471: * send a command to GF (indirectly).
1472: * @param text the command, exactly the string that is going to be sent
1473: * @param andRead if true, the returned XML will be read an displayed accordingly
1474: * @param undoSteps How many undo steps need to be done to undo this command.
1475: * If undoSteps == 0, then nothing is done. If it is < 0, it gets
1476: * subtracted from the last number on the undoStack. That way, both
1477: * this command and the last one get undone together (since the undo
1478: * value is actually increased).
1479: */
1480: protected void send(String text, boolean andRead, int undoSteps) {
1481: if (sendLogger.isLoggable(Level.FINE)) {
1482: sendLogger.fine("## send: '" + text + "', undo steps: "
1483: + undoSteps);
1484: }
1485:
1486: this .display.resetLin();
1487: display(false, true, false);
1488: linearization.reset();
1489: if (undoSteps > 0) { //undo itself should not push sth. on the stack, only pop
1490: undoStack.push(new Integer(undoSteps));
1491: } else if (undoSteps < 0) {
1492: final int oldUndo = ((Integer) undoStack.pop()).intValue();
1493: final int newUndo = oldUndo - undoSteps;
1494: if (sendLogger.isLoggable(Level.FINER)) {
1495: sendLogger.finer("modified undoStack, top was "
1496: + oldUndo + ", but is now: " + newUndo);
1497: }
1498: undoStack.push(new Integer(newUndo));
1499: }
1500: gfCapsule.realSend(text);
1501:
1502: if (andRead) {
1503: processGfedit();
1504: }
1505: }
1506:
1507: /**
1508: * Asks the respective read methods to read the front matter of GF.
1509: * That can be the greetings and loading messages.
1510: * The latter are always read.
1511: * When <gfinit> is read, the function returns.
1512: * @param pm to monitor the loading progress. May be null
1513: * @param greetingsToo if the greeting text from GF is expected
1514: */
1515: private void processInit(ProgressMonitor pm, boolean greetingsToo) {
1516: String next = null;
1517: if (greetingsToo) {
1518: StringTuple greetings = gfCapsule.readGfGreetings();
1519: next = greetings.first;
1520: this .display.addToStages(greetings.second, greetings.second
1521: .replaceAll("\\n", "<br>"));
1522: display(true, true, false);
1523: }
1524: Utils.tickProgress(pm, 5300, null);
1525: StringTuple loading = gfCapsule.readGfLoading(next, pm);
1526: next = loading.first;
1527: this .display.addToStages(loading.second, Utils.replaceAll(
1528: loading.second, "\n", "<br>\n"));
1529: display(true, true, false);
1530:
1531: if (next.equals("<gfinit>")) {
1532: processGfinit();
1533: }
1534: }
1535:
1536: /**
1537: * Takes care of reading the <gfinit> part
1538: * Fills the new category menu.
1539: */
1540: private void processGfinit() {
1541: NewCategoryMenuResult ncmr = gfCapsule.readGfinit();
1542: if (ncmr != null) {
1543: formNewMenu(ncmr);
1544: }
1545: }
1546:
1547: /**
1548: * Takes care of reading the output from GF starting with
1549: * >gfedit< and last reads >/gfedit<.
1550: * Feeds the editor with what was read.
1551: * This makes this method nearly the central method of the editor.
1552: */
1553: private void processGfedit() {
1554: final GfeditResult gfedit = gfCapsule.readGfedit(newObject);
1555: formHmsg(gfedit.hmsg);
1556: //now the form methods are called:
1557: DefaultMutableTreeNode topNode = null;
1558: TreeAnalysisResult tar = new TreeAnalysisResult(null, -1,
1559: false, true, false, false, null, null);
1560: TreeAnalyser treeAnalyser = new TreeAnalyser(autoCoerce,
1561: coerceReduceRM, easyAttributes, hideCoerce,
1562: hideCoerceAggressive, highlightSubtypingErrors,
1563: showSelfResult);
1564: if (gfedit.hmsg.treeChanged && newObject) {
1565: topNode = formTree(gfedit.treeString);
1566: tar = treeAnalyser.analyseTree(topNode);
1567: focusPosition = tar.focusPosition;
1568: currentNode = tar.currentNode;
1569: }
1570: //only sent sth. to GF directly, if we have sth. to send, and if it is not forbidden
1571: if (tar.command == null || !gfedit.hmsg.recurse) {
1572: //for normal grammars (not the OCL ones),
1573: //the nextCommand feature is not used, thus
1574: //only this branch is executed.
1575:
1576: // nothing special is to be done here,
1577: // the tree analysis has
1578: // not told us to send sth. to GF,
1579: // so display the rest and do most of the
1580: // expensive stuff
1581:
1582: if (topNode != null) { //the case of !treeChanged or !newObject
1583: DefaultMutableTreeNode transformedTreeRoot = TreeAnalyser
1584: .transformTree(topNode);
1585: showTree(tree, transformedTreeRoot);
1586: }
1587:
1588: if (gfedit.gfCommands != null) {
1589: final Vector usedCommandVector = RefinementMenuTransformer
1590: .transformRefinementMenu(tar,
1591: gfedit.gfCommands, gfCapsule);
1592: final boolean isAbstract = "Abstract"
1593: .equals(selectedMenuLanguage);
1594: refinementMenu.formRefinementMenu(usedCommandVector,
1595: gfedit.hmsg.appendix, currentNode, isAbstract,
1596: tar.easyAttributes && tar.reduceCoerce,
1597: focusPosition, gfCapsule);
1598: }
1599: if (newObject) {
1600: //MUST come after readLin, but since formLin is called later on too,
1601: //this cannot be enforced with a local this.linearization
1602: String linString = gfedit.linearizations;
1603: //is set only here, when it is fresh
1604: linearization.setLinearization(linString);
1605: formLin();
1606: }
1607: if (gfedit.message != null && gfedit.message.length() > 1) {
1608: logger.fine("message found: '" + gfedit.message + "'");
1609: this .display.addToStages("\n-------------\n"
1610: + gfedit.message, "<br><hr>" + gfedit.message);
1611: //in case no language is displayed
1612: display(true, false, false);
1613: }
1614: } else {
1615: // OK, sth. has to be sent to GF without displaying
1616: // the linearization of this run
1617: send(tar.command, true, -tar.undoSteps);
1618: }
1619: refinementMenu.requestFocus();
1620: }
1621:
1622: /**
1623: * prints the available command line options
1624: */
1625: private static void printUsage() {
1626: System.err
1627: .println("Usage: java -jar [-h/--html] [-b/--base baseURL] [-o/--ocl] [grammarfile(s)]");
1628: System.err.println("where -h activates the HTML mode");
1629: System.err
1630: .println("and -b sets the base location to which links in HTML are relative to. "
1631: + "Default is the current directory.");
1632: }
1633:
1634: /**
1635: * starts the editor
1636: * @param args only the first parameter is used, it has to be a complete GF command,
1637: * which is executed and thus should load the needed grammars
1638: */
1639: public static void main(String args[]) {
1640: //command line parsing
1641: CmdLineParser parser = new CmdLineParser();
1642: CmdLineParser.Option optHtml = parser.addBooleanOption('h',
1643: "html");
1644: CmdLineParser.Option optBase = parser.addStringOption('b',
1645: "base");
1646: CmdLineParser.Option optOcl = parser.addBooleanOption('o',
1647: "ocl");
1648: CmdLineParser.Option gfBin = parser.addStringOption('g',
1649: "gfbin");
1650: // Parse the command line options.
1651:
1652: try {
1653: parser.parse(args);
1654: } catch (CmdLineParser.OptionException e) {
1655: System.err.println(e.getMessage());
1656: printUsage();
1657: System.exit(2);
1658: }
1659: Boolean isHtml = (Boolean) parser.getOptionValue(optHtml,
1660: Boolean.FALSE);
1661: String baseString = (String) parser.getOptionValue(optBase,
1662: null);
1663: String gfBinString = (String) parser
1664: .getOptionValue(gfBin, null);
1665: Boolean isOcl = (Boolean) parser.getOptionValue(optOcl,
1666: Boolean.FALSE);
1667: String[] otherArgs = parser.getRemainingArgs();
1668:
1669: URL myBaseURL;
1670: if (baseString != null) {
1671: try {
1672: myBaseURL = new URL(baseString);
1673: } catch (MalformedURLException me) {
1674: logger.warning(me.getLocalizedMessage());
1675: me.printStackTrace();
1676: myBaseURL = null;
1677: }
1678: } else {
1679: myBaseURL = null;
1680: }
1681:
1682: // if (logger.isLoggable(Level.FINER)) {
1683: // logger.finer(isHtml + " : " + baseString + " : " + otherArgs);
1684: // }
1685: //construct the call to GF
1686: String gfName = ((gfBinString != null && !gfBinString
1687: .equals("")) ? gfBinString : "gf");
1688: String[] gfCall = new String[2 + otherArgs.length];
1689: gfCall[0] = gfName;
1690: gfCall[1] = "-java";
1691: for (int i = 0; i < otherArgs.length; i++) {
1692: gfCall[2 + i] = otherArgs[i];
1693: }
1694: Locale.setDefault(Locale.US);
1695: logger.info("call to GF: " + gfCall);
1696: GFEditor2 gui = new GFEditor2(gfCall, isHtml.booleanValue(),
1697: myBaseURL, isOcl.booleanValue());
1698: if (logger.isLoggable(Level.FINER)) {
1699: logger.finer("main finished");
1700: }
1701: }
1702:
1703: /**
1704: * Calls the Java GF GUI to edit an OCL constraint. To be called by GFinterface
1705: * @param gfCmd the command to start the GF, must include the -java and all modules
1706: * @param callback the callback class that knows how to store the constraints
1707: * @param initAbs the initial abstract syntax tree (not OCL)
1708: * @param initDefault if initAbs is empty, then initDefault is used
1709: * @param pm to monitor the loading progress. May be null
1710: */
1711: static void mainConstraint(String[] gfCmd,
1712: ConstraintCallback callback, String initAbs,
1713: String initDefault, ProgressMonitor pm) {
1714: Locale.setDefault(Locale.US);
1715: GFEditor2 gui;
1716: if (initAbs.equals("")) {
1717: gui = new GFEditor2(gfCmd, callback, "[ctn] g "
1718: + initDefault, pm);
1719: } else {
1720: gui = new GFEditor2(gfCmd, callback, "[ctn] g " + initAbs,
1721: pm);
1722: }
1723:
1724: }
1725:
1726: /**
1727: * we should not end the program, just close the GF editor
1728: * possibly sending something back to KeY
1729: */
1730: private void endProgram() {
1731: String saveQuestion;
1732: if (this .callback == null) {
1733: saveQuestion = "Save text before exiting?";
1734: } else {
1735: send("' ;; >>");
1736: if (this .currentNode.isMeta()) {
1737: saveQuestion = "Incomplete OCL found.\nThis can only be saved (and loaded again) in an internal representation.\nStill save before exiting?";
1738: } else {
1739: saveQuestion = "Save constraint before exiting?";
1740: }
1741: }
1742: int returnStatus;
1743: if (this .newObject) {
1744: returnStatus = JOptionPane.showConfirmDialog(this ,
1745: saveQuestion, "Save before quitting?",
1746: JOptionPane.YES_NO_CANCEL_OPTION,
1747: JOptionPane.QUESTION_MESSAGE);
1748: } else {
1749: returnStatus = JOptionPane.NO_OPTION;
1750: }
1751: if (returnStatus == JOptionPane.CANCEL_OPTION) {
1752: return;
1753: } else if (returnStatus == JOptionPane.NO_OPTION) {
1754: shutDown();
1755: return;
1756: }
1757: if (this .callback != null) {
1758: try {
1759: // quit should always work even if we cannot send something proper
1760: // back to Together/KeY.
1761: // Hence this try-catch
1762: if (returnStatus == JOptionPane.YES_OPTION) {
1763: //check, if there are open metavariables
1764: //send("' ;; >>"); already done above
1765: if (!this .currentNode.isMeta()) {
1766: logger
1767: .info("No metavariables found, saving OCL");
1768: //no open nodes, we can save OCL
1769: String ocl = (String) linearization
1770: .getLinearizations().get(
1771: modelModulName + "OCL");
1772: if (ocl == null) {
1773: //OCL not present, so switch it on
1774: langMenuModel.setActive(modelModulName
1775: + "OCL", true);
1776: send("on " + modelModulName + "OCL");
1777: ocl = (String) linearization
1778: .getLinearizations().get(
1779: modelModulName + "OCL");
1780: }
1781: ocl = Utils.compactSpaces(ocl.trim()).trim();
1782:
1783: this .callback.sendConstraint(ocl);
1784: } else {
1785: logger.info("Metavariables found, saving AST");
1786: //Abstract is always present
1787: String abs = (String) linearization
1788: .getLinearizations().get("Abstract");
1789: //then remove duplicate white space
1790: abs = removeMetavariableNumbers(abs)
1791: .replaceAll("\\s+", " ").trim();
1792: this .callback.sendAbstract(abs);
1793: }
1794:
1795: }
1796: } catch (Exception e) { // just print information about the exception
1797: System.err
1798: .println("GFEditor2.endProgram() Caught an Exception.");
1799: System.err.println("e.getLocalizedMessage(): "
1800: + e.getLocalizedMessage());
1801: System.err.println("e.toString(): " + e);
1802: System.err.println("e.printStackTrace():");
1803: e.printStackTrace(System.err);
1804: } finally {
1805: if (this .callback != null) { // send linearization as a class invariant
1806: Utils
1807: .cleanupFromUMLTypes(callback
1808: .getGrammarsDir());
1809: }
1810: shutDown();
1811: }
1812: } else if (returnStatus == JOptionPane.YES_OPTION) {
1813: final Action saveAction = new SaveAction();
1814: saveAction.actionPerformed(null);
1815: shutDown();
1816: }
1817: }
1818:
1819: /**
1820: * In the GF AST, all metavariables have numbers behind them,
1821: * like ?4. But GF cannot parse these, so the numbers have to be
1822: * removed.
1823: * Be aware, that this method also replaces ?n inside String literals!
1824: * @param abs The GF AST
1825: * @return abs, but without numbers behind the '?'
1826: */
1827: private static String removeMetavariableNumbers(String abs) {
1828: return abs.replaceAll("\\?\\d+", "\\?");
1829: }
1830:
1831: /**
1832: * Shuts down GF and terminates the edior
1833: */
1834: private void shutDown() {
1835: try {
1836: send("q", false, 1); // tell external GF process to quit
1837: } finally {
1838: removeAll();
1839: dispose();
1840: }
1841: }
1842:
1843: /**
1844: * Performs some global settings like setting treeChanged and newObject,
1845: * which can depend on the hmsg.
1846: * Also the display gets cleared of wished so.
1847: * @param hmsg The parsed hmsg.
1848: */
1849: private void formHmsg(Hmsg hmsg) {
1850: if (hmsg.clear) {
1851: //clear output before linearization
1852: this .display.resetLin();
1853: display(true, false, false);
1854: linearization.reset();
1855: }
1856: if (hmsg.newObject) {
1857: this .newObject = true;
1858: }
1859: }
1860:
1861: /**
1862: * Fills the new category menu and sets the label 'grammar' to
1863: * display the name of the abstract grammar.
1864: * Fills langMenuModel and registers the presence of the
1865: * loaded languages in linearization.linearizations.
1866: */
1867: private void formNewMenu(NewCategoryMenuResult nmr) {
1868: //fill newCategoryMenu
1869: for (int i = 0; i < nmr.menuContent.length; i++) {
1870: newCategoryMenu.addItem(nmr.menuContent[i]);
1871: }
1872: //add the languages to the menu
1873: for (int i = 0; i < nmr.languages.length; i++) {
1874: final boolean active;
1875: if (nmr.languages[i].equals("Abstract")) {
1876: active = false;
1877: } else {
1878: active = true;
1879: }
1880: this .langMenuModel.add(nmr.languages[i], active);
1881:
1882: //select FromUMLTypesOCL by default
1883: if (nmr.languages[i].equals(modelModulName + "OCL")) {
1884: this .selectedMenuLanguage = modelModulName + "OCL";
1885: //TODO select OCL also in the menu
1886: }
1887: //'register' the presence of this language if possible
1888: if (linearization != null) {
1889: linearization.getLinearizations().put(nmr.languages[i],
1890: null);
1891: }
1892: }
1893: //tell the user, which abstract grammar is used
1894: //and save the import path
1895: grammar.setText(nmr.grammarName);
1896: for (int i = 0; i < nmr.paths.length; i++) {
1897: fileString += "--" + nmr.paths[i] + "\n";
1898: if (nmr.paths[i].lastIndexOf('.') != nmr.paths[i]
1899: .indexOf('.'))
1900: grammar.setText(nmr.paths[i].substring(0,
1901: nmr.paths[i].indexOf('.')).toUpperCase()
1902: + " ");
1903: }
1904:
1905: }
1906:
1907: /**
1908: * Parses the GF-output between <linearization> </linearization> tags
1909: *
1910: * Expects the linearization string to be given to this.linearization.
1911: */
1912: private void formLin() {
1913: //reset previous output
1914: this .display.resetLin();
1915:
1916: linearization.parseLin(langMenuModel);
1917: display(true, false, true);
1918:
1919: //do highlighting
1920: this .linearizationArea.getHighlighter().removeAllHighlights();
1921: this .htmlLinPane.getHighlighter().removeAllHighlights();
1922:
1923: Vector mahsVector = linearization
1924: .calculateHighlights(focusPosition);
1925: for (Iterator it = mahsVector.iterator(); it.hasNext();) {
1926: MarkedAreaHighlightingStatus mahs = (MarkedAreaHighlightingStatus) it
1927: .next();
1928: //now highlight
1929: if (mahs.focused && mahs.incorrect) {
1930: highlight(mahs.ma, Color.ORANGE);
1931: highlightHtml(mahs.ma, Color.ORANGE);
1932: } else if (mahs.focused) {
1933: highlight(mahs.ma, linearizationArea
1934: .getSelectionColor());
1935: highlightHtml(mahs.ma, linearizationArea
1936: .getSelectionColor());
1937: } else if (mahs.incorrect) {
1938: highlight(mahs.ma, Color.RED);
1939: highlightHtml(mahs.ma, Color.RED);
1940: }
1941: }
1942: }
1943:
1944: /**
1945: * Small method that takes this.display and displays its content
1946: * accordingly to what it is (pure text/HTML)
1947: * @param doDisplay If the text should get displayed
1948: * @param saveScroll if the old scroll state should be saved
1949: * @param restoreScroll if the old scroll state should be restored
1950: */
1951: private void display(boolean doDisplay, boolean saveScroll,
1952: boolean restoreScroll) {
1953: //Display the pure text
1954: final String text = this .display.getText();
1955: if (doDisplay) {
1956: this .linearizationArea.setText(text);
1957: }
1958: if (restoreScroll) {
1959: //this.outputPanelText.getVerticalScrollBar().setValue(this.display.scrollText);
1960: this .linearizationArea
1961: .scrollRectToVisible(this .display.recText);
1962: }
1963: if (saveScroll) {
1964: //this.display.scrollText = this.outputPanelText.getVerticalScrollBar().getValue();
1965: this .display.recText = this .linearizationArea
1966: .getVisibleRect();
1967: }
1968:
1969: //Display the HTML
1970: final String html = this .display.getHtml(this .font);
1971: if (doDisplay) {
1972: this .htmlLinPane.setText(html);
1973: }
1974: if (restoreScroll) {
1975: //this.outputPanelHtml.getVerticalScrollBar().setValue(this.display.scrollHtml);
1976: this .htmlLinPane.scrollRectToVisible(this .display.recHtml);
1977: }
1978: if (saveScroll) {
1979: //this.display.scrollHtml = this.outputPanelHtml.getVerticalScrollBar().getValue();
1980: this .display.recHtml = this .htmlLinPane.getVisibleRect();
1981: }
1982: }
1983:
1984: /**
1985: * Highlights the given MarkedArea in htmlLinPane
1986: * @param ma the MarkedArea
1987: * @param color the color the highlight should get
1988: */
1989: private void highlightHtml(final MarkedArea ma, Color color) {
1990: try {
1991: int begin = ma.htmlBegin;
1992: int end = ma.htmlEnd;
1993: //When creating the HtmlMarkedArea, we don't know, if
1994: //it is going to be the last or not.
1995: if (end > this .htmlLinPane.getDocument().getLength()) {
1996: end = this .htmlLinPane.getDocument().getLength();
1997: }
1998: this .htmlLinPane.getHighlighter().addHighlight(
1999: begin,
2000: end,
2001: new DefaultHighlighter.DefaultHighlightPainter(
2002: color));
2003: if (redLogger.isLoggable(Level.FINER)) {
2004: redLogger.finer("HTML HIGHLIGHT: "
2005: + this .htmlLinPane.getDocument().getText(begin,
2006: end - begin) + "; Color:" + color);
2007: }
2008: } catch (BadLocationException e) {
2009: redLogger.warning("HTML highlighting problem!\n"
2010: + e.getLocalizedMessage() + " : "
2011: + e.offsetRequested() + "\nHtmlMarkedArea: " + ma
2012: + "\nhtmlLinPane length: "
2013: + this .htmlLinPane.getDocument().getLength());
2014: }
2015: }
2016:
2017: /**
2018: * Highlights the given MarkedArea in linearizationArea
2019: * @param ma the MarkedArea
2020: * @param color the color the highlight should get
2021: */
2022: private void highlight(final MarkedArea ma, Color color) {
2023: try {
2024: int begin = ma.begin;
2025: int end = ma.end;
2026: //When creating the MarkedArea, we don't know, if
2027: //it is going to be the last or not.
2028: if (end > this .linearizationArea.getText().length()) {
2029: end = this .linearizationArea.getText().length() + 1;
2030: }
2031: this .linearizationArea.getHighlighter().addHighlight(
2032: begin,
2033: end,
2034: new DefaultHighlighter.DefaultHighlightPainter(
2035: color));
2036: if (redLogger.isLoggable(Level.FINER)) {
2037: redLogger.finer("HIGHLIGHT: "
2038: + this .linearizationArea.getText(begin, end
2039: - begin) + "; Color:" + color);
2040: }
2041: } catch (BadLocationException e) {
2042: redLogger.warning("highlighting problem!\n"
2043: + e.getLocalizedMessage() + " : "
2044: + e.offsetRequested() + "\nMarkedArea: " + ma
2045: + "\nlinearizationArea length: "
2046: + this .linearizationArea.getText().length());
2047: }
2048: }
2049:
2050: /**
2051: * Sets the font on all the GUI-elements to font.
2052: * @param newFont the font everything should have afterwards
2053: */
2054: private void fontEveryWhere(Font newFont) {
2055: linearizationArea.setFont(newFont);
2056: htmlLinPane.setFont(newFont);
2057: parseField.setFont(newFont);
2058: tree.tree.setFont(newFont);
2059: refinementMenu.setFont(newFont);
2060: save.setFont(newFont);
2061: grammar.setFont(newFont);
2062: open.setFont(newFont);
2063: newTopic.setFont(newFont);
2064: gfCommand.setFont(newFont);
2065: leftMeta.setFont(newFont);
2066: left.setFont(newFont);
2067: top.setFont(newFont);
2068: right.setFont(newFont);
2069: rightMeta.setFont(newFont);
2070: subtermDescLabel.setFont(newFont);
2071: subtermNameLabel.setFont(newFont);
2072: read.setFont(newFont);
2073: alpha.setFont(newFont);
2074: random.setFont(newFont);
2075: undo.setFont(newFont);
2076: checkSubtyping.setFont(newFont);
2077: filterMenu.setFont(newFont);
2078: setSubmenuFont(filterMenu, newFont, false);
2079: modify.setFont(newFont);
2080: statusLabel.setFont(newFont);
2081: menuBar.setFont(newFont);
2082: newCategoryMenu.setFont(newFont);
2083: readDialog.setFont(newFont);
2084: mlMenu.setFont(newFont);
2085: setSubmenuFont(mlMenu, newFont, false);
2086: modeMenu.setFont(newFont);
2087: setSubmenuFont(modeMenu, newFont, false);
2088: langMenu.setFont(newFont);
2089: setSubmenuFont(langMenu, newFont, false);
2090: fileMenu.setFont(newFont);
2091: setSubmenuFont(fileMenu, newFont, false);
2092: usabilityMenu.setFont(newFont);
2093: setSubmenuFont(usabilityMenu, newFont, false);
2094: viewMenu.setFont(newFont);
2095: setSubmenuFont(viewMenu, newFont, false);
2096: setSubmenuFont(sizeMenu, newFont, false);
2097: setSubmenuFont(fontMenu, newFont, true);
2098: //update also the HTML with the new size
2099: display(true, false, true);
2100: }
2101:
2102: /**
2103: * Set the font in the submenus of menu.
2104: * Recursion depth is 1, so subsubmenus don't get fontified.
2105: * @param subMenu The menu whose submenus should get fontified
2106: * @param font the chosen font
2107: * @param onlySize If only the font size or the whole font should
2108: * be changed
2109: */
2110: private void setSubmenuFont(JMenu subMenu, Font font,
2111: boolean onlySize) {
2112: for (int i = 0; i < subMenu.getItemCount(); i++) {
2113: JMenuItem item = subMenu.getItem(i);
2114: if (item != null) {
2115: //due to a bug in the jvm (already reported) deactivated
2116: if (false && onlySize) {
2117: Font newFont = new Font(item.getFont().getName(),
2118: Font.PLAIN, font.getSize());
2119: item.setFont(newFont);
2120: } else {
2121: item.setFont(font);
2122: }
2123: //String name = item.getClass().getName();
2124: //if (logger.isLoggable(Level.FINER)) logger.finer(name);
2125: }
2126: }
2127: }
2128:
2129: /**
2130: * Writes the given String to the given Filename
2131: * @param str the text to be written
2132: * @param fileName the name of the file that is to be filled
2133: */
2134: static void writeOutput(String str, String fileName) {
2135:
2136: try {
2137: FileOutputStream fos = new FileOutputStream(fileName);
2138: Writer out = new OutputStreamWriter(fos, "UTF8");
2139: out.write(str);
2140: out.close();
2141: } catch (IOException e) {
2142: JOptionPane.showMessageDialog(null, "Document is empty!",
2143: "Error", JOptionPane.ERROR_MESSAGE);
2144: }
2145: }
2146:
2147: /**
2148: * Parses the GF-output between <tree> </tree> tags
2149: * and build the corresponding tree.
2150: *
2151: * parses the already read XML for the tree and stores the tree nodes
2152: * in nodeTable with their numbers as keys
2153: *
2154: * Also does some tree analyzing, if other actions have to be taken.
2155: *
2156: * @param treeString the string representation for the XML tree
2157: * @return null, if no commands have to be executed afterwards.
2158: * If the result is non-null, then result.s should be sent to GF
2159: * afterwards, and no other form-method on this read-run is to be executed.
2160: * result.i is the amount of undo steps that this command needs.
2161: */
2162: private DefaultMutableTreeNode formTree(String treeString) {
2163: if (treeLogger.isLoggable(Level.FINER)) {
2164: treeLogger.finer("treeString: " + treeString);
2165: }
2166:
2167: /**
2168: * stores the nodes and the indention of their children.
2169: * When all children of a node are read,
2170: * the next brethren / uncle node 'registers' with the same
2171: * indention depth to show that the next children are his.
2172: */
2173: Hashtable parentNodes = new Hashtable();
2174: String s = treeString;
2175: /** consecutive node numbering */
2176: int index = 0;
2177: /** the node that gets created from the current line */
2178: DefaultMutableTreeNode newChildNode = null;
2179: /** is a star somewhere in treestring? 1 if so, 0 otherwise */
2180: int star = 0;
2181: if (s.indexOf('*') != -1) {
2182: star = 1;
2183: }
2184: DefaultMutableTreeNode topNode = null;
2185: while (s.length() > 0) {
2186: /**
2187: * every two ' ' indicate one tree depth level
2188: * shift first gets assigned the indention depth in
2189: * characters, later the tree depth
2190: */
2191: int shift = 0;
2192: boolean selected = false;
2193: while ((s.length() > 0)
2194: && ((s.charAt(0) == '*') || (s.charAt(0) == ' '))) {
2195: if (s.charAt(0) == '*') {
2196: selected = true;
2197: }
2198: s = s.substring(1);
2199: shift++;
2200: }
2201: if (s.length() > 0) {
2202: /** to save the top node*/
2203: boolean isTop = false;
2204: int j = s.indexOf("\n");
2205: //is sth like "andS : Sent ", i.e. "fun : type " before trimming
2206: String gfline = s.substring(0, j).trim();
2207: GfAstNode node = new GfAstNode(gfline);
2208: // use indentation to calculate the parent
2209: index++;
2210: s = s.substring(j + 1);
2211: shift = (shift - star) / 2;
2212:
2213: /**
2214: * we know the parent, so we can ask it for the param information
2215: * for the next child (the parent knows how many it has already)
2216: * and save it in an AstNodeData
2217: */
2218: DefaultMutableTreeNode parent = (DefaultMutableTreeNode) parentNodes
2219: .get(new Integer(shift));
2220:
2221: /** compute the now child's position */
2222: String newPos;
2223: if ((parent != null)
2224: && (parent.getUserObject() instanceof AstNodeData)
2225: && parent.getUserObject() != null) {
2226: AstNodeData pand = (AstNodeData) parent
2227: .getUserObject();
2228: newPos = LinPosition.calculateChildPosition(
2229: pand.position, pand.childNum++);
2230: } else {
2231: //only the case for the root node
2232: newPos = "[]";
2233: isTop = true;
2234: }
2235:
2236: //default case, if we can get more information, this is overwritten
2237: AstNodeData and;
2238: Printname childPrintname = null;
2239: if (!node.isMeta()) {
2240: childPrintname = this .printnameManager
2241: .getPrintname(node.getFun());
2242: }
2243: Printname parentPrintname = null;
2244: AstNodeData parentAnd = null;
2245: String parentConstraint = "";
2246: if (parent != null) {
2247: parentAnd = (AstNodeData) parent.getUserObject();
2248: if (parentAnd != null) {
2249: parentConstraint = parentAnd.constraint;
2250: }
2251: }
2252: if (childPrintname != null) {
2253: //we know this one
2254: and = new RefinedAstNodeData(childPrintname, node,
2255: newPos, selected, parentConstraint);
2256: } else if (parent != null && node.isMeta()) {
2257: //new child without refinement
2258: if (parentAnd != null) {
2259: parentPrintname = parentAnd.getPrintname();
2260: }
2261: if (parentPrintname != null) {
2262: int paramPosition = parent.getChildCount();
2263: String paramName = parentPrintname
2264: .getParamName(paramPosition);
2265: if (paramName == null) {
2266: paramName = node.getFun();
2267: }
2268: //if tooltip turns out to be null that's OK
2269: String paramTooltip = parentPrintname
2270: .htmlifySingleParam(paramPosition);
2271: // if (logger.isLoggable(Level.FINER)) {
2272: // logger.finer("new node-parsing: '" + name + "', fun: '" + fun + "', type: '" + paramType + "'");
2273: // }
2274: and = new UnrefinedAstNodeData(paramTooltip,
2275: node, newPos, selected,
2276: parentConstraint);
2277:
2278: } else {
2279: and = new RefinedAstNodeData(null, node,
2280: newPos, selected, parentConstraint);
2281: }
2282: } else {
2283: //something unparsable, bad luck
2284: //or refined and not described
2285: and = new RefinedAstNodeData(null, node, newPos,
2286: selected, parentConstraint);
2287: }
2288:
2289: //add to the parent node
2290: newChildNode = new DefaultMutableTreeNode(and);
2291: if (parent != null) {
2292: parent.add(newChildNode);
2293: }
2294: parentNodes.put(new Integer(shift + 1), newChildNode);
2295: if (isTop) {
2296: topNode = newChildNode;
2297: }
2298: }
2299: }
2300: //to be deferred to later step in readGfEdit
2301: return topNode;
2302: }
2303:
2304: /**
2305: * Shows the tree, scrolls to the selected node and updates the
2306: * mapping table between displayed node paths and AST positions.
2307: * @param myTreePanel the panel of GFEditor2
2308: * @param topNode The root node of the tree, that has the other nodes
2309: * already as its children
2310: */
2311: private void showTree(DynamicTree2 myTreePanel,
2312: DefaultMutableTreeNode topNode) {
2313: myTreePanel.clear();
2314: nodeTable.clear();
2315: //the rootNode is not shown, therefore, a dummy node plays this role
2316: final DefaultMutableTreeNode rootNode = new DefaultMutableTreeNode();
2317: rootNode.add(topNode);
2318: ((DefaultTreeModel) (myTreePanel.tree.getModel()))
2319: .setRoot(rootNode);
2320: /**
2321: * the path in the JTree (not in GF repesentation!) to the
2322: * current new node.
2323: */
2324: TreePath path = null;
2325: TreePath selectionPath = null;
2326: // now fill nodeTable
2327: for (Enumeration e = rootNode.breadthFirstEnumeration(); e
2328: .hasMoreElements();) {
2329: DefaultMutableTreeNode currNode = (DefaultMutableTreeNode) e
2330: .nextElement();
2331: AstNodeData and = (AstNodeData) currNode.getUserObject();
2332:
2333: path = new TreePath(currNode.getPath());
2334: if (and == null) {
2335: //only the case for the root node
2336: nodeTable.put(path, "[]");
2337: } else {
2338: nodeTable.put(path, and.position);
2339: if (and.selected) {
2340: selectionPath = path;
2341: if (treeLogger.isLoggable(Level.FINE)) {
2342: treeLogger.fine("new selectionPath: "
2343: + selectionPath);
2344: }
2345:
2346: DefaultMutableTreeNode parent = null;
2347: if (currNode.getParent() instanceof DefaultMutableTreeNode) {
2348: parent = (DefaultMutableTreeNode) currNode
2349: .getParent();
2350: }
2351: Printname parentPrintname = null;
2352: //display the current refinement description
2353: if ((parent != null)
2354: && (parent.getUserObject() != null)
2355: && (parent.getUserObject() instanceof AstNodeData)) {
2356: AstNodeData parentAnd = (AstNodeData) parent
2357: .getUserObject();
2358: parentPrintname = parentAnd.getPrintname();
2359: }
2360: // set the description of the current parameter to a more
2361: // prominent place
2362: String paramName = null;
2363: int paramPosition = -1;
2364: if (parentPrintname != null) {
2365: paramPosition = parent.getIndex(currNode);
2366: paramName = parentPrintname
2367: .getParamName(paramPosition);
2368: }
2369: if (paramName == null) {
2370: subtermNameLabel.setText(actionOnSubtermString);
2371: subtermDescLabel.setText("");
2372: } else {
2373: subtermNameLabel.setText("<html><b>"
2374: + paramName + ": </b></html>");
2375: String paramDesc = parentPrintname
2376: .getParamDescription(paramPosition);
2377: if (paramDesc == null) {
2378: subtermDescLabel.setText("");
2379: } else {
2380: subtermDescLabel.setText("<html>"
2381: + paramDesc + "</html>");
2382: }
2383: }
2384: statusLabel.setText(and.node.getType());
2385: }
2386: }
2387: }
2388: //also set the old selectionPath since we know that we do know,
2389: //that the selectionChanged event is bogus.
2390: myTreePanel.oldSelection = selectionPath;
2391: myTreePanel.tree.setSelectionPath(selectionPath);
2392: myTreePanel.tree.scrollPathToVisible(selectionPath);
2393: //show the selected as the 'selected' one in the JTree
2394: myTreePanel.tree.makeVisible(selectionPath);
2395: gui2.toFront();
2396: }
2397:
2398: /**
2399: * Removes anything but the "new" from the new category menu
2400: */
2401: private void resetNewCategoryMenu() {
2402: //remove everything except "New"
2403: while (1 < newCategoryMenu.getItemCount())
2404: newCategoryMenu.removeItemAt(1);
2405: }
2406:
2407: /**
2408: * Pops up a window for input of the wanted data and asks ic
2409: * afterwards, if the data has the right format.
2410: * Then gives that to GF.
2411: * TODO Is called from RefinementMenu, but uses display. Where to put?
2412: * @param ic the InputCommand that specifies the wanted format/type
2413: */
2414: protected void executeInputCommand(InputCommand ic) {
2415: String s = (String) JOptionPane.showInputDialog(this , ic
2416: .getTitleText(), ic.getTitleText(),
2417: JOptionPane.QUESTION_MESSAGE, null, null, "");
2418: StringBuffer reason = new StringBuffer();
2419: Object value = ic.validate(s, reason);
2420: if (value != null) {
2421: send("[t] g " + value);
2422: if (logger.isLoggable(Level.FINER)) {
2423: logger.finer("sending string " + value);
2424: }
2425: } else {
2426: this .display.addToStages("\n" + reason.toString(), "<p>"
2427: + reason.toString() + "</p>");
2428: display(true, false, false);
2429: }
2430: }
2431:
2432: /**
2433: * Handles the showing of the popup menu and the parse field
2434: * @param e the MouseEvent, that caused the call of this function
2435: */
2436: protected void maybeShowPopup(MouseEvent e) {
2437: //int i=outputVector.size()-1;
2438: // right click:
2439: if (e.isPopupTrigger()) {
2440: if (popUpLogger.isLoggable(Level.FINER)) {
2441: popUpLogger.finer("changing pop-up menu2!");
2442: }
2443: JPopupMenu popup2 = refinementMenu.producePopup();
2444: popup2.show(e.getComponent(), e.getX(), e.getY());
2445: }
2446: // middle click
2447: if (e.getButton() == MouseEvent.BUTTON2) {
2448: // selection Exists:
2449: if (popUpLogger.isLoggable(Level.FINER)) {
2450: popUpLogger.finer(e.getX() + " " + e.getY());
2451: }
2452: String selectedText;
2453:
2454: if (currentNode.isMeta()) {
2455: // we do not want the ?3 to be in parseField, that disturbs
2456: selectedText = "";
2457: } else {
2458: final String language;
2459: //put together the currently focused text
2460: if (e.getComponent() instanceof JTextComponent) {
2461: JTextComponent jtc = (JTextComponent) e
2462: .getComponent();
2463: int pos = jtc.viewToModel(e.getPoint());
2464: final boolean htmlClicked = (jtc instanceof JTextPane);
2465: language = linearization.getLanguageForPos(pos,
2466: htmlClicked);
2467: } else {
2468: language = "Abstract";
2469: }
2470: selectedText = linearization.getSelectedLinearization(
2471: language, focusPosition);
2472:
2473: }
2474: //compute the size of parseField
2475: if (selectedText.length() < 5)
2476: // if (treeCbMenuItem.isSelected())
2477: // parseField.setBounds(e.getX()+(int)Math.round(tree.getBounds().getWidth()), e.getY()+80, 400, 40);
2478: // else
2479: parseField.setBounds(e.getX(), e.getY() + 80, 400, 40);
2480: else
2481: // if (treeCbMenuItem.isSelected())
2482: // parseField.setBounds(e.getX()+(int)Math.round(tree.getBounds().getWidth()), e.getY()+80, selectedText.length()*20, 40);
2483: // else
2484: parseField.setBounds(e.getX(), e.getY() + 80,
2485: selectedText.length() * 20, 40);
2486: getLayeredPane().add(parseField, new Integer(1), 0);
2487: parseField.setText(selectedText);
2488: parseField.requestFocusInWindow();
2489: }
2490: }
2491:
2492: /**
2493: * Adds toHmsg to the [hmsg] part of command, if that is present.
2494: * If not, prepends toHmsg in square brackets to command
2495: * @param command The command for GF
2496: * @param toHmsg the text, that should occur inside [] before the command
2497: * @return the updated command (s.a.)
2498: */
2499: private static String addToHmsg(String command, String toHmsg) {
2500: command = command.trim();
2501: if (command.startsWith("[")) {
2502: command = "[" + toHmsg + command.substring(1);
2503: } else {
2504: command = "[" + toHmsg + "] " + command;
2505: }
2506: return command;
2507: }
2508:
2509: /**
2510: * pop-up menu (adapted from DynamicTree2):
2511: * @author janna
2512: */
2513: class PopupListener extends MouseAdapter {
2514: public void mousePressed(MouseEvent e) {
2515: // int selStart = tree.getRowForLocation(e.getX(), e.getY());
2516: // output.setSelectionRow(selStart);
2517: if (popUpLogger.isLoggable(Level.FINER)) {
2518: popUpLogger.finer("mouse pressed2: "
2519: + linearizationArea.getSelectionStart() + " "
2520: + linearizationArea.getSelectionEnd());
2521: }
2522: maybeShowPopup(e);
2523: }
2524:
2525: public void mouseReleased(MouseEvent e) {
2526: //nothing to be done here
2527: }
2528: }
2529:
2530: /**
2531: * Encapsulates the opening of terms or linearizations to a file.
2532: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2533: * @author daniels
2534: */
2535: class OpenAction extends AbstractAction {
2536: public OpenAction() {
2537: super ("Open Text", null);
2538: putValue(SHORT_DESCRIPTION,
2539: "Opens abstract syntax trees or linearizations for the current grammar");
2540: putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_O));
2541: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2542: KeyEvent.VK_O, ActionEvent.CTRL_MASK));
2543: }
2544:
2545: public void actionPerformed(ActionEvent e) {
2546: if (saveFc.getChoosableFileFilters().length < 2)
2547: saveFc.addChoosableFileFilter(new GrammarFilter());
2548: int returnVal = saveFc.showOpenDialog(GFEditor2.this );
2549: if (returnVal == JFileChooser.APPROVE_OPTION) {
2550: resetNewCategoryMenu();
2551: langMenuModel.resetLanguages();
2552:
2553: File file = saveFc.getSelectedFile();
2554: // opening the file for editing :
2555: if (logger.isLoggable(Level.FINER))
2556: logger.finer("opening: "
2557: + file.getPath().replace('\\',
2558: File.separatorChar));
2559: if (saveTypeGroup.getSelection().getActionCommand()
2560: .equals("term")) {
2561: if (logger.isLoggable(Level.FINER))
2562: logger.finer(" opening as a term ");
2563: send("[nt] open "
2564: + file.getPath().replace('\\',
2565: File.separatorChar));
2566: } else {
2567: if (logger.isLoggable(Level.FINER))
2568: logger.finer(" opening as a linearization ");
2569: send("[nt] openstring "
2570: + file.getPath().replace('\\',
2571: File.separatorChar));
2572: }
2573:
2574: fileString = "";
2575: grammar.setText("No Topic ");
2576: }
2577: }
2578: }
2579:
2580: /**
2581: * Encapsulates the saving of terms or linearizations to a file.
2582: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2583: * @author daniels
2584: */
2585: class SaveAction extends AbstractAction {
2586: public SaveAction() {
2587: super ("Save As", null);
2588: putValue(SHORT_DESCRIPTION,
2589: "Saves either the current linearizations or the AST");
2590: putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_S));
2591: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2592: KeyEvent.VK_S, ActionEvent.CTRL_MASK));
2593: }
2594:
2595: public void actionPerformed(ActionEvent e) {
2596: if (saveFc.getChoosableFileFilters().length < 2)
2597: saveFc.addChoosableFileFilter(new GrammarFilter());
2598: int returnVal = saveFc.showSaveDialog(GFEditor2.this );
2599: if (returnVal == JFileChooser.APPROVE_OPTION) {
2600: File file = saveFc.getSelectedFile();
2601: if (logger.isLoggable(Level.FINER))
2602: logger.finer("saving as " + file);
2603: final String abstractLin = linearization
2604: .getLinearizations().get("Abstract").toString();
2605:
2606: if (saveTypeGroup.getSelection().getActionCommand()
2607: .equals("term")) {
2608: // saving as a term
2609: writeOutput(removeMetavariableNumbers(abstractLin),
2610: file.getPath());
2611: } else {
2612: // saving as a linearization:
2613: /** collects the show linearizations */
2614: StringBuffer text = new StringBuffer();
2615: /** if sth. at all is shown already*/
2616: boolean sthAtAll = false;
2617: for (Iterator it = linearization
2618: .getLinearizations().keySet().iterator(); it
2619: .hasNext();) {
2620: Object key = it.next();
2621: if (!key.equals("Abstract")) {
2622: if (sthAtAll) {
2623: text.append("\n\n");
2624: }
2625: text.append(linearization
2626: .getLinearizations().get(key));
2627: sthAtAll = true;
2628: }
2629: }
2630: if (sthAtAll) {
2631: writeOutput(text.toString(), file.getPath());
2632: if (logger.isLoggable(Level.FINER))
2633: logger.finer(file + " saved.");
2634: } else {
2635: if (logger.isLoggable(Level.FINER))
2636: logger
2637: .warning("no concrete language shown, saving abstract");
2638: writeOutput(
2639: removeMetavariableNumbers(abstractLin),
2640: file.getPath());
2641: if (logger.isLoggable(Level.FINER))
2642: logger.finer(file + " saved.");
2643: }
2644: }
2645: }
2646:
2647: }
2648: }
2649:
2650: /**
2651: * Encapsulates adding new languages for the current abstract grammar.
2652: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2653: * @author daniels
2654: */
2655: class ImportAction extends AbstractAction {
2656: public ImportAction() {
2657: super ("Add", null);
2658: putValue(SHORT_DESCRIPTION,
2659: "add another concrete language for the current abstract grammar");
2660: putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_A));
2661: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2662: KeyEvent.VK_A, ActionEvent.CTRL_MASK));
2663: }
2664:
2665: public void actionPerformed(ActionEvent e) {
2666: //add another language (Add...)
2667: if (fc.getChoosableFileFilters().length < 2)
2668: fc.addChoosableFileFilter(new GrammarFilter());
2669: int returnVal = fc.showOpenDialog(GFEditor2.this );
2670: if (returnVal == JFileChooser.APPROVE_OPTION) {
2671: File file = fc.getSelectedFile();
2672:
2673: resetNewCategoryMenu();
2674: langMenuModel.resetLanguages();
2675: // importing a new language :
2676: if (logger.isLoggable(Level.FINER))
2677: logger.finer("importing: "
2678: + file.getPath().replace('\\', '/'));
2679: fileString = "";
2680: //TODO does that load paths in UNIX-notation under windows?
2681: send("i "
2682: + file.getPath().replace('\\',
2683: File.separatorChar), false, 1);
2684: processGfinit();
2685: processGfedit();
2686: }
2687: }
2688:
2689: }
2690:
2691: /**
2692: * Encapsulates starting over with a new grammar.
2693: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2694: * @author daniels
2695: */
2696: class NewTopicAction extends AbstractAction {
2697: public NewTopicAction() {
2698: super ("New Grammar", null);
2699: putValue(SHORT_DESCRIPTION,
2700: "dismiss current editing and load a new grammar");
2701: putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_N));
2702: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2703: KeyEvent.VK_N, ActionEvent.CTRL_MASK));
2704: }
2705:
2706: public void actionPerformed(ActionEvent e) {
2707: if (fc.getChoosableFileFilters().length < 2)
2708: fc.addChoosableFileFilter(new GrammarFilter());
2709: int returnVal = fc.showOpenDialog(GFEditor2.this );
2710: if (returnVal == JFileChooser.APPROVE_OPTION) {
2711: int n = JOptionPane
2712: .showConfirmDialog(
2713: GFEditor2.this ,
2714: "This will dismiss the previous editing. Would you like to continue?",
2715: "Starting a new topic",
2716: JOptionPane.YES_NO_OPTION);
2717: if (n == JOptionPane.YES_OPTION) {
2718: File file = fc.getSelectedFile();
2719: // importing a new grammar :
2720: newObject = false;
2721: statusLabel.setText(status);
2722: subtermDescLabel.setText("");
2723: subtermNameLabel.setText("");
2724: refinementMenu.reset();
2725: tree.resetTree();
2726: resetNewCategoryMenu();
2727: langMenuModel.resetLanguages();
2728: selectedMenuLanguage = "Abstract";
2729: rbMenuItemShort.setSelected(true);
2730: rbMenuItemUnTyped.setSelected(true);
2731: typedMenuItems = false;
2732:
2733: fileString = "";
2734: grammar.setText("No Topic ");
2735: display.resetLin();
2736: display(true, true, false);
2737: undoStack.clear();
2738: send(" e "
2739: + file.getPath().replace('\\',
2740: File.separatorChar), false, 1);
2741: processInit(null, false);
2742: processGfedit();
2743: resetPrintnames(true);
2744: }
2745: }
2746: }
2747:
2748: }
2749:
2750: /**
2751: * Encapsulates starting over without loading new grammars
2752: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2753: * @author daniels
2754: */
2755: class ResetAction extends AbstractAction {
2756: public ResetAction() {
2757: super ("Reset", null);
2758: putValue(SHORT_DESCRIPTION,
2759: "discard everything including the loaded grammars");
2760: putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_R));
2761: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2762: KeyEvent.VK_R, ActionEvent.CTRL_MASK));
2763: }
2764:
2765: public void actionPerformed(ActionEvent e) {
2766: newObject = false;
2767: statusLabel.setText(status);
2768: subtermDescLabel.setText("");
2769: subtermNameLabel.setText("");
2770: refinementMenu.reset();
2771: tree.resetTree();
2772: langMenuModel.resetLanguages();
2773: resetNewCategoryMenu();
2774: selectedMenuLanguage = "Abstract";
2775:
2776: rbMenuItemShort.setSelected(true);
2777: rbMenuItemUnTyped.setSelected(true);
2778: typedMenuItems = false;
2779:
2780: fileString = "";
2781: grammar.setText("No Topic ");
2782: undoStack.clear();
2783: send("e", false, 1);
2784: processGfinit();
2785: }
2786:
2787: }
2788:
2789: /**
2790: * Encapsulates exiting the program
2791: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2792: * @author daniels
2793: */
2794: class QuitAction extends AbstractAction {
2795: public QuitAction() {
2796: super ("Quit", null);
2797: putValue(SHORT_DESCRIPTION, "exit the editor");
2798: putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_Q));
2799: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2800: KeyEvent.VK_Q, ActionEvent.CTRL_MASK));
2801: }
2802:
2803: public void actionPerformed(ActionEvent e) {
2804: endProgram();
2805: }
2806:
2807: }
2808:
2809: /**
2810: * Encapsulates the random command for GF
2811: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2812: * @author daniels
2813: */
2814: class RandomAction extends AbstractAction {
2815: public RandomAction() {
2816: super ("Random", null);
2817: putValue(SHORT_DESCRIPTION,
2818: "build a random AST from the current cursor position");
2819: //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_M));
2820: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2821: KeyEvent.VK_M, ActionEvent.CTRL_MASK));
2822: }
2823:
2824: public void actionPerformed(ActionEvent e) {
2825: send("[t] a");
2826: }
2827:
2828: }
2829:
2830: /**
2831: * Encapsulates the undo command for GF
2832: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2833: * @author daniels
2834: */
2835: class UndoAction extends AbstractAction {
2836: public UndoAction() {
2837: super ("Undo", null);
2838: putValue(SHORT_DESCRIPTION, "undo the last command");
2839: //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_U));
2840: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2841: KeyEvent.VK_U, ActionEvent.CTRL_MASK));
2842: }
2843:
2844: public void actionPerformed(ActionEvent e) {
2845: int undoSteps = 1;
2846: if (!undoStack.empty()) {
2847: undoSteps = ((Integer) undoStack.pop()).intValue();
2848: }
2849: send("[t] u " + undoSteps, true, 0);
2850: }
2851: }
2852:
2853: /**
2854: * Encapsulates alpha command for GF
2855: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2856: * @author daniels
2857: */
2858: class AlphaAction extends AbstractAction {
2859: public AlphaAction() {
2860: super ("Alpha", null);
2861: putValue(SHORT_DESCRIPTION,
2862: "Performing alpha-conversion, rename bound variables");
2863: //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_P));
2864: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2865: KeyEvent.VK_P, ActionEvent.CTRL_MASK));
2866: }
2867:
2868: public void actionPerformed(ActionEvent e) {
2869: String s = JOptionPane.showInputDialog("Type string:",
2870: alphaInput);
2871: if (s != null) {
2872: alphaInput = s;
2873: send("[t] x " + s);
2874: }
2875: }
2876:
2877: }
2878:
2879: /**
2880: * Encapsulates the input dialog and sending of arbitrary commands to GF
2881: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2882: * @author daniels
2883: */
2884: class GfCommandAction extends AbstractAction {
2885: public GfCommandAction() {
2886: super ("GF command", null);
2887: putValue(SHORT_DESCRIPTION, "send a command to GF");
2888: //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_G));
2889: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2890: KeyEvent.VK_G, ActionEvent.CTRL_MASK));
2891: }
2892:
2893: public void actionPerformed(ActionEvent e) {
2894: String s = JOptionPane.showInputDialog("Command:",
2895: commandInput);
2896: if (s != null) {
2897: commandInput = s;
2898: s = addToHmsg(s, "t");
2899: if (logger.isLoggable(Level.FINER))
2900: logger.finer("sending: " + s);
2901: send(s);
2902: }
2903: }
2904: }
2905:
2906: /**
2907: * Encapsulates the showing of the read dialog
2908: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2909: * @author daniels
2910: */
2911: class ReadAction extends AbstractAction {
2912: public ReadAction() {
2913: super ("Read", null);
2914: putValue(SHORT_DESCRIPTION,
2915: "Refining with term or linearization from typed string or file");
2916: //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_E));
2917: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2918: KeyEvent.VK_E, ActionEvent.CTRL_MASK));
2919: }
2920:
2921: public void actionPerformed(ActionEvent e) {
2922: readDialog.show();
2923: }
2924:
2925: }
2926:
2927: /**
2928: * Encapsulates the splitting of the main window
2929: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2930: * @author daniels
2931: */
2932: class SplitAction extends AbstractAction {
2933: public SplitAction() {
2934: super ("Split Windows", null);
2935: putValue(SHORT_DESCRIPTION,
2936: "Splits the refinement menu into its own window");
2937: putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_L));
2938: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2939: KeyEvent.VK_L, ActionEvent.CTRL_MASK));
2940: }
2941:
2942: public void actionPerformed(ActionEvent e) {
2943: coverPanel.remove(centerPanel);
2944: centerPanel2.add(middlePanelUp, BorderLayout.SOUTH);
2945: if (((JCheckBoxMenuItem) viewMenu.getItem(0)).isSelected()) {
2946: centerPanel2.add(treePanel, BorderLayout.CENTER);
2947: } else {
2948: centerPanel2.add(outputPanelUp, BorderLayout.CENTER);
2949: }
2950: coverPanel.add(centerPanel2, BorderLayout.CENTER);
2951: gui2.getContentPane().add(
2952: refinementMenu.getRefinementListsContainer());
2953: gui2.setVisible(true);
2954: pack();
2955: repaint();
2956: }
2957:
2958: }
2959:
2960: /**
2961: * Encapsulates the combining of the main window
2962: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2963: * @author daniels
2964: */
2965: class CombineAction extends AbstractAction {
2966: public CombineAction() {
2967: super ("One Window", null);
2968: putValue(SHORT_DESCRIPTION,
2969: "Refinement menu and linearization areas in one window");
2970: putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_W));
2971: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
2972: KeyEvent.VK_W, ActionEvent.CTRL_MASK));
2973: }
2974:
2975: public void actionPerformed(ActionEvent e) {
2976: coverPanel.remove(centerPanel2);
2977: middlePanel.add(middlePanelUp, BorderLayout.NORTH);
2978: if (((JCheckBoxMenuItem) viewMenu.getItem(0)).isSelected()) {
2979: gui2.setVisible(false);
2980: centerPanel.setLeftComponent(treePanel);
2981: } else {
2982: centerPanel.setLeftComponent(outputPanelUp);
2983: gui2.setVisible(false);
2984: }
2985: coverPanel.add(centerPanel, BorderLayout.CENTER);
2986: centerPanelDown
2987: .add(refinementMenu.getRefinementListsContainer(),
2988: BorderLayout.CENTER);
2989: //centerPanelDown.add(refinementMenu.refinementSubcatPanel, BorderLayout.EAST);
2990: pack();
2991: repaint();
2992: }
2993:
2994: }
2995:
2996: /**
2997: * Starts a run on the AST to hunt down open subtyping witnesses
2998: * Is not local in initializeGUI because jswat cannot have active breakpoints in such a class, whyever.
2999: * @author daniels
3000: */
3001: class SubtypeAction extends AbstractAction {
3002: public SubtypeAction() {
3003: super ("Close Subtypes", null);
3004: putValue(SHORT_DESCRIPTION,
3005: "try to automatically refine Subtype relations");
3006: //putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_U));
3007: putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(
3008: KeyEvent.VK_T, ActionEvent.CTRL_MASK));
3009: }
3010:
3011: public void actionPerformed(ActionEvent e) {
3012: String resetCommand;
3013: int usteps;
3014: if (focusPosition != null) {
3015: //go back to where we come from
3016: resetCommand = "[t] mp " + focusPosition.position;
3017: usteps = 1;
3018: } else {
3019: resetCommand = "[t] gf";
3020: usteps = 0;
3021: }
3022: SubtypingProber sp = new SubtypingProber(gfCapsule);
3023: int undos = sp.checkSubtyping();
3024: send(resetCommand, true, undos + usteps);
3025: }
3026: }
3027:
3028: /**
3029: * Takes care, which classes are present and which states they have.
3030: * @author daniels
3031: */
3032: class LangMenuModel implements LanguageManager {
3033: Logger menuLogger = Logger
3034: .getLogger("de.uka.ilkd.key.ocl.gf.GFEditor2.MenuModel");
3035:
3036: /**
3037: * Just a mutable tuple of language name and whether this language
3038: * is displayed or not.
3039: */
3040: class LangActiveTuple {
3041: String lang;
3042: boolean active;
3043:
3044: public LangActiveTuple(String lang, boolean active) {
3045: this .lang = lang;
3046: this .active = active;
3047: }
3048:
3049: public String toString() {
3050: return lang + " : " + active;
3051: }
3052: }
3053:
3054: private Vector languages = new Vector();
3055: /** the group containing RadioButtons for the language the menus
3056: * should have
3057: */
3058: private ButtonGroup languageGroup = new ButtonGroup();
3059:
3060: void updateMenus() {
3061: for (Iterator it = this .languages.iterator(); it.hasNext();) {
3062: LangActiveTuple lat = (LangActiveTuple) it.next();
3063: boolean alreadyPresent = false;
3064: // language already in the list of available languages?
3065: for (int i = 0; i < langMenu.getItemCount() - 2; i++)
3066: if ((langMenu.getItem(i) != null)
3067: && langMenu.getItem(i).getText().equals(
3068: lat.lang)) {
3069: alreadyPresent = true;
3070: break;
3071: }
3072: if (!alreadyPresent) {
3073: //add item to the language list:
3074: JCheckBoxMenuItem cbMenuItem = new JCheckBoxMenuItem(
3075: lat.lang);
3076: if (menuLogger.isLoggable(Level.FINER))
3077: menuLogger.finer("menu item: " + lat.lang);
3078: cbMenuItem.setSelected(lat.active);
3079: cbMenuItem.setActionCommand("lang");
3080: cbMenuItem
3081: .addActionListener(this .langDisplayListener);
3082: langMenu.insert(cbMenuItem,
3083: langMenu.getItemCount() - 2);
3084:
3085: JRadioButtonMenuItem rbMenuItem = new JRadioButtonMenuItem(
3086: lat.lang);
3087: rbMenuItem.setActionCommand(lat.lang);
3088: rbMenuItem
3089: .addActionListener(this .menuLanguageListener);
3090: languageGroup.add(rbMenuItem);
3091: if (lat.lang.equals(selectedMenuLanguage)) {
3092: if (menuLogger.isLoggable(Level.FINER)) {
3093: menuLogger.finer("Selecting "
3094: + selectedMenuLanguage);
3095: }
3096: rbMenuItem.setSelected(true);
3097: }
3098: mlMenu.add(rbMenuItem);
3099:
3100: }
3101: }
3102: //stolen from fontEverywhere
3103: setSubmenuFont(langMenu, font, false);
3104: setSubmenuFont(mlMenu, font, false);
3105: }
3106:
3107: /**
3108: * Sets language myLang to myActive.
3109: * Does nothing, if myLang is not already there.
3110: * @param myLang The name of the language
3111: * @param myActive whether the language is displayed or not
3112: */
3113: void setActive(String myLang, boolean myActive) {
3114: boolean alreadyThere = false;
3115: for (Iterator it = this .languages.iterator(); it.hasNext();) {
3116: LangActiveTuple current = (LangActiveTuple) it.next();
3117: if (current.lang.equals(myLang)) {
3118: current.active = myActive;
3119: alreadyThere = true;
3120: }
3121: }
3122: if (!alreadyThere) {
3123: menuLogger.warning(myLang + " not yet known");
3124: }
3125: }
3126:
3127: /**
3128: * Checks if myLang is already present, and if not,
3129: * adds it. In that case, myActive is ignored.
3130: * @param myLang The name of the language
3131: * @param myActive whether the language is displayed or not
3132: */
3133: public void add(String myLang, boolean myActive) {
3134: boolean alreadyThere = false;
3135: for (Iterator it = this .languages.iterator(); it.hasNext();) {
3136: LangActiveTuple current = (LangActiveTuple) it.next();
3137: if (current.lang.equals(myLang)) {
3138: alreadyThere = true;
3139: }
3140: }
3141: if (!alreadyThere) {
3142: if (menuLogger.isLoggable(Level.FINER)) {
3143: menuLogger.finer(myLang + " added");
3144: }
3145: LangActiveTuple lat = new LangActiveTuple(myLang,
3146: myActive);
3147: this .languages.add(lat);
3148: }
3149: updateMenus();
3150: }
3151:
3152: /**
3153: * @param myLang The language in question
3154: * @return true iff the language is present and set to active,
3155: * false otherwise.
3156: */
3157: public boolean isLangActive(String myLang) {
3158: for (Iterator it = this .languages.iterator(); it.hasNext();) {
3159: LangActiveTuple current = (LangActiveTuple) it.next();
3160: if (current.lang.equals(myLang)) {
3161: return current.active;
3162: }
3163: }
3164: return false;
3165: }
3166:
3167: /**
3168: * initializes a virgin languages menu
3169: */
3170: public LangMenuModel() {
3171: resetLanguages();
3172: }
3173:
3174: /**
3175: * Resets the Languages menu so that it only contains a seperator and the Add button.
3176: * Resets the shown menu languages.
3177: * Resets the CheckBoxes that display the available languages.
3178: */
3179: void resetLanguages() {
3180: langMenu.removeAll();
3181: langMenu.addSeparator();
3182: JMenuItem fileMenuItem = new JMenuItem(new ImportAction());
3183: langMenu.add(fileMenuItem);
3184:
3185: mlMenu.removeAll();
3186: this .languageGroup = new ButtonGroup();
3187: this .languages = new Vector();
3188: updateMenus();
3189: }
3190:
3191: /**
3192: * Listens to the language menu RadioButtons and sends the
3193: * menu language changing commands suiting to the respective
3194: * button to GF.
3195: * Operates on selectedMenuLanguage from GFEditor2.
3196: */
3197: private ActionListener menuLanguageListener = new ActionListener() {
3198: public void actionPerformed(ActionEvent e) {
3199: final String action = e.getActionCommand();
3200: // must be a menu language
3201: selectedMenuLanguage = action;
3202: final String sendLang;
3203: if (action.equals("Abstract")) {
3204: sendLang = "Abs";
3205: } else {
3206: sendLang = action;
3207: }
3208: send("ml " + sendLang);
3209: resetPrintnames(true);
3210:
3211: return;
3212: }
3213: };
3214:
3215: /**
3216: * listens to the CheckBoxes in the Language menu and switches the
3217: * correspondend languages on or off when the user clicks on them
3218: */
3219: private ActionListener langDisplayListener = new ActionListener() {
3220: public void actionPerformed(ActionEvent e) {
3221: if (newObject) {
3222: //clear display of text and HTML
3223: display.resetLin();
3224: display(true, false, true);
3225: formLin();
3226: }
3227: final String lang = ((JCheckBoxMenuItem) e.getSource())
3228: .getText();
3229: if (((JCheckBoxMenuItem) e.getSource()).isSelected()) {
3230: if (menuLogger.isLoggable(Level.FINER)) {
3231: menuLogger.finer("turning on language '" + lang
3232: + "'");
3233: }
3234: setActive(lang, true);
3235: send("on " + lang);
3236: } else {
3237: if (menuLogger.isLoggable(Level.FINER)) {
3238: menuLogger.finer("turning off language '"
3239: + lang + "'");
3240: }
3241: setActive(lang, false);
3242: send("off " + lang);
3243: }
3244: return;
3245: }
3246: };
3247: }
3248: }
|