src/Tools/jEdit/src/isabelle.scala
author wenzelm
Tue Apr 15 11:26:17 2014 +0200 (2014-04-15)
changeset 56586 5ef60881681d
parent 56578 e73723b39c82
child 56587 83777a91f5de
permissions -rw-r--r--
explicit menu action to complete word;
     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       "sml")              // Standard ML (not Isabelle/ML)
    34 
    35   private lazy val ml_syntax: Outer_Syntax =
    36     Outer_Syntax.init().no_tokens.
    37       set_language_context(Completion.Language_Context.ML_outer)
    38 
    39   private lazy val sml_syntax: Outer_Syntax =
    40     Outer_Syntax.init().no_tokens.
    41       set_language_context(Completion.Language_Context.SML_outer)
    42 
    43   private lazy val news_syntax: Outer_Syntax =
    44     Outer_Syntax.init().no_tokens
    45 
    46   def mode_syntax(name: String): Option[Outer_Syntax] =
    47     name match {
    48       case "isabelle" | "isabelle-markup" =>
    49         PIDE.session.recent_syntax match {
    50           case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
    51           case _ => None
    52         }
    53       case "isabelle-options" => Some(Options.options_syntax)
    54       case "isabelle-root" => Some(Build.root_syntax)
    55       case "isabelle-ml" => Some(ml_syntax)
    56       case "isabelle-news" => Some(news_syntax)
    57       case "isabelle-output" => None
    58       case "sml" => Some(sml_syntax)
    59       case _ => None
    60     }
    61 
    62 
    63   /* token markers */
    64 
    65   private val markers =
    66     Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
    67 
    68   def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
    69 
    70 
    71   /* dockable windows */
    72 
    73   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
    74 
    75   def documentation_dockable(view: View): Option[Documentation_Dockable] =
    76     wm(view).getDockableWindow("isabelle-documentation") match {
    77       case dockable: Documentation_Dockable => Some(dockable)
    78       case _ => None
    79     }
    80 
    81   def find_dockable(view: View): Option[Find_Dockable] =
    82     wm(view).getDockableWindow("isabelle-find") match {
    83       case dockable: Find_Dockable => Some(dockable)
    84       case _ => None
    85     }
    86 
    87   def monitor_dockable(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   def output_dockable(view: View): Option[Output_Dockable] =
    94     wm(view).getDockableWindow("isabelle-output") match {
    95       case dockable: Output_Dockable => Some(dockable)
    96       case _ => None
    97     }
    98 
    99   def protocol_dockable(view: View): Option[Protocol_Dockable] =
   100     wm(view).getDockableWindow("isabelle-protocol") match {
   101       case dockable: Protocol_Dockable => Some(dockable)
   102       case _ => None
   103     }
   104 
   105   def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
   106     wm(view).getDockableWindow("isabelle-raw-output") match {
   107       case dockable: Raw_Output_Dockable => Some(dockable)
   108       case _ => None
   109     }
   110 
   111   def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
   112     wm(view).getDockableWindow("isabelle-simplifier-trace") match {
   113       case dockable: Simplifier_Trace_Dockable => Some(dockable)
   114       case _ => None
   115     }
   116 
   117   def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
   118     wm(view).getDockableWindow("isabelle-sledgehammer") match {
   119       case dockable: Sledgehammer_Dockable => Some(dockable)
   120       case _ => None
   121     }
   122 
   123   def symbols_dockable(view: View): Option[Symbols_Dockable] =
   124     wm(view).getDockableWindow("isabelle-symbols") match {
   125       case dockable: Symbols_Dockable => Some(dockable)
   126       case _ => None
   127     }
   128 
   129   def syslog_dockable(view: View): Option[Syslog_Dockable] =
   130     wm(view).getDockableWindow("isabelle-syslog") match {
   131       case dockable: Syslog_Dockable => Some(dockable)
   132       case _ => None
   133     }
   134 
   135   def theories_dockable(view: View): Option[Theories_Dockable] =
   136     wm(view).getDockableWindow("isabelle-theories") match {
   137       case dockable: Theories_Dockable => Some(dockable)
   138       case _ => None
   139     }
   140 
   141   def timing_dockable(view: View): Option[Timing_Dockable] =
   142     wm(view).getDockableWindow("isabelle-timing") match {
   143       case dockable: Timing_Dockable => Some(dockable)
   144       case _ => None
   145     }
   146 
   147 
   148   /* continuous checking */
   149 
   150   private val CONTINUOUS_CHECKING = "editor_continuous_checking"
   151 
   152   def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
   153 
   154   def continuous_checking_=(b: Boolean)
   155   {
   156     Swing_Thread.require()
   157 
   158     if (continuous_checking != b) {
   159       PIDE.options.bool(CONTINUOUS_CHECKING) = b
   160       PIDE.options_changed()
   161       PIDE.editor.flush()
   162     }
   163   }
   164 
   165   def set_continuous_checking() { continuous_checking = true }
   166   def reset_continuous_checking() { continuous_checking = false }
   167   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
   168 
   169   class Continuous_Checking extends CheckBox("Continuous checking")
   170   {
   171     tooltip = "Continuous checking of proof document (visible and required parts)"
   172     reactions += { case ButtonClicked(_) => continuous_checking = selected }
   173     def load() { selected = continuous_checking }
   174     load()
   175   }
   176 
   177 
   178   /* required document nodes */
   179 
   180   private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
   181   {
   182     Swing_Thread.require()
   183     PIDE.document_model(view.getBuffer) match {
   184       case Some(model) =>
   185         model.node_required = (if (toggle) !model.node_required else set)
   186       case None =>
   187     }
   188   }
   189 
   190   def set_node_required(view: View) { node_required_update(view, set = true) }
   191   def reset_node_required(view: View) { node_required_update(view, set = false) }
   192   def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
   193 
   194 
   195   /* font size */
   196 
   197   def reset_font_size() {
   198     Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
   199   }
   200   def increase_font_size() { Font_Info.main_change.step(1) }
   201   def decrease_font_size() { Font_Info.main_change.step(-1) }
   202 
   203 
   204   /* structured edits */
   205 
   206   def insert_line_padding(text_area: JEditTextArea, text: String)
   207   {
   208     val buffer = text_area.getBuffer
   209     JEdit_Lib.buffer_edit(buffer) {
   210       val text1 =
   211         if (text_area.getSelectionCount == 0) {
   212           def pad(range: Text.Range): String =
   213             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
   214 
   215           val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
   216           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
   217           pad(before_caret) + text + pad(caret)
   218         }
   219         else text
   220       text_area.setSelectedText(text1)
   221     }
   222   }
   223 
   224   def edit_command(
   225     snapshot: Document.Snapshot,
   226     buffer: Buffer,
   227     padding: Boolean,
   228     id: Document_ID.Generic,
   229     s: String)
   230   {
   231     if (!snapshot.is_outdated) {
   232       snapshot.state.find_command(snapshot.version, id) match {
   233         case Some((node, command)) =>
   234           node.command_start(command) match {
   235             case Some(start) =>
   236               JEdit_Lib.buffer_edit(buffer) {
   237                 val range = command.proper_range + start
   238                 if (padding) {
   239                   buffer.insert(start + range.length, "\n" + s)
   240                 }
   241                 else {
   242                   buffer.remove(start, range.length)
   243                   buffer.insert(start, s)
   244                 }
   245               }
   246             case None =>
   247           }
   248         case None =>
   249       }
   250     }
   251   }
   252 
   253 
   254   /* completion */
   255 
   256   def complete(view: View, word_only: Boolean)
   257   {
   258     if (!Completion_Popup.Text_Area.action(view.getTextArea, word_only))
   259       CompleteWord.completeWord(view)
   260   }
   261 
   262 
   263   /* control styles */
   264 
   265   def control_sub(text_area: JEditTextArea)
   266   { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
   267 
   268   def control_sup(text_area: JEditTextArea)
   269   { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
   270 
   271   def control_bold(text_area: JEditTextArea)
   272   { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
   273 
   274   def control_reset(text_area: JEditTextArea)
   275   { Token_Markup.edit_control_style(text_area, "") }
   276 
   277 
   278   /* block styles */
   279 
   280   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   281   {
   282     s1.foreach(text_area.userInput(_))
   283     s2.foreach(text_area.userInput(_))
   284     s2.foreach(_ => text_area.goToPrevCharacter(false))
   285   }
   286 
   287   def input_bsub(text_area: JEditTextArea)
   288   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   289 
   290   def input_bsup(text_area: JEditTextArea)
   291   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   292 
   293 
   294   /* spell-checker dictionary */
   295 
   296   def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
   297   {
   298     for {
   299       spell_checker <- PIDE.spell_checker.get
   300       doc_view <- PIDE.document_view(text_area)
   301       rendering = doc_view.get_rendering()
   302       range = JEdit_Lib.before_caret_range(text_area, rendering)
   303       Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
   304     } {
   305       spell_checker.update(word, include, permanent)
   306       JEdit_Lib.jedit_views().foreach(_.repaint())
   307     }
   308   }
   309 
   310   def reset_dictionary()
   311   {
   312     for (spell_checker <- PIDE.spell_checker.get)
   313     {
   314       spell_checker.reset()
   315       JEdit_Lib.jedit_views().foreach(_.repaint())
   316     }
   317   }
   318 }
   319