src/Tools/jEdit/src/isabelle_actions.scala
changeset 50208 1382ad6d4774
parent 50207 54be125d8cdc
child 50209 907373a080b9
     1.1 --- a/src/Tools/jEdit/src/isabelle_actions.scala	Sun Nov 25 21:23:20 2012 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,82 +0,0 @@
     1.4 -/*  Title:      Tools/jEdit/src/plugin.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Convenience actions for Isabelle/jEdit.
     1.8 -*/
     1.9 -
    1.10 -package isabelle.jedit
    1.11 -
    1.12 -
    1.13 -import isabelle._
    1.14 -
    1.15 -import org.gjt.sp.jedit.{jEdit, View, Buffer}
    1.16 -import org.gjt.sp.jedit.textarea.JEditTextArea
    1.17 -
    1.18 -
    1.19 -object Isabelle_Actions
    1.20 -{
    1.21 -  /* font size */
    1.22 -
    1.23 -  def change_font_size(view: View, change: Int => Int)
    1.24 -  {
    1.25 -    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    1.26 -    jEdit.setIntegerProperty("view.fontsize", size)
    1.27 -    jEdit.propertiesChanged()
    1.28 -    jEdit.saveSettings()
    1.29 -    view.getStatus.setMessageAndClear("Text font size: " + size)
    1.30 -  }
    1.31 -
    1.32 -  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    1.33 -  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    1.34 -
    1.35 -
    1.36 -  /* full checking */
    1.37 -
    1.38 -  def check_buffer(buffer: Buffer)
    1.39 -  {
    1.40 -    PIDE.document_model(buffer) match {
    1.41 -      case None =>
    1.42 -      case Some(model) => model.full_perspective()
    1.43 -    }
    1.44 -  }
    1.45 -
    1.46 -  def cancel_execution() { PIDE.session.cancel_execution() }
    1.47 -
    1.48 -
    1.49 -  /* control styles */
    1.50 -
    1.51 -  def control_sub(text_area: JEditTextArea)
    1.52 -  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    1.53 -
    1.54 -  def control_sup(text_area: JEditTextArea)
    1.55 -  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    1.56 -
    1.57 -  def control_isub(text_area: JEditTextArea)
    1.58 -  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    1.59 -
    1.60 -  def control_isup(text_area: JEditTextArea)
    1.61 -  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
    1.62 -
    1.63 -  def control_bold(text_area: JEditTextArea)
    1.64 -  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    1.65 -
    1.66 -  def control_reset(text_area: JEditTextArea)
    1.67 -  { Token_Markup.edit_control_style(text_area, "") }
    1.68 -
    1.69 -
    1.70 -  /* block styles */
    1.71 -
    1.72 -  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
    1.73 -  {
    1.74 -    s1.foreach(text_area.userInput(_))
    1.75 -    s2.foreach(text_area.userInput(_))
    1.76 -    s2.foreach(_ => text_area.goToPrevCharacter(false))
    1.77 -  }
    1.78 -
    1.79 -  def input_bsub(text_area: JEditTextArea)
    1.80 -  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
    1.81 -
    1.82 -  def input_bsup(text_area: JEditTextArea)
    1.83 -  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
    1.84 -}
    1.85 -