src/Tools/jEdit/src/isabelle_actions.scala
author wenzelm
Sun Nov 25 21:10:29 2012 +0100 (2012-11-25)
changeset 50206 6626bc5ed053
parent 50205 788c8263e634
permissions -rw-r--r--
tuned signature;
uniform view.fontsize fallback;
wenzelm@50183
     1
/*  Title:      Tools/jEdit/src/plugin.scala
wenzelm@50183
     2
    Author:     Makarius
wenzelm@50183
     3
wenzelm@50183
     4
Convenience actions for Isabelle/jEdit.
wenzelm@50183
     5
*/
wenzelm@50183
     6
wenzelm@50183
     7
package isabelle.jedit
wenzelm@50183
     8
wenzelm@50183
     9
wenzelm@50183
    10
import isabelle._
wenzelm@50183
    11
wenzelm@50198
    12
import org.gjt.sp.jedit.{jEdit, View, Buffer}
wenzelm@50183
    13
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@50183
    14
wenzelm@50183
    15
wenzelm@50183
    16
object Isabelle_Actions
wenzelm@50183
    17
{
wenzelm@50198
    18
  /* font size */
wenzelm@50198
    19
wenzelm@50198
    20
  def change_font_size(view: View, change: Int => Int)
wenzelm@50198
    21
  {
wenzelm@50206
    22
    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
wenzelm@50206
    23
    jEdit.setIntegerProperty("view.fontsize", size)
wenzelm@50198
    24
    jEdit.propertiesChanged()
wenzelm@50198
    25
    jEdit.saveSettings()
wenzelm@50198
    26
    view.getStatus.setMessageAndClear("Text font size: " + size)
wenzelm@50198
    27
  }
wenzelm@50198
    28
wenzelm@50198
    29
  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
wenzelm@50198
    30
  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
wenzelm@50198
    31
wenzelm@50198
    32
wenzelm@50183
    33
  /* full checking */
wenzelm@50183
    34
wenzelm@50183
    35
  def check_buffer(buffer: Buffer)
wenzelm@50183
    36
  {
wenzelm@50205
    37
    PIDE.document_model(buffer) match {
wenzelm@50183
    38
      case None =>
wenzelm@50183
    39
      case Some(model) => model.full_perspective()
wenzelm@50183
    40
    }
wenzelm@50183
    41
  }
wenzelm@50183
    42
wenzelm@50205
    43
  def cancel_execution() { PIDE.session.cancel_execution() }
wenzelm@50183
    44
wenzelm@50183
    45
wenzelm@50183
    46
  /* control styles */
wenzelm@50183
    47
wenzelm@50183
    48
  def control_sub(text_area: JEditTextArea)
wenzelm@50187
    49
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
    50
wenzelm@50183
    51
  def control_sup(text_area: JEditTextArea)
wenzelm@50187
    52
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
    53
wenzelm@50183
    54
  def control_isub(text_area: JEditTextArea)
wenzelm@50187
    55
  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
wenzelm@50183
    56
wenzelm@50183
    57
  def control_isup(text_area: JEditTextArea)
wenzelm@50187
    58
  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
wenzelm@50183
    59
wenzelm@50183
    60
  def control_bold(text_area: JEditTextArea)
wenzelm@50187
    61
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
    62
wenzelm@50183
    63
  def control_reset(text_area: JEditTextArea)
wenzelm@50187
    64
  { Token_Markup.edit_control_style(text_area, "") }
wenzelm@50183
    65
wenzelm@50183
    66
wenzelm@50183
    67
  /* block styles */
wenzelm@50183
    68
wenzelm@50183
    69
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
    70
  {
wenzelm@50183
    71
    s1.foreach(text_area.userInput(_))
wenzelm@50183
    72
    s2.foreach(text_area.userInput(_))
wenzelm@50183
    73
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
    74
  }
wenzelm@50183
    75
wenzelm@50183
    76
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
    77
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
    78
wenzelm@50183
    79
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
    80
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@50183
    81
}
wenzelm@50183
    82