src/Tools/jEdit/src/isabelle.scala
author wenzelm
Sun Nov 25 21:35:29 2012 +0100 (2012-11-25)
changeset 50208 1382ad6d4774
parent 50206 src/Tools/jEdit/src/isabelle_actions.scala@6626bc5ed053
child 50209 907373a080b9
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/isabelle.scala
     2     Author:     Makarius
     3 
     4 Convenience operations 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 import org.gjt.sp.jedit.gui.DockableWindowManager
    15 
    16 
    17 object Isabelle
    18 {
    19   /* dockable windows */
    20 
    21   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    22 
    23   def docked_session(view: View): Option[Session_Dockable] =
    24     wm(view).getDockableWindow("isabelle-session") match {
    25       case dockable: Session_Dockable => Some(dockable)
    26       case _ => None
    27     }
    28 
    29   def docked_output(view: View): Option[Output_Dockable] =
    30     wm(view).getDockableWindow("isabelle-output") match {
    31       case dockable: Output_Dockable => Some(dockable)
    32       case _ => None
    33     }
    34 
    35   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
    36     wm(view).getDockableWindow("isabelle-raw-output") match {
    37       case dockable: Raw_Output_Dockable => Some(dockable)
    38       case _ => None
    39     }
    40 
    41   def docked_protocol(view: View): Option[Protocol_Dockable] =
    42     wm(view).getDockableWindow("isabelle-protocol") match {
    43       case dockable: Protocol_Dockable => Some(dockable)
    44       case _ => None
    45     }
    46 
    47 
    48   /* font size */
    49 
    50   def change_font_size(view: View, change: Int => Int)
    51   {
    52     val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
    53     jEdit.setIntegerProperty("view.fontsize", size)
    54     jEdit.propertiesChanged()
    55     jEdit.saveSettings()
    56     view.getStatus.setMessageAndClear("Text font size: " + size)
    57   }
    58 
    59   def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    60   def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    61 
    62 
    63   /* full checking */
    64 
    65   def check_buffer(buffer: Buffer)
    66   {
    67     PIDE.document_model(buffer) match {
    68       case None =>
    69       case Some(model) => model.full_perspective()
    70     }
    71   }
    72 
    73   def cancel_execution() { PIDE.session.cancel_execution() }
    74 
    75 
    76   /* control styles */
    77 
    78   def control_sub(text_area: JEditTextArea)
    79   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    80 
    81   def control_sup(text_area: JEditTextArea)
    82   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    83 
    84   def control_isub(text_area: JEditTextArea)
    85   { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
    86 
    87   def control_isup(text_area: JEditTextArea)
    88   { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
    89 
    90   def control_bold(text_area: JEditTextArea)
    91   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
    92 
    93   def control_reset(text_area: JEditTextArea)
    94   { Token_Markup.edit_control_style(text_area, "") }
    95 
    96 
    97   /* block styles */
    98 
    99   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   100   {
   101     s1.foreach(text_area.userInput(_))
   102     s2.foreach(text_area.userInput(_))
   103     s2.foreach(_ => text_area.goToPrevCharacter(false))
   104   }
   105 
   106   def input_bsub(text_area: JEditTextArea)
   107   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   108 
   109   def input_bsup(text_area: JEditTextArea)
   110   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   111 }
   112