From c9b5a36e03b6ca60bd905ca10e308da78fac3a25 Mon Sep 17 00:00:00 2001
From: hdaniels <unknown>
Date: Thu, 23 Jun 2005 10:18:36 +0000
Subject: [PATCH] changed 'Open' into 'Open Text' and 'New Topic' into 'New
 Grammar'

---
 src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java
index 52e6d8d49..634f2c08b 100644
--- a/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java
+++ b/src/JavaGUI2/de/uka/ilkd/key/ocl/gf/GFEditor2.java
@@ -3444,8 +3444,8 @@ KeyListener, FocusListener {
          */
         class OpenAction extends AbstractAction {
                 public OpenAction() {
-                        super("Open", null);
-                        putValue(SHORT_DESCRIPTION, "Opens abstract syntax trees or linearizations");
+                        super("Open Text", null);
+                        putValue(SHORT_DESCRIPTION, "Opens abstract syntax trees or linearizations for the current grammar");
                         putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_O));
                         putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_O, ActionEvent.CTRL_MASK));
                 }
@@ -3586,10 +3586,10 @@ KeyListener, FocusListener {
          */
         class NewTopicAction extends AbstractAction {
                 public NewTopicAction() {
-                        super("New Topic", null);
+                        super("New Grammar", null);
                         putValue(SHORT_DESCRIPTION, "dismiss current editing and load a new grammar");
-                        putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_T));
-                        putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_T, ActionEvent.CTRL_MASK));
+                        putValue(MNEMONIC_KEY, new Integer(KeyEvent.VK_N));
+                        putValue(ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_N, ActionEvent.CTRL_MASK));
                 }
                 
                 public void actionPerformed(ActionEvent e) {