tuned signature;
authorwenzelm
Sun Nov 25 21:35:29 2012 +0100 (2012-11-25)
changeset 502081382ad6d4774
parent 50207 54be125d8cdc
child 50209 907373a080b9
tuned signature;
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/actions.xml
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/isabelle_actions.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Sun Nov 25 21:23:20 2012 +0100
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Sun Nov 25 21:35:29 2012 +0100
     1.3 @@ -15,7 +15,7 @@
     1.4    "src/html_panel.scala"
     1.5    "src/hyperlink.scala"
     1.6    "src/info_dockable.scala"
     1.7 -  "src/isabelle_actions.scala"
     1.8 +  "src/isabelle.scala"
     1.9    "src/isabelle_encoding.scala"
    1.10    "src/isabelle_logic.scala"
    1.11    "src/isabelle_options.scala"
     2.1 --- a/src/Tools/jEdit/src/actions.xml	Sun Nov 25 21:23:20 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/actions.xml	Sun Nov 25 21:35:29 2012 +0100
     2.3 @@ -44,62 +44,62 @@
     2.4  	</ACTION>
     2.5  	<ACTION NAME="isabelle.increase-font-size">
     2.6  	  <CODE>
     2.7 -	    isabelle.jedit.Isabelle_Actions.increase_font_size(view);
     2.8 +	    isabelle.jedit.Isabelle.increase_font_size(view);
     2.9  	  </CODE>
    2.10  	</ACTION>
    2.11  	<ACTION NAME="isabelle.decrease-font-size">
    2.12  	  <CODE>
    2.13 -	    isabelle.jedit.Isabelle_Actions.decrease_font_size(view);
    2.14 +	    isabelle.jedit.Isabelle.decrease_font_size(view);
    2.15  	  </CODE>
    2.16  	</ACTION>
    2.17  	<ACTION NAME="isabelle.check-buffer">
    2.18  	  <CODE>
    2.19 -	    isabelle.jedit.Isabelle_Actions.check_buffer(buffer);
    2.20 +	    isabelle.jedit.Isabelle.check_buffer(buffer);
    2.21  	  </CODE>
    2.22  	</ACTION>
    2.23  	<ACTION NAME="isabelle.cancel-execution">
    2.24  	  <CODE>
    2.25 -	    isabelle.jedit.Isabelle_Actions.cancel_execution();
    2.26 +	    isabelle.jedit.Isabelle.cancel_execution();
    2.27  	  </CODE>
    2.28  	</ACTION>
    2.29  	<ACTION NAME="isabelle.control-sub">
    2.30  	  <CODE>
    2.31 -	    isabelle.jedit.Isabelle_Actions.control_sub(textArea);
    2.32 +	    isabelle.jedit.Isabelle.control_sub(textArea);
    2.33  	  </CODE>
    2.34  	</ACTION>
    2.35  	<ACTION NAME="isabelle.control-sup">
    2.36  	  <CODE>
    2.37 -	    isabelle.jedit.Isabelle_Actions.control_sup(textArea);
    2.38 +	    isabelle.jedit.Isabelle.control_sup(textArea);
    2.39  	  </CODE>
    2.40  	</ACTION>
    2.41  	<ACTION NAME="isabelle.control-isub">
    2.42  	  <CODE>
    2.43 -	    isabelle.jedit.Isabelle_Actions.control_isub(textArea);
    2.44 +	    isabelle.jedit.Isabelle.control_isub(textArea);
    2.45  	  </CODE>
    2.46  	</ACTION>
    2.47  	<ACTION NAME="isabelle.control-isup">
    2.48  	  <CODE>
    2.49 -	    isabelle.jedit.Isabelle_Actions.control_isup(textArea);
    2.50 +	    isabelle.jedit.Isabelle.control_isup(textArea);
    2.51  	  </CODE>
    2.52  	</ACTION>
    2.53  	<ACTION NAME="isabelle.control-bold">
    2.54  	  <CODE>
    2.55 -	    isabelle.jedit.Isabelle_Actions.control_bold(textArea);
    2.56 +	    isabelle.jedit.Isabelle.control_bold(textArea);
    2.57  	  </CODE>
    2.58  	</ACTION>
    2.59  	<ACTION NAME="isabelle.control-reset">
    2.60  	  <CODE>
    2.61 -	    isabelle.jedit.Isabelle_Actions.control_reset(textArea);
    2.62 +	    isabelle.jedit.Isabelle.control_reset(textArea);
    2.63  	  </CODE>
    2.64  	</ACTION>
    2.65  	<ACTION NAME="isabelle.input-bsub">
    2.66  	  <CODE>
    2.67 -	    isabelle.jedit.Isabelle_Actions.input_bsub(textArea);
    2.68 +	    isabelle.jedit.Isabelle.input_bsub(textArea);
    2.69  	  </CODE>
    2.70  	</ACTION>
    2.71  	<ACTION NAME="isabelle.input-bsup">
    2.72  	  <CODE>
    2.73 -	    isabelle.jedit.Isabelle_Actions.input_bsup(textArea);
    2.74 +	    isabelle.jedit.Isabelle.input_bsup(textArea);
    2.75  	  </CODE>
    2.76  	</ACTION>
    2.77  </ACTIONS>
    2.78 \ No newline at end of file
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Sun Nov 25 21:35:29 2012 +0100
     3.3 @@ -0,0 +1,112 @@
     3.4 +/*  Title:      Tools/jEdit/src/isabelle.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Convenience operations for Isabelle/jEdit.
     3.8 +*/
     3.9 +
    3.10 +package isabelle.jedit
    3.11 +
    3.12 +
    3.13 +import isabelle._
    3.14 +
    3.15 +import org.gjt.sp.jedit.{jEdit, View, Buffer}
    3.16 +import org.gjt.sp.jedit.textarea.JEditTextArea
    3.17 +import org.gjt.sp.jedit.gui.DockableWindowManager
    3.18 +
    3.19 +
    3.20 +object Isabelle
    3.21 +{
    3.22 +  /* dockable windows */
    3.23 +
    3.24 +  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    3.25 +
    3.26 +  def docked_session(view: View): Option[Session_Dockable] =
    3.27 +    wm(view).getDockableWindow("isabelle-session") match {
    3.28 +      case dockable: Session_Dockable => Some(dockable)
    3.29 +      case _ => None
    3.30 +    }
    3.31 +
    3.32 +  def docked_output(view: View): Option[Output_Dockable] =
    3.33 +    wm(view).getDockableWindow("isabelle-output") match {
    3.34 +      case dockable: Output_Dockable => Some(dockable)
    3.35 +      case _ => None
    3.36 +    }
    3.37 +
    3.38 +  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
    3.39 +    wm(view).getDockableWindow("isabelle-raw-output") match {
    3.40 +      case dockable: Raw_Output_Dockable => Some(dockable)
    3.41 +      case _ => None
    3.42 +    }
    3.43 +
    3.44 +  def docked_protocol(view: View): Option[Protocol_Dockable] =
    3.45 +    wm(view).getDockableWindow("isabelle-protocol") match {
    3.46 +      case dockable: Protocol_Dockable => Some(dockable)
    3.47 +      case _ => None
    3.48 +    }
    3.49 +
    3.50 +
    3.51 +  /* font size */
    3.52 +
    3.53 +  def change_font_size(view: View, change: Int => Int)
    3.54 +  {
    3.55 +    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    3.56 +    jEdit.setIntegerProperty("view.fontsize", size)
    3.57 +    jEdit.propertiesChanged()
    3.58 +    jEdit.saveSettings()
    3.59 +    view.getStatus.setMessageAndClear("Text font size: " + size)
    3.60 +  }
    3.61 +
    3.62 +  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    3.63 +  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    3.64 +
    3.65 +
    3.66 +  /* full checking */
    3.67 +
    3.68 +  def check_buffer(buffer: Buffer)
    3.69 +  {
    3.70 +    PIDE.document_model(buffer) match {
    3.71 +      case None =>
    3.72 +      case Some(model) => model.full_perspective()
    3.73 +    }
    3.74 +  }
    3.75 +
    3.76 +  def cancel_execution() { PIDE.session.cancel_execution() }
    3.77 +
    3.78 +
    3.79 +  /* control styles */
    3.80 +
    3.81 +  def control_sub(text_area: JEditTextArea)
    3.82 +  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    3.83 +
    3.84 +  def control_sup(text_area: JEditTextArea)
    3.85 +  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    3.86 +
    3.87 +  def control_isub(text_area: JEditTextArea)
    3.88 +  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    3.89 +
    3.90 +  def control_isup(text_area: JEditTextArea)
    3.91 +  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
    3.92 +
    3.93 +  def control_bold(text_area: JEditTextArea)
    3.94 +  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    3.95 +
    3.96 +  def control_reset(text_area: JEditTextArea)
    3.97 +  { Token_Markup.edit_control_style(text_area, "") }
    3.98 +
    3.99 +
   3.100 +  /* block styles */
   3.101 +
   3.102 +  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   3.103 +  {
   3.104 +    s1.foreach(text_area.userInput(_))
   3.105 +    s2.foreach(text_area.userInput(_))
   3.106 +    s2.foreach(_ => text_area.goToPrevCharacter(false))
   3.107 +  }
   3.108 +
   3.109 +  def input_bsub(text_area: JEditTextArea)
   3.110 +  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   3.111 +
   3.112 +  def input_bsup(text_area: JEditTextArea)
   3.113 +  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   3.114 +}
   3.115 +
     4.1 --- a/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 21:23:20 2012 +0100
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,82 +0,0 @@
     4.4 -/*  Title:      Tools/jEdit/src/plugin.scala
     4.5 -    Author:     Makarius
     4.6 -
     4.7 -Convenience actions for Isabelle/jEdit.
     4.8 -*/
     4.9 -
    4.10 -package isabelle.jedit
    4.11 -
    4.12 -
    4.13 -import isabelle._
    4.14 -
    4.15 -import org.gjt.sp.jedit.{jEdit, View, Buffer}
    4.16 -import org.gjt.sp.jedit.textarea.JEditTextArea
    4.17 -
    4.18 -
    4.19 -object Isabelle_Actions
    4.20 -{
    4.21 -  /* font size */
    4.22 -
    4.23 -  def change_font_size(view: View, change: Int => Int)
    4.24 -  {
    4.25 -    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    4.26 -    jEdit.setIntegerProperty("view.fontsize", size)
    4.27 -    jEdit.propertiesChanged()
    4.28 -    jEdit.saveSettings()
    4.29 -    view.getStatus.setMessageAndClear("Text font size: " + size)
    4.30 -  }
    4.31 -
    4.32 -  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    4.33 -  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    4.34 -
    4.35 -
    4.36 -  /* full checking */
    4.37 -
    4.38 -  def check_buffer(buffer: Buffer)
    4.39 -  {
    4.40 -    PIDE.document_model(buffer) match {
    4.41 -      case None =>
    4.42 -      case Some(model) => model.full_perspective()
    4.43 -    }
    4.44 -  }
    4.45 -
    4.46 -  def cancel_execution() { PIDE.session.cancel_execution() }
    4.47 -
    4.48 -
    4.49 -  /* control styles */
    4.50 -
    4.51 -  def control_sub(text_area: JEditTextArea)
    4.52 -  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    4.53 -
    4.54 -  def control_sup(text_area: JEditTextArea)
    4.55 -  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    4.56 -
    4.57 -  def control_isub(text_area: JEditTextArea)
    4.58 -  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    4.59 -
    4.60 -  def control_isup(text_area: JEditTextArea)
    4.61 -  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
    4.62 -
    4.63 -  def control_bold(text_area: JEditTextArea)
    4.64 -  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    4.65 -
    4.66 -  def control_reset(text_area: JEditTextArea)
    4.67 -  { Token_Markup.edit_control_style(text_area, "") }
    4.68 -
    4.69 -
    4.70 -  /* block styles */
    4.71 -
    4.72 -  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
    4.73 -  {
    4.74 -    s1.foreach(text_area.userInput(_))
    4.75 -    s2.foreach(text_area.userInput(_))
    4.76 -    s2.foreach(_ => text_area.goToPrevCharacter(false))
    4.77 -  }
    4.78 -
    4.79 -  def input_bsub(text_area: JEditTextArea)
    4.80 -  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
    4.81 -
    4.82 -  def input_bsup(text_area: JEditTextArea)
    4.83 -  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
    4.84 -}
    4.85 -
     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 21:23:20 2012 +0100
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sun Nov 25 21:35:29 2012 +0100
     5.3 @@ -17,7 +17,6 @@
     5.4  import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     5.5  import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
     5.6  import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
     5.7 -import org.gjt.sp.jedit.gui.DockableWindowManager
     5.8  
     5.9  import org.gjt.sp.util.SyntaxUtilities
    5.10  
    5.11 @@ -104,35 +103,6 @@
    5.12        Document_View.exit(text_area)
    5.13      }
    5.14    }
    5.15 -
    5.16 -
    5.17 -  /* dockable windows */
    5.18 -
    5.19 -  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    5.20 -
    5.21 -  def docked_session(view: View): Option[Session_Dockable] =
    5.22 -    wm(view).getDockableWindow("isabelle-session") match {
    5.23 -      case dockable: Session_Dockable => Some(dockable)
    5.24 -      case _ => None
    5.25 -    }
    5.26 -
    5.27 -  def docked_output(view: View): Option[Output_Dockable] =
    5.28 -    wm(view).getDockableWindow("isabelle-output") match {
    5.29 -      case dockable: Output_Dockable => Some(dockable)
    5.30 -      case _ => None
    5.31 -    }
    5.32 -
    5.33 -  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
    5.34 -    wm(view).getDockableWindow("isabelle-raw-output") match {
    5.35 -      case dockable: Raw_Output_Dockable => Some(dockable)
    5.36 -      case _ => None
    5.37 -    }
    5.38 -
    5.39 -  def docked_protocol(view: View): Option[Protocol_Dockable] =
    5.40 -    wm(view).getDockableWindow("isabelle-protocol") match {
    5.41 -      case dockable: Protocol_Dockable => Some(dockable)
    5.42 -      case _ => None
    5.43 -    }
    5.44  }
    5.45  
    5.46  
     6.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Sun Nov 25 21:23:20 2012 +0100
     6.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Nov 25 21:35:29 2012 +0100
     6.3 @@ -51,12 +51,12 @@
     6.4    }
     6.5  
     6.6    private val cancel = new Button("Cancel") {
     6.7 -    reactions += { case ButtonClicked(_) => Isabelle_Actions.cancel_execution() }
     6.8 +    reactions += { case ButtonClicked(_) => Isabelle.cancel_execution() }
     6.9    }
    6.10    cancel.tooltip = jEdit.getProperty("isabelle.cancel-execution.label")
    6.11  
    6.12    private val check = new Button("Check") {
    6.13 -    reactions += { case ButtonClicked(_) => Isabelle_Actions.check_buffer(view.getBuffer) }
    6.14 +    reactions += { case ButtonClicked(_) => Isabelle.check_buffer(view.getBuffer) }
    6.15    }
    6.16    check.tooltip = jEdit.getProperty("isabelle.check-buffer.label")
    6.17