some keyboard shortcuts for important actions;
authorwenzelm
Sat, 10 Sep 2011 16:30:08 +0200
changeset 44865 679f0d57e831
parent 44864 e50557cb0eb6
child 44866 0eb8284a64bd
some keyboard shortcuts for important actions; proper label properties, which are also required for jEdit "Shortcuts" options panel;
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/session_dockable.scala
--- 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
--- 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)