src/Tools/jEdit/src/isabelle.scala
author wenzelm
Tue Jan 08 18:24:52 2013 +0100 (2013-01-08)
changeset 50775 8c1cda8ad833
parent 50433 9131dadb2bf7
child 51533 3f6280aedbcc
permissions -rw-r--r--
upper bound for font size;
     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_theories(view: View): Option[Theories_Dockable] =
    24     wm(view).getDockableWindow("isabelle-theories") match {
    25       case dockable: Theories_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   def docked_monitor(view: View): Option[Monitor_Dockable] =
    48     wm(view).getDockableWindow("isabelle-monitor") match {
    49       case dockable: Monitor_Dockable => Some(dockable)
    50       case _ => None
    51     }
    52 
    53 
    54   /* font size */
    55 
    56   def change_font_size(view: View, change: Int => Int)
    57   {
    58     val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
    59     jEdit.setIntegerProperty("view.fontsize", size)
    60     jEdit.propertiesChanged()
    61     jEdit.saveSettings()
    62     view.getStatus.setMessageAndClear("Text font size: " + size)
    63   }
    64 
    65   def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
    66   def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
    67 
    68 
    69   /* structured insert */
    70 
    71   def insert_line_padding(text_area: JEditTextArea, text: String)
    72   {
    73     val buffer = text_area.getBuffer
    74     JEdit_Lib.buffer_edit(buffer) {
    75       val text1 =
    76         if (text_area.getSelectionCount == 0) {
    77           def pad(range: Text.Range): String =
    78             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
    79 
    80           val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
    81           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
    82           pad(before_caret) + text + pad(caret)
    83         }
    84         else text
    85       text_area.setSelectedText(text1)
    86     }
    87   }
    88 
    89 
    90   /* control styles */
    91 
    92   def control_sub(text_area: JEditTextArea)
    93   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
    94 
    95   def control_sup(text_area: JEditTextArea)
    96   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
    97 
    98   def control_isub(text_area: JEditTextArea)
    99   { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
   100 
   101   def control_isup(text_area: JEditTextArea)
   102   { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
   103 
   104   def control_bold(text_area: JEditTextArea)
   105   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   106 
   107   def control_reset(text_area: JEditTextArea)
   108   { Token_Markup.edit_control_style(text_area, "") }
   109 
   110 
   111   /* block styles */
   112 
   113   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   114   {
   115     s1.foreach(text_area.userInput(_))
   116     s2.foreach(text_area.userInput(_))
   117     s2.foreach(_ => text_area.goToPrevCharacter(false))
   118   }
   119 
   120   def input_bsub(text_area: JEditTextArea)
   121   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   122 
   123   def input_bsup(text_area: JEditTextArea)
   124   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   125 }
   126