tuned signature;
authorwenzelm
Sun Nov 25 21:40:34 2012 +0100 (2012-11-25)
changeset 50209907373a080b9
parent 50208 1382ad6d4774
child 50210 747db833fbf7
child 50218 d50119e69453
tuned signature;
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Tools/jEdit/src/Isabelle.props	Sun Nov 25 21:35:29 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/Isabelle.props	Sun Nov 25 21:40:34 2012 +0100
     1.3 @@ -27,14 +27,14 @@
     1.4  options.isabelle-rendering.code=new isabelle.jedit.Isabelle_Options2();
     1.5  
     1.6  #actions
     1.7 +isabelle.check-buffer.label=Commence full proof checking of current buffer
     1.8 +isabelle.check-buffer.shortcut=C+e SPACE
     1.9 +isabelle.cancel-execution.label=Cancel current proof checking process
    1.10 +isabelle.cancel-execution.shortcut=C+e BACK_SPACE
    1.11  isabelle.increase-font-size.label=Increase font size
    1.12  isabelle.increase-font-size.shortcut=C+PLUS
    1.13  isabelle.decrease-font-size.label=Decrease font size
    1.14  isabelle.decrease-font-size.shortcut=C+MINUS
    1.15 -isabelle.check-buffer.label=Commence full proof checking of current buffer
    1.16 -isabelle.check-buffer.shortcut=C+e SPACE
    1.17 -isabelle.cancel-execution.label=Cancel current proof checking process
    1.18 -isabelle.cancel-execution.shortcut=C+e BACK_SPACE
    1.19  isabelle.control-isub.label=Control subscript
    1.20  isabelle.control-isub.shortcut=C+e DOWN
    1.21  isabelle.control-isup.label=Control superscript
     2.1 --- a/src/Tools/jEdit/src/actions.xml	Sun Nov 25 21:35:29 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/actions.xml	Sun Nov 25 21:40:34 2012 +0100
     2.3 @@ -42,6 +42,16 @@
     2.4  			wm.addDockableWindow("isabelle-symbols");
     2.5  		</CODE>
     2.6  	</ACTION>
     2.7 +	<ACTION NAME="isabelle.check-buffer">
     2.8 +	  <CODE>
     2.9 +	    isabelle.jedit.PIDE.check_buffer(buffer);
    2.10 +	  </CODE>
    2.11 +	</ACTION>
    2.12 +	<ACTION NAME="isabelle.cancel-execution">
    2.13 +	  <CODE>
    2.14 +	    isabelle.jedit.PIDE.cancel_execution();
    2.15 +	  </CODE>
    2.16 +	</ACTION>
    2.17  	<ACTION NAME="isabelle.increase-font-size">
    2.18  	  <CODE>
    2.19  	    isabelle.jedit.Isabelle.increase_font_size(view);
    2.20 @@ -52,16 +62,6 @@
    2.21  	    isabelle.jedit.Isabelle.decrease_font_size(view);
    2.22  	  </CODE>
    2.23  	</ACTION>
    2.24 -	<ACTION NAME="isabelle.check-buffer">
    2.25 -	  <CODE>
    2.26 -	    isabelle.jedit.Isabelle.check_buffer(buffer);
    2.27 -	  </CODE>
    2.28 -	</ACTION>
    2.29 -	<ACTION NAME="isabelle.cancel-execution">
    2.30 -	  <CODE>
    2.31 -	    isabelle.jedit.Isabelle.cancel_execution();
    2.32 -	  </CODE>
    2.33 -	</ACTION>
    2.34  	<ACTION NAME="isabelle.control-sub">
    2.35  	  <CODE>
    2.36  	    isabelle.jedit.Isabelle.control_sub(textArea);
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Sun Nov 25 21:35:29 2012 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sun Nov 25 21:40:34 2012 +0100
     3.3 @@ -60,19 +60,6 @@
     3.4    def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
     3.5  
     3.6  
     3.7 -  /* full checking */
     3.8 -
     3.9 -  def check_buffer(buffer: Buffer)
    3.10 -  {
    3.11 -    PIDE.document_model(buffer) match {
    3.12 -      case None =>
    3.13 -      case Some(model) => model.full_perspective()
    3.14 -    }
    3.15 -  }
    3.16 -
    3.17 -  def cancel_execution() { PIDE.session.cancel_execution() }
    3.18 -
    3.19 -
    3.20    /* control styles */
    3.21  
    3.22    def control_sub(text_area: JEditTextArea)
     4.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 21:35:29 2012 +0100
     4.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 21:40:34 2012 +0100
     4.3 @@ -103,6 +103,19 @@
     4.4        Document_View.exit(text_area)
     4.5      }
     4.6    }
     4.7 +
     4.8 +
     4.9 +  /* full checking */
    4.10 +
    4.11 +  def check_buffer(buffer: Buffer)
    4.12 +  {
    4.13 +    PIDE.document_model(buffer) match {
    4.14 +      case None =>
    4.15 +      case Some(model) => model.full_perspective()
    4.16 +    }
    4.17 +  }
    4.18 +
    4.19 +  def cancel_execution() { PIDE.session.cancel_execution() }
    4.20  }
    4.21  
    4.22  
     5.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Nov 25 21:35:29 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Nov 25 21:40:34 2012 +0100
     5.3 @@ -51,12 +51,12 @@
     5.4    }
     5.5  
     5.6    private val cancel = new Button("Cancel") {
     5.7 -    reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
     5.8 +    reactions += { case ButtonClicked(_) => PIDE.cancel_execution() }
     5.9    }
    5.10    cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
    5.11  
    5.12    private val check = new Button("Check") {
    5.13 -    reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
    5.14 +    reactions += { case ButtonClicked(_) => PIDE.check_buffer(view.getBuffer) }
    5.15    }
    5.16    check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
    5.17