explicit jEdit actions -- to enable key mappings, for example;
authorwenzelm
Sat Sep 10 14:48:06 2011 +0200 (2011-09-10)
changeset 44864e50557cb0eb6
parent 44863 49ea566cb3b4
child 44865 679f0d57e831
explicit jEdit actions -- to enable key mappings, for example;
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/actions.xml	Sat Sep 10 14:28:07 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/actions.xml	Sat Sep 10 14:48:06 2011 +0200
     1.3 @@ -57,5 +57,14 @@
     1.4  	    isabelle.jedit.Isabelle.input_bold(textArea);
     1.5  	  </CODE>
     1.6  	</ACTION>
     1.7 -
     1.8 +	<ACTION NAME="isabelle.check-buffer">
     1.9 +	  <CODE>
    1.10 +	    isabelle.jedit.Isabelle.check_buffer(buffer);
    1.11 +	  </CODE>
    1.12 +	</ACTION>
    1.13 +	<ACTION NAME="isabelle.cancel-execution">
    1.14 +	  <CODE>
    1.15 +	    isabelle.jedit.Isabelle.cancel_execution();
    1.16 +	  </CODE>
    1.17 +	</ACTION>
    1.18  </ACTIONS>
    1.19 \ No newline at end of file
     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Sep 10 14:28:07 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Sep 10 14:48:06 2011 +0200
     2.3 @@ -343,6 +343,16 @@
     2.4    def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded)
     2.5    def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded)
     2.6    def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded)
     2.7 +
     2.8 +  def check_buffer(buffer: Buffer)
     2.9 +  {
    2.10 +    document_model(buffer) match {
    2.11 +      case None =>
    2.12 +      case Some(model) => model.full_perspective()
    2.13 +    }
    2.14 +  }
    2.15 +
    2.16 +  def cancel_execution() { session.cancel_execution() }
    2.17  }
    2.18  
    2.19  
     3.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 14:28:07 2011 +0200
     3.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 10 14:48:06 2011 +0200
     3.3 @@ -62,19 +62,12 @@
     3.4    session_phase.tooltip = "Prover status"
     3.5  
     3.6    private val cancel = new Button("Cancel") {
     3.7 -    reactions += { case ButtonClicked(_) => Isabelle.session.cancel_execution }
     3.8 +    reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
     3.9    }
    3.10    cancel.tooltip = "Cancel current proof checking process"
    3.11  
    3.12    private val check = new Button("Check") {
    3.13 -    reactions +=
    3.14 -    {
    3.15 -      case ButtonClicked(_) =>
    3.16 -        Isabelle.document_model(view.getBuffer) match {
    3.17 -          case None =>
    3.18 -          case Some(model) => model.full_perspective()
    3.19 -        }
    3.20 -    }
    3.21 +    reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
    3.22    }
    3.23    check.tooltip = "Commence full proof checking of current buffer"
    3.24