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