src/Tools/jEdit/src/isabelle.scala
author wenzelm
Tue Feb 18 19:00:13 2014 +0100 (2014-02-18)
changeset 55557 aa1adeca714b
parent 55500 cdbbaa3074a8
child 55558 298274c970b6
permissions -rw-r--r--
standardized action and panel names;
     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 scala.swing.CheckBox
    13 import scala.swing.event.ButtonClicked
    14 
    15 import org.gjt.sp.jedit.{jEdit, View, Buffer}
    16 import org.gjt.sp.jedit.textarea.JEditTextArea
    17 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
    18 
    19 
    20 object Isabelle
    21 {
    22   /* editor modes */
    23 
    24   val modes =
    25     List(
    26       "isabelle",         // theory source
    27       "isabelle-ml",      // ML source
    28       "isabelle-markup",  // SideKick markup tree
    29       "isabelle-news",    // NEWS
    30       "isabelle-options", // etc/options
    31       "isabelle-output",  // pretty text area output
    32       "isabelle-root")    // session ROOT
    33 
    34   private lazy val symbols_syntax = Outer_Syntax.init().no_tokens
    35 
    36   def mode_syntax(name: String): Option[Outer_Syntax] =
    37     name match {
    38       case "isabelle" | "isabelle-markup" =>
    39         val syntax = PIDE.session.recent_syntax
    40         if (syntax == Outer_Syntax.empty) None else Some(syntax)
    41       case "isabelle-options" => Some(Options.options_syntax)
    42       case "isabelle-root" => Some(Build.root_syntax)
    43       case "isabelle-ml" | "isabelle-news" => Some(symbols_syntax)
    44       case "isabelle-output" => None
    45       case _ => None
    46     }
    47 
    48 
    49   /* token markers */
    50 
    51   private val markers =
    52     Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
    53 
    54   def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
    55 
    56 
    57   /* dockable windows */
    58 
    59   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    60 
    61   def docked_theories(view: View): Option[Theories_Dockable] =
    62     wm(view).getDockableWindow("isabelle-theories") match {
    63       case dockable: Theories_Dockable => Some(dockable)
    64       case _ => None
    65     }
    66 
    67   def docked_timing(view: View): Option[Timing_Dockable] =
    68     wm(view).getDockableWindow("isabelle-timing") match {
    69       case dockable: Timing_Dockable => Some(dockable)
    70       case _ => None
    71     }
    72 
    73   def docked_output(view: View): Option[Output_Dockable] =
    74     wm(view).getDockableWindow("isabelle-output") match {
    75       case dockable: Output_Dockable => Some(dockable)
    76       case _ => None
    77     }
    78 
    79   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
    80     wm(view).getDockableWindow("isabelle-raw-output") match {
    81       case dockable: Raw_Output_Dockable => Some(dockable)
    82       case _ => None
    83     }
    84 
    85   def docked_simplifier_trace(view: View): Option[Simplifier_Trace_Dockable] =
    86     wm(view).getDockableWindow("isabelle-simplifier-trace") match {
    87       case dockable: Simplifier_Trace_Dockable => Some(dockable)
    88       case _ => None
    89     }
    90 
    91   def docked_protocol(view: View): Option[Protocol_Dockable] =
    92     wm(view).getDockableWindow("isabelle-protocol") match {
    93       case dockable: Protocol_Dockable => Some(dockable)
    94       case _ => None
    95     }
    96 
    97   def docked_monitor(view: View): Option[Monitor_Dockable] =
    98     wm(view).getDockableWindow("isabelle-monitor") match {
    99       case dockable: Monitor_Dockable => Some(dockable)
   100       case _ => None
   101     }
   102 
   103 
   104   /* continuous checking */
   105 
   106   private val CONTINUOUS_CHECKING = "editor_continuous_checking"
   107 
   108   def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
   109 
   110   def continuous_checking_=(b: Boolean)
   111   {
   112     Swing_Thread.require()
   113 
   114     if (continuous_checking != b) {
   115       PIDE.options.bool(CONTINUOUS_CHECKING) = b
   116       PIDE.options_changed()
   117       PIDE.editor.flush()
   118     }
   119   }
   120 
   121   def set_continuous_checking() { continuous_checking = true }
   122   def reset_continuous_checking() { continuous_checking = false }
   123   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
   124 
   125   class Continuous_Checking extends CheckBox("Continuous checking")
   126   {
   127     tooltip = "Continuous checking of proof document (visible and required parts)"
   128     reactions += { case ButtonClicked(_) => continuous_checking = selected }
   129     def load() { selected = continuous_checking }
   130     load()
   131   }
   132 
   133 
   134   /* required document nodes */
   135 
   136   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
   137   {
   138     Swing_Thread.require()
   139     PIDE.document_model(view.getBuffer) match {
   140       case Some(model) =>
   141         model.node_required = (if (toggle) !model.node_required else set)
   142       case None =>
   143     }
   144   }
   145 
   146   def set_node_required(view: View) { node_required_update(view, set = true) }
   147   def reset_node_required(view: View) { node_required_update(view, set = false) }
   148   def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
   149 
   150 
   151   /* font size */
   152 
   153   def reset_font_size(view: View): Unit =
   154     Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
   155 
   156   def increase_font_size(view: View): Unit =
   157     Rendering.font_size_change(view, i => i + ((i / 10) max 1))
   158 
   159   def decrease_font_size(view: View): Unit =
   160     Rendering.font_size_change(view, i => i - ((i / 10) max 1))
   161 
   162 
   163   /* structured edits */
   164 
   165   def insert_line_padding(text_area: JEditTextArea, text: String)
   166   {
   167     val buffer = text_area.getBuffer
   168     JEdit_Lib.buffer_edit(buffer) {
   169       val text1 =
   170         if (text_area.getSelectionCount == 0) {
   171           def pad(range: Text.Range): String =
   172             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
   173 
   174           val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
   175           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
   176           pad(before_caret) + text + pad(caret)
   177         }
   178         else text
   179       text_area.setSelectedText(text1)
   180     }
   181   }
   182 
   183   def edit_command(
   184     snapshot: Document.Snapshot,
   185     buffer: Buffer,
   186     padding: Boolean,
   187     id: Document_ID.Generic,
   188     s: String)
   189   {
   190     if (!snapshot.is_outdated) {
   191       snapshot.state.find_command(snapshot.version, id) match {
   192         case Some((node, command)) =>
   193           node.command_start(command) match {
   194             case Some(start) =>
   195               JEdit_Lib.buffer_edit(buffer) {
   196                 val range = command.proper_range + start
   197                 if (padding) {
   198                   buffer.insert(start + range.length, "\n" + s)
   199                 }
   200                 else {
   201                   buffer.remove(start, range.length)
   202                   buffer.insert(start, s)
   203                 }
   204               }
   205             case None =>
   206           }
   207         case None =>
   208       }
   209     }
   210   }
   211 
   212 
   213   /* completion */
   214 
   215   def complete(view: View)
   216   {
   217     Completion_Popup.Text_Area(view.getTextArea) match {
   218       case Some(text_area_completion) =>
   219         text_area_completion.action(immediate = true, explicit = true)
   220       case None => CompleteWord.completeWord(view)
   221     }
   222   }
   223 
   224 
   225   /* control styles */
   226 
   227   def control_sub(text_area: JEditTextArea)
   228   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
   229 
   230   def control_sup(text_area: JEditTextArea)
   231   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
   232 
   233   def control_bold(text_area: JEditTextArea)
   234   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   235 
   236   def control_reset(text_area: JEditTextArea)
   237   { Token_Markup.edit_control_style(text_area, "") }
   238 
   239 
   240   /* block styles */
   241 
   242   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   243   {
   244     s1.foreach(text_area.userInput(_))
   245     s2.foreach(text_area.userInput(_))
   246     s2.foreach(_ => text_area.goToPrevCharacter(false))
   247   }
   248 
   249   def input_bsub(text_area: JEditTextArea)
   250   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   251 
   252   def input_bsup(text_area: JEditTextArea)
   253   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   254 }
   255