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