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;
     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 size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    23     jEdit.setIntegerProperty("view.fontsize", size)
    24     jEdit.propertiesChanged()
    25     jEdit.saveSettings()
    26     view.getStatus.setMessageAndClear("Text font size: " + size)
    27   }
    28 
    29   def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    30   def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    31 
    32 
    33   /* full checking */
    34 
    35   def check_buffer(buffer: Buffer)
    36   {
    37     PIDE.document_model(buffer) match {
    38       case None =>
    39       case Some(model) => model.full_perspective()
    40     }
    41   }
    42 
    43   def cancel_execution() { PIDE.session.cancel_execution() }
    44 
    45 
    46   /* control styles */
    47 
    48   def control_sub(text_area: JEditTextArea)
    49   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    50 
    51   def control_sup(text_area: JEditTextArea)
    52   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    53 
    54   def control_isub(text_area: JEditTextArea)
    55   { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    56 
    57   def control_isup(text_area: JEditTextArea)
    58   { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
    59 
    60   def control_bold(text_area: JEditTextArea)
    61   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    62 
    63   def control_reset(text_area: JEditTextArea)
    64   { Token_Markup.edit_control_style(text_area, "") }
    65 
    66 
    67   /* block styles */
    68 
    69   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
    70   {
    71     s1.foreach(text_area.userInput(_))
    72     s2.foreach(text_area.userInput(_))
    73     s2.foreach(_ => text_area.goToPrevCharacter(false))
    74   }
    75 
    76   def input_bsub(text_area: JEditTextArea)
    77   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
    78 
    79   def input_bsup(text_area: JEditTextArea)
    80   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
    81 }
    82