clones of increase-font-size / decrease-font-size to allow two further shortcuts for various keyboard layouts;

--- a/src/Tools/jEdit/src/actions.xml	Sun Jun 23 20:12:01 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Sun Jun 23 20:26:31 2013 +0200
@@ -62,11 +62,21 @@
 	    isabelle.jedit.Isabelle.increase_font_size(view);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.increase-font-size2">
+	  <CODE>
+	    isabelle.jedit.Isabelle.increase_font_size(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.decrease-font-size">
 	  <CODE>
 	    isabelle.jedit.Isabelle.decrease_font_size(view);
 	  </CODE>
 	</ACTION>
+	<ACTION NAME="isabelle.decrease-font-size2">
+	  <CODE>
+	    isabelle.jedit.Isabelle.decrease_font_size(view);
+	  </CODE>
+	</ACTION>
 	<ACTION NAME="isabelle.control-sub">
 	  <CODE>
 	    isabelle.jedit.Isabelle.control_sub(textArea);

--- a/src/Tools/jEdit/src/jEdit.props	Sun Jun 23 20:12:01 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Sun Jun 23 20:26:31 2013 +0200
@@ -199,9 +199,15 @@
 isabelle.decrease-font-size.label=Decrease font size
 isabelle.decrease-font-size.shortcut2=C+SUBTRACT
 isabelle.decrease-font-size.shortcut=C+MINUS
+isabelle.decrease-font-size2.label=Decrease font size (clone)
+#isabelle.decrease-font-size2.shortcut2=C+SUBTRACT
+#isabelle.decrease-font-size2.shortcut=C+MINUS
 isabelle.increase-font-size.label=Increase font size
 isabelle.increase-font-size.shortcut2=C+ADD
 isabelle.increase-font-size.shortcut=C+PLUS
+isabelle.increase-font-size2.label=Increase font size (clone)
+#isabelle.increase-font-size2.shortcut2=C+ADD
+isabelle.increase-font-size2.shortcut=C+EQUALS
 lang.usedefaultlocale=false
 largefilemode=full
 line-end.shortcut=END