src/Tools/jEdit/src/isabelle_actions.scala
author wenzelm
Sat Nov 24 16:40:42 2012 +0100 (2012-11-24)
changeset 50187 b5a09812abc4
parent 50183 2b3e24e1c9e7
child 50198 0c7b351a6871
permissions -rw-r--r--
special handling of control symbols in Symbols dockable;
less obscure Scala names;
     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.Buffer
    13 import org.gjt.sp.jedit.textarea.JEditTextArea
    14 
    15 
    16 object Isabelle_Actions
    17 {
    18   /* full checking */
    19 
    20   def check_buffer(buffer: Buffer)
    21   {
    22     Isabelle.document_model(buffer) match {
    23       case None =>
    24       case Some(model) => model.full_perspective()
    25     }
    26   }
    27 
    28   def cancel_execution() { Isabelle.session.cancel_execution() }
    29 
    30 
    31   /* control styles */
    32 
    33   def control_sub(text_area: JEditTextArea)
    34   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    35 
    36   def control_sup(text_area: JEditTextArea)
    37   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    38 
    39   def control_isub(text_area: JEditTextArea)
    40   { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    41 
    42   def control_isup(text_area: JEditTextArea)
    43   { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
    44 
    45   def control_bold(text_area: JEditTextArea)
    46   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    47 
    48   def control_reset(text_area: JEditTextArea)
    49   { Token_Markup.edit_control_style(text_area, "") }
    50 
    51 
    52   /* block styles */
    53 
    54   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
    55   {
    56     s1.foreach(text_area.userInput(_))
    57     s2.foreach(text_area.userInput(_))
    58     s2.foreach(_ => text_area.goToPrevCharacter(false))
    59   }
    60 
    61   def input_bsub(text_area: JEditTextArea)
    62   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
    63 
    64   def input_bsup(text_area: JEditTextArea)
    65   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
    66 }
    67