src/Tools/jEdit/src/isabelle.scala
author wenzelm
Thu Aug 29 12:38:33 2013 +0200 (2013-08-29)
changeset 53274 1760c01f1c78
parent 53272 0dfd78ff7696
child 53276 cbed0aa0b0db
permissions -rw-r--r--
maintain Completion_Popup.Text_Area as client property like Document_View;
global Completion_Popup.Text_Area init/exit like SideKickPlugin;
eliminated old SideKick completion -- cover all Isabelle modes uniformly;
dynamic lookup of Isabelle.mode_syntax -- NB: buffer mode might be undefined in intermediate stages;
     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   /* editor modes */
    20 
    21   val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news")
    22 
    23   def mode_syntax(name: String): Option[Outer_Syntax] =
    24     name match {
    25       case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax
    26       case "isabelle-options" => Some(Options.options_syntax)
    27       case "isabelle-root" => Some(Build.root_syntax)
    28       case "isabelle-news" => Some(Outer_Syntax.empty)
    29       case _ => None
    30     }
    31 
    32 
    33   /* dockable windows */
    34 
    35   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    36 
    37   def docked_theories(view: View): Option[Theories_Dockable] =
    38     wm(view).getDockableWindow("isabelle-theories") match {
    39       case dockable: Theories_Dockable => Some(dockable)
    40       case _ => None
    41     }
    42 
    43   def docked_timing(view: View): Option[Timing_Dockable] =
    44     wm(view).getDockableWindow("isabelle-timing") match {
    45       case dockable: Timing_Dockable => Some(dockable)
    46       case _ => None
    47     }
    48 
    49   def docked_output(view: View): Option[Output_Dockable] =
    50     wm(view).getDockableWindow("isabelle-output") match {
    51       case dockable: Output_Dockable => Some(dockable)
    52       case _ => None
    53     }
    54 
    55   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
    56     wm(view).getDockableWindow("isabelle-raw-output") match {
    57       case dockable: Raw_Output_Dockable => Some(dockable)
    58       case _ => None
    59     }
    60 
    61   def docked_protocol(view: View): Option[Protocol_Dockable] =
    62     wm(view).getDockableWindow("isabelle-protocol") match {
    63       case dockable: Protocol_Dockable => Some(dockable)
    64       case _ => None
    65     }
    66 
    67   def docked_monitor(view: View): Option[Monitor_Dockable] =
    68     wm(view).getDockableWindow("isabelle-monitor") match {
    69       case dockable: Monitor_Dockable => Some(dockable)
    70       case _ => None
    71     }
    72 
    73 
    74   /* continuous checking */
    75 
    76   private val CONTINUOUS_CHECKING = "editor_continuous_checking"
    77 
    78   def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
    79 
    80   def continuous_checking_=(b: Boolean)
    81   {
    82     Swing_Thread.require()
    83 
    84     if (continuous_checking != b) {
    85       PIDE.options.bool(CONTINUOUS_CHECKING) = b
    86       PIDE.options_changed()
    87       PIDE.editor.flush()
    88     }
    89   }
    90 
    91   def set_continuous_checking() { continuous_checking = true }
    92   def reset_continuous_checking() { continuous_checking = false }
    93   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
    94 
    95 
    96   /* required document nodes */
    97 
    98   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
    99   {
   100     Swing_Thread.require()
   101     PIDE.document_model(view.getBuffer) match {
   102       case Some(model) =>
   103         model.node_required = (if (toggle) !model.node_required else set)
   104       case None =>
   105     }
   106   }
   107 
   108   def set_node_required(view: View) { node_required_update(view, set = true) }
   109   def reset_node_required(view: View) { node_required_update(view, set = false) }
   110   def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
   111 
   112 
   113   /* font size */
   114 
   115   def reset_font_size(view: View): Unit =
   116     Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
   117 
   118   def increase_font_size(view: View): Unit =
   119     Rendering.font_size_change(view, i => i + ((i / 10) max 1))
   120 
   121   def decrease_font_size(view: View): Unit =
   122     Rendering.font_size_change(view, i => i - ((i / 10) max 1))
   123 
   124 
   125   /* structured insert */
   126 
   127   def insert_line_padding(text_area: JEditTextArea, text: String)
   128   {
   129     val buffer = text_area.getBuffer
   130     JEdit_Lib.buffer_edit(buffer) {
   131       val text1 =
   132         if (text_area.getSelectionCount == 0) {
   133           def pad(range: Text.Range): String =
   134             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
   135 
   136           val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
   137           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
   138           pad(before_caret) + text + pad(caret)
   139         }
   140         else text
   141       text_area.setSelectedText(text1)
   142     }
   143   }
   144 
   145 
   146   /* control styles */
   147 
   148   def control_sub(text_area: JEditTextArea)
   149   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
   150 
   151   def control_sup(text_area: JEditTextArea)
   152   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
   153 
   154   def control_bold(text_area: JEditTextArea)
   155   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   156 
   157   def control_reset(text_area: JEditTextArea)
   158   { Token_Markup.edit_control_style(text_area, "") }
   159 
   160 
   161   /* block styles */
   162 
   163   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   164   {
   165     s1.foreach(text_area.userInput(_))
   166     s2.foreach(text_area.userInput(_))
   167     s2.foreach(_ => text_area.goToPrevCharacter(false))
   168   }
   169 
   170   def input_bsub(text_area: JEditTextArea)
   171   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   172 
   173   def input_bsup(text_area: JEditTextArea)
   174   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   175 }
   176