# HG changeset patch
# User wenzelm
# Date 1315658886 -7200
# Node ID e50557cb0eb6b84373ed01d4e35fd8a4cf8d107f
# Parent  49ea566cb3b4587f9347857101e9ad7e83191b11
explicit jEdit actions -- to enable key mappings, for example;

diff -r 49ea566cb3b4 -r e50557cb0eb6 src/Tools/jEdit/src/actions.xml
--- a/src/Tools/jEdit/src/actions.xml	Sat Sep 10 14:28:07 2011 +0200
+++ b/src/Tools/jEdit/src/actions.xml	Sat Sep 10 14:48:06 2011 +0200
@@ -57,5 +57,14 @@
 	    isabelle.jedit.Isabelle.input_bold(textArea);
 	  </CODE>
 	</ACTION>
-
+	<ACTION NAME="isabelle.check-buffer">
+	  <CODE>
+	    isabelle.jedit.Isabelle.check_buffer(buffer);
+	  </CODE>
+	</ACTION>
+	<ACTION NAME="isabelle.cancel-execution">
+	  <CODE>
+	    isabelle.jedit.Isabelle.cancel_execution();
+	  </CODE>
+	</ACTION>
 </ACTIONS>
\ No newline at end of file
diff -r 49ea566cb3b4 -r e50557cb0eb6 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Sep 10 14:28:07 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Sep 10 14:48:06 2011 +0200
@@ -343,6 +343,16 @@
   def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
   def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
   def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
+
+  def check_buffer(buffer: Buffer)
+  {
+    document_model(buffer) match {
+      case None =>
+      case Some(model) => model.full_perspective()
+    }
+  }
+
+  def cancel_execution() { session.cancel_execution() }
 }
 
 
diff -r 49ea566cb3b4 -r e50557cb0eb6 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 14:28:07 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 14:48:06 2011 +0200
@@ -62,19 +62,12 @@
   session_phase.tooltip = "Prover status"
 
   private val cancel = new Button("Cancel") {
-    reactions += { case ButtonClicked(_) => Isabelle.session.cancel_execution }
+    reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
   }
   cancel.tooltip = "Cancel current proof checking process"
 
   private val check = new Button("Check") {
-    reactions +=
-    {
-      case ButtonClicked(_) =>
-        Isabelle.document_model(view.getBuffer) match {
-          case None =>
-          case Some(model) => model.full_perspective()
-        }
-    }
+    reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
   }
   check.tooltip = "Commence full proof checking of current buffer"