# HG changeset patch
# User wenzelm
# Date 1315665008 -7200
# Node ID 679f0d57e8313bf500e13a4b11db8f1e01338220
# Parent  e50557cb0eb6b84373ed01d4e35fd8a4cf8d107f
some keyboard shortcuts for important actions;
proper label properties, which are also required for jEdit "Shortcuts" options panel;

diff -r e50557cb0eb6 -r 679f0d57e831 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Sat Sep 10 14:48:06 2011 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props	Sat Sep 10 16:30:08 2011 +0200
@@ -38,8 +38,15 @@
 options.isabelle.auto-start=true
 
 #actions
+isabelle.check-buffer.label=Commence full proof checking of current buffer
+isabelle.check-buffer.shortcut=C+e SPACE
+isabelle.cancel-execution.label=Cancel current proof checking process
+isabelle.cancel-execution.shortcut=C+e BACK_SPACE
+isabelle.input-isub.label=Input subscript
 isabelle.input-isub.shortcut=C+e DOWN
+isabelle.input-isup.label=Input superscript
 isabelle.input-isup.shortcut=C+e UP
+isabelle.input-bold.label=Input bold face
 isabelle.input-bold.shortcut=C+e RIGHT
 
 #menu actions
diff -r e50557cb0eb6 -r 679f0d57e831 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 14:48:06 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 16:30:08 2011 +0200
@@ -19,7 +19,7 @@
 import javax.swing.JList
 import javax.swing.border.{BevelBorder, SoftBevelBorder}
 
-import org.gjt.sp.jedit.View
+import org.gjt.sp.jedit.{View, jEdit}
 
 
 class Session_Dockable(view: View, position: String) extends Dockable(view: View, position: String)
@@ -64,12 +64,12 @@
   private val cancel = new Button("Cancel") {
     reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
   }
-  cancel.tooltip = "Cancel current proof checking process"
+  cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
 
   private val check = new Button("Check") {
     reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
   }
-  check.tooltip = "Commence full proof checking of current buffer"
+  check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
 
   private val logic = Isabelle.logic_selector(Isabelle.Property("logic"))
   logic.listenTo(logic.selection)