src/Tools/jEdit/src/isabelle.scala
author wenzelm
Thu Aug 29 21:49:46 2013 +0200 (2013-08-29)
changeset 53293 fd27b8f5a479
parent 53281 251e1a2aa792
child 53322 a4cd032172e0
permissions -rw-r--r--
added action isabelle.complete, using standard jEdit keyboard shortcut;
     1 /*  Title:      Tools/jEdit/src/isabelle.scala
     2     Author:     Makarius
     3 
     4 Global configuration and 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, CompleteWord}
    15 
    16 
    17 object Isabelle
    18 {
    19   /* editor modes */
    20 
    21   val modes =
    22     List(
    23       "isabelle",         // theory source
    24       "isabelle-markup",  // SideKick markup tree
    25       "isabelle-news",    // NEWS
    26       "isabelle-options", // etc/options
    27       "isabelle-output",  // pretty text area output
    28       "isabelle-root")    // session ROOT
    29 
    30   private lazy val news_syntax = Outer_Syntax.init().no_tokens
    31 
    32   def mode_syntax(name: String): Option[Outer_Syntax] =
    33     name match {
    34       case "isabelle" | "isabelle-markup" =>
    35         val syntax = PIDE.session.recent_syntax
    36         if (syntax == Outer_Syntax.empty) None else Some(syntax)
    37       case "isabelle-options" => Some(Options.options_syntax)
    38       case "isabelle-root" => Some(Build.root_syntax)
    39       case "isabelle-news" => Some(news_syntax)
    40       case "isabelle-output" => None
    41       case _ => None
    42     }
    43 
    44 
    45   /* token markers */
    46 
    47   private val markers =
    48     Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
    49 
    50   def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
    51 
    52 
    53   /* dockable windows */
    54 
    55   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    56 
    57   def docked_theories(view: View): Option[Theories_Dockable] =
    58     wm(view).getDockableWindow("isabelle-theories") match {
    59       case dockable: Theories_Dockable => Some(dockable)
    60       case _ => None
    61     }
    62 
    63   def docked_timing(view: View): Option[Timing_Dockable] =
    64     wm(view).getDockableWindow("isabelle-timing") match {
    65       case dockable: Timing_Dockable => Some(dockable)
    66       case _ => None
    67     }
    68 
    69   def docked_output(view: View): Option[Output_Dockable] =
    70     wm(view).getDockableWindow("isabelle-output") match {
    71       case dockable: Output_Dockable => Some(dockable)
    72       case _ => None
    73     }
    74 
    75   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
    76     wm(view).getDockableWindow("isabelle-raw-output") match {
    77       case dockable: Raw_Output_Dockable => Some(dockable)
    78       case _ => None
    79     }
    80 
    81   def docked_protocol(view: View): Option[Protocol_Dockable] =
    82     wm(view).getDockableWindow("isabelle-protocol") match {
    83       case dockable: Protocol_Dockable => Some(dockable)
    84       case _ => None
    85     }
    86 
    87   def docked_monitor(view: View): Option[Monitor_Dockable] =
    88     wm(view).getDockableWindow("isabelle-monitor") match {
    89       case dockable: Monitor_Dockable => Some(dockable)
    90       case _ => None
    91     }
    92 
    93 
    94   /* continuous checking */
    95 
    96   private val CONTINUOUS_CHECKING = "editor_continuous_checking"
    97 
    98   def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
    99 
   100   def continuous_checking_=(b: Boolean)
   101   {
   102     Swing_Thread.require()
   103 
   104     if (continuous_checking != b) {
   105       PIDE.options.bool(CONTINUOUS_CHECKING) = b
   106       PIDE.options_changed()
   107       PIDE.editor.flush()
   108     }
   109   }
   110 
   111   def set_continuous_checking() { continuous_checking = true }
   112   def reset_continuous_checking() { continuous_checking = false }
   113   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
   114 
   115 
   116   /* required document nodes */
   117 
   118   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
   119   {
   120     Swing_Thread.require()
   121     PIDE.document_model(view.getBuffer) match {
   122       case Some(model) =>
   123         model.node_required = (if (toggle) !model.node_required else set)
   124       case None =>
   125     }
   126   }
   127 
   128   def set_node_required(view: View) { node_required_update(view, set = true) }
   129   def reset_node_required(view: View) { node_required_update(view, set = false) }
   130   def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
   131 
   132 
   133   /* font size */
   134 
   135   def reset_font_size(view: View): Unit =
   136     Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
   137 
   138   def increase_font_size(view: View): Unit =
   139     Rendering.font_size_change(view, i => i + ((i / 10) max 1))
   140 
   141   def decrease_font_size(view: View): Unit =
   142     Rendering.font_size_change(view, i => i - ((i / 10) max 1))
   143 
   144 
   145   /* structured insert */
   146 
   147   def insert_line_padding(text_area: JEditTextArea, text: String)
   148   {
   149     val buffer = text_area.getBuffer
   150     JEdit_Lib.buffer_edit(buffer) {
   151       val text1 =
   152         if (text_area.getSelectionCount == 0) {
   153           def pad(range: Text.Range): String =
   154             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
   155 
   156           val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
   157           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
   158           pad(before_caret) + text + pad(caret)
   159         }
   160         else text
   161       text_area.setSelectedText(text1)
   162     }
   163   }
   164 
   165 
   166   /* completion */
   167 
   168   def complete(view: View)
   169   {
   170     Completion_Popup.Text_Area(view.getTextArea) match {
   171       case Some(text_area_completion) => text_area_completion.action(true)
   172       case None => CompleteWord.completeWord(view)
   173     }
   174   }
   175 
   176 
   177   /* control styles */
   178 
   179   def control_sub(text_area: JEditTextArea)
   180   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
   181 
   182   def control_sup(text_area: JEditTextArea)
   183   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
   184 
   185   def control_bold(text_area: JEditTextArea)
   186   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   187 
   188   def control_reset(text_area: JEditTextArea)
   189   { Token_Markup.edit_control_style(text_area, "") }
   190 
   191 
   192   /* block styles */
   193 
   194   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   195   {
   196     s1.foreach(text_area.userInput(_))
   197     s2.foreach(text_area.userInput(_))
   198     s2.foreach(_ => text_area.goToPrevCharacter(false))
   199   }
   200 
   201   def input_bsub(text_area: JEditTextArea)
   202   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   203 
   204   def input_bsup(text_area: JEditTextArea)
   205   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   206 }
   207