src/Tools/jEdit/src/isabelle.scala
author wenzelm
Wed Jul 31 21:13:05 2013 +0200 (2013-07-31)
changeset 52816 c608e0ade554
parent 52815 eaad5fe7bb1b
child 52974 908e8a36e975
permissions -rw-r--r--
home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
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_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_timing(view: View): Option[Timing_Dockable] =
    30     wm(view).getDockableWindow("isabelle-timing") match {
    31       case dockable: Timing_Dockable => Some(dockable)
    32       case _ => None
    33     }
    34 
    35   def docked_output(view: View): Option[Output_Dockable] =
    36     wm(view).getDockableWindow("isabelle-output") match {
    37       case dockable: Output_Dockable => Some(dockable)
    38       case _ => None
    39     }
    40 
    41   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
    42     wm(view).getDockableWindow("isabelle-raw-output") match {
    43       case dockable: Raw_Output_Dockable => Some(dockable)
    44       case _ => None
    45     }
    46 
    47   def docked_protocol(view: View): Option[Protocol_Dockable] =
    48     wm(view).getDockableWindow("isabelle-protocol") match {
    49       case dockable: Protocol_Dockable => Some(dockable)
    50       case _ => None
    51     }
    52 
    53   def docked_monitor(view: View): Option[Monitor_Dockable] =
    54     wm(view).getDockableWindow("isabelle-monitor") match {
    55       case dockable: Monitor_Dockable => Some(dockable)
    56       case _ => None
    57     }
    58 
    59 
    60   /* continuous checking */
    61 
    62   private val CONTINUOUS_CHECKING = "editor_continuous_checking"
    63 
    64   def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
    65 
    66   def continuous_checking_=(b: Boolean)
    67   {
    68     Swing_Thread.require()
    69 
    70     if (continuous_checking != b) {
    71       PIDE.options.bool(CONTINUOUS_CHECKING) = b
    72       PIDE.options_changed()
    73       PIDE.flush_buffers()
    74     }
    75   }
    76 
    77   def set_continuous_checking() { continuous_checking = true }
    78   def reset_continuous_checking() { continuous_checking = false }
    79   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
    80 
    81 
    82   /* required document nodes */
    83 
    84   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
    85   {
    86     Swing_Thread.require()
    87     PIDE.document_model(view.getBuffer) match {
    88       case Some(model) =>
    89         model.node_required = (if (toggle) !model.node_required else set)
    90       case None =>
    91     }
    92   }
    93 
    94   def set_node_required(view: View) { node_required_update(view, set = true) }
    95   def reset_node_required(view: View) { node_required_update(view, set = false) }
    96   def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
    97 
    98 
    99   /* font size */
   100 
   101   def change_font_size(view: View, change: Int => Int)
   102   {
   103     val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
   104     jEdit.setIntegerProperty("view.fontsize", size)
   105     jEdit.propertiesChanged()
   106     jEdit.saveSettings()
   107     view.getStatus.setMessageAndClear("Text font size: " + size)
   108   }
   109 
   110   def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
   111   def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
   112 
   113 
   114   /* structured insert */
   115 
   116   def insert_line_padding(text_area: JEditTextArea, text: String)
   117   {
   118     val buffer = text_area.getBuffer
   119     JEdit_Lib.buffer_edit(buffer) {
   120       val text1 =
   121         if (text_area.getSelectionCount == 0) {
   122           def pad(range: Text.Range): String =
   123             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
   124 
   125           val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
   126           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
   127           pad(before_caret) + text + pad(caret)
   128         }
   129         else text
   130       text_area.setSelectedText(text1)
   131     }
   132   }
   133 
   134 
   135   /* control styles */
   136 
   137   def control_sub(text_area: JEditTextArea)
   138   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
   139 
   140   def control_sup(text_area: JEditTextArea)
   141   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
   142 
   143   def control_isub(text_area: JEditTextArea)
   144   { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
   145 
   146   def control_isup(text_area: JEditTextArea)
   147   { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
   148 
   149   def control_bold(text_area: JEditTextArea)
   150   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   151 
   152   def control_reset(text_area: JEditTextArea)
   153   { Token_Markup.edit_control_style(text_area, "") }
   154 
   155 
   156   /* block styles */
   157 
   158   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   159   {
   160     s1.foreach(text_area.userInput(_))
   161     s2.foreach(text_area.userInput(_))
   162     s2.foreach(_ => text_area.goToPrevCharacter(false))
   163   }
   164 
   165   def input_bsub(text_area: JEditTextArea)
   166   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   167 
   168   def input_bsup(text_area: JEditTextArea)
   169   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   170 }
   171