# HG changeset patch
# User wenzelm
# Date 1372011991 -7200
# Node ID fce1c133e1f8330e8679652494098df576e3ad45
# Parent  9d1cc9a22177cdb10d0e8a3cbe11c1f605044fc5
clones of increase-font-size / decrease-font-size to allow two further shortcuts for various keyboard layouts;

diff -r 9d1cc9a22177 -r fce1c133e1f8 src/Tools/jEdit/src/actions.xml
--- 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);
diff -r 9d1cc9a22177 -r fce1c133e1f8 src/Tools/jEdit/src/jEdit.props
--- 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