src/Tools/jEdit/src/isabelle_actions.scala
author wenzelm
Sun Nov 25 17:15:21 2012 +0100 (2012-11-25 ago)
changeset 50198 0c7b351a6871
parent 50187 b5a09812abc4
child 50205 788c8263e634
permissions -rw-r--r--
added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
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@50198
    22
    val FONT_SIZE = "view.fontsize"
wenzelm@50198
    23
    val size = change(jEdit.getIntegerProperty(FONT_SIZE, 12)) max 5
wenzelm@50198
    24
    jEdit.setIntegerProperty(FONT_SIZE, size)
wenzelm@50198
    25
    jEdit.propertiesChanged()
wenzelm@50198
    26
    jEdit.saveSettings()
wenzelm@50198
    27
    view.getStatus.setMessageAndClear("Text font size: " + size)
wenzelm@50198
    28
  }
wenzelm@50198
    29
wenzelm@50198
    30
  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
wenzelm@50198
    31
  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
wenzelm@50198
    32
wenzelm@50198
    33
wenzelm@50183
    34
  /* full checking */
wenzelm@50183
    35
wenzelm@50183
    36
  def check_buffer(buffer: Buffer)
wenzelm@50183
    37
  {
wenzelm@50183
    38
    Isabelle.document_model(buffer) match {
wenzelm@50183
    39
      case None =>
wenzelm@50183
    40
      case Some(model) => model.full_perspective()
wenzelm@50183
    41
    }
wenzelm@50183
    42
  }
wenzelm@50183
    43
wenzelm@50187
    44
  def cancel_execution() { Isabelle.session.cancel_execution() }
wenzelm@50183
    45
wenzelm@50183
    46
wenzelm@50183
    47
  /* control styles */
wenzelm@50183
    48
wenzelm@50183
    49
  def control_sub(text_area: JEditTextArea)
wenzelm@50187
    50
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
    51
wenzelm@50183
    52
  def control_sup(text_area: JEditTextArea)
wenzelm@50187
    53
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
    54
wenzelm@50183
    55
  def control_isub(text_area: JEditTextArea)
wenzelm@50187
    56
  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
wenzelm@50183
    57
wenzelm@50183
    58
  def control_isup(text_area: JEditTextArea)
wenzelm@50187
    59
  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
wenzelm@50183
    60
wenzelm@50183
    61
  def control_bold(text_area: JEditTextArea)
wenzelm@50187
    62
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
    63
wenzelm@50183
    64
  def control_reset(text_area: JEditTextArea)
wenzelm@50187
    65
  { Token_Markup.edit_control_style(text_area, "") }
wenzelm@50183
    66
wenzelm@50183
    67
wenzelm@50183
    68
  /* block styles */
wenzelm@50183
    69
wenzelm@50183
    70
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
    71
  {
wenzelm@50183
    72
    s1.foreach(text_area.userInput(_))
wenzelm@50183
    73
    s2.foreach(text_area.userInput(_))
wenzelm@50183
    74
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
    75
  }
wenzelm@50183
    76
wenzelm@50183
    77
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
    78
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
    79
wenzelm@50183
    80
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
    81
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@50183
    82
}
wenzelm@50183
    83