updated key bindings to execution range;
authorwenzelm
Mon, 29 Jul 2013 20:34:53 +0200
changeset 52777 fa71ab256f70
parent 52776 fd81d51460b7
child 52778 19fa3e3964f0
updated key bindings to execution range;
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/actions.xml	Mon Jul 29 19:55:38 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Mon Jul 29 20:34:53 2013 +0200
@@ -52,14 +52,14 @@
 			wm.addDockableWindow("isabelle-symbols");
 		</CODE>
 	</ACTION>
-	<ACTION NAME="isabelle.check-buffer">
+	<ACTION NAME="isabelle.execution-range-none">
 	  <CODE>
-	    isabelle.jedit.PIDE.check_buffer(buffer);
+	    isabelle.jedit.PIDE.execution_range_none();
 	  </CODE>
 	</ACTION>
-	<ACTION NAME="isabelle.cancel-execution">
+	<ACTION NAME="isabelle.execution-range-visible">
 	  <CODE>
-	    isabelle.jedit.PIDE.cancel_execution();
+	    isabelle.jedit.PIDE.execution_range_visible();
 	  </CODE>
 	</ACTION>
 	<ACTION NAME="isabelle.increase-font-size">
--- a/src/Tools/jEdit/src/jEdit.props	Mon Jul 29 19:55:38 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Jul 29 20:34:53 2013 +0200
@@ -185,10 +185,10 @@
 isabelle-readme.dock-position=bottom
 isabelle-symbols.dock-position=bottom
 isabelle-theories.dock-position=right
-isabelle.cancel-execution.label=Cancel execution
-isabelle.cancel-execution.shortcut=C+e BACK_SPACE
-isabelle.check-buffer.label=Commence full checking
-isabelle.check-buffer.shortcut=C+e SPACE
+isabelle.execution-range-none.label=Check nothing
+isabelle.execution-range-none.shortcut=C+e BACK_SPACE
+isabelle.execution-range-visible=Check visible parts of theories
+isabelle.execution-range-visible.shortcut=C+e SPACE
 isabelle.control-bold.label=Control bold
 isabelle.control-bold.shortcut=C+e RIGHT
 isabelle.control-isub.label=Control subscript
--- a/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 19:55:38 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Jul 29 20:34:53 2013 +0200
@@ -154,6 +154,9 @@
       )
     }
   }
+
+  def execution_range_none(): Unit = update_execution_range(Execution_Range.NONE)
+  def execution_range_visible(): Unit = update_execution_range(Execution_Range.VISIBLE)
 }