src/Tools/jEdit/src/isabelle.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64817 0bb6b582bb4f
child 64882 c3b42ac0cf81
permissions -rw-r--r--
tuned signature;
     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 java.awt.Frame
    13 
    14 import scala.swing.CheckBox
    15 import scala.swing.event.ButtonClicked
    16 
    17 import org.gjt.sp.jedit.{jEdit, View, Buffer}
    18 import org.gjt.sp.jedit.buffer.JEditBuffer
    19 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, StructureMatcher, Selection}
    20 import org.gjt.sp.jedit.syntax.TokenMarker
    21 import org.gjt.sp.jedit.indent.IndentRule
    22 import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
    23 import org.jedit.options.CombinedOptions
    24 
    25 
    26 object Isabelle
    27 {
    28   /* editor modes */
    29 
    30   val modes =
    31     List(
    32       "isabelle",         // theory source
    33       "isabelle-ml",      // ML source
    34       "isabelle-news",    // NEWS
    35       "isabelle-options", // etc/options
    36       "isabelle-output",  // pretty text area output
    37       "isabelle-root",    // session ROOT
    38       "sml")              // Standard ML (not Isabelle/ML)
    39 
    40   private lazy val ml_syntax: Outer_Syntax =
    41     Outer_Syntax.init().no_tokens.
    42       set_language_context(Completion.Language_Context.ML_outer)
    43 
    44   private lazy val sml_syntax: Outer_Syntax =
    45     Outer_Syntax.init().no_tokens.
    46       set_language_context(Completion.Language_Context.SML_outer)
    47 
    48   private lazy val news_syntax: Outer_Syntax =
    49     Outer_Syntax.init().no_tokens
    50 
    51   def mode_syntax(mode: String): Option[Outer_Syntax] =
    52     mode match {
    53       case "isabelle" => Some(PIDE.resources.base.syntax)
    54       case "isabelle-options" => Some(Options.options_syntax)
    55       case "isabelle-root" => Some(Sessions.root_syntax)
    56       case "isabelle-ml" => Some(ml_syntax)
    57       case "isabelle-news" => Some(news_syntax)
    58       case "isabelle-output" => None
    59       case "sml" => Some(sml_syntax)
    60       case _ => None
    61     }
    62 
    63   def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
    64     if (buffer == null) None
    65     else
    66       (JEdit_Lib.buffer_mode(buffer), Document_Model.get(buffer)) match {
    67         case ("isabelle", Some(model)) =>
    68           Some(PIDE.session.recent_syntax(model.node_name))
    69         case (mode, _) => mode_syntax(mode)
    70       }
    71 
    72 
    73   /* token markers */
    74 
    75   private val mode_markers: Map[String, TokenMarker] =
    76     Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) +
    77       ("bibtex" -> new Bibtex_JEdit.Token_Marker)
    78 
    79   def mode_token_marker(mode: String): Option[TokenMarker] = mode_markers.get(mode)
    80 
    81   def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
    82   {
    83     val mode = JEdit_Lib.buffer_mode(buffer)
    84     if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
    85     else mode_token_marker(mode)
    86   }
    87 
    88 
    89   /* text structure */
    90 
    91   def indent_rule(mode: String): Option[IndentRule] =
    92     mode match {
    93       case "isabelle" | "isabelle-options" | "isabelle-root" =>
    94         Some(Text_Structure.Indent_Rule)
    95       case _ => None
    96     }
    97 
    98   def structure_matchers(mode: String): List[StructureMatcher] =
    99     if (mode == "isabelle") List(Text_Structure.Matcher) else Nil
   100 
   101 
   102   /* dockable windows */
   103 
   104   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
   105 
   106   def debugger_dockable(view: View): Option[Debugger_Dockable] =
   107     wm(view).getDockableWindow("isabelle-debugger") match {
   108       case dockable: Debugger_Dockable => Some(dockable)
   109       case _ => None
   110     }
   111 
   112   def documentation_dockable(view: View): Option[Documentation_Dockable] =
   113     wm(view).getDockableWindow("isabelle-documentation") match {
   114       case dockable: Documentation_Dockable => Some(dockable)
   115       case _ => None
   116     }
   117 
   118   def monitor_dockable(view: View): Option[Monitor_Dockable] =
   119     wm(view).getDockableWindow("isabelle-monitor") match {
   120       case dockable: Monitor_Dockable => Some(dockable)
   121       case _ => None
   122     }
   123 
   124   def output_dockable(view: View): Option[Output_Dockable] =
   125     wm(view).getDockableWindow("isabelle-output") match {
   126       case dockable: Output_Dockable => Some(dockable)
   127       case _ => None
   128     }
   129 
   130   def protocol_dockable(view: View): Option[Protocol_Dockable] =
   131     wm(view).getDockableWindow("isabelle-protocol") match {
   132       case dockable: Protocol_Dockable => Some(dockable)
   133       case _ => None
   134     }
   135 
   136   def query_dockable(view: View): Option[Query_Dockable] =
   137     wm(view).getDockableWindow("isabelle-query") match {
   138       case dockable: Query_Dockable => Some(dockable)
   139       case _ => None
   140     }
   141 
   142   def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
   143     wm(view).getDockableWindow("isabelle-raw-output") match {
   144       case dockable: Raw_Output_Dockable => Some(dockable)
   145       case _ => None
   146     }
   147 
   148   def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
   149     wm(view).getDockableWindow("isabelle-simplifier-trace") match {
   150       case dockable: Simplifier_Trace_Dockable => Some(dockable)
   151       case _ => None
   152     }
   153 
   154   def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
   155     wm(view).getDockableWindow("isabelle-sledgehammer") match {
   156       case dockable: Sledgehammer_Dockable => Some(dockable)
   157       case _ => None
   158     }
   159 
   160   def state_dockable(view: View): Option[State_Dockable] =
   161     wm(view).getDockableWindow("isabelle-state") match {
   162       case dockable: State_Dockable => Some(dockable)
   163       case _ => None
   164     }
   165 
   166   def symbols_dockable(view: View): Option[Symbols_Dockable] =
   167     wm(view).getDockableWindow("isabelle-symbols") match {
   168       case dockable: Symbols_Dockable => Some(dockable)
   169       case _ => None
   170     }
   171 
   172   def syslog_dockable(view: View): Option[Syslog_Dockable] =
   173     wm(view).getDockableWindow("isabelle-syslog") match {
   174       case dockable: Syslog_Dockable => Some(dockable)
   175       case _ => None
   176     }
   177 
   178   def theories_dockable(view: View): Option[Theories_Dockable] =
   179     wm(view).getDockableWindow("isabelle-theories") match {
   180       case dockable: Theories_Dockable => Some(dockable)
   181       case _ => None
   182     }
   183 
   184   def timing_dockable(view: View): Option[Timing_Dockable] =
   185     wm(view).getDockableWindow("isabelle-timing") match {
   186       case dockable: Timing_Dockable => Some(dockable)
   187       case _ => None
   188     }
   189 
   190 
   191   /* continuous checking */
   192 
   193   private val CONTINUOUS_CHECKING = "editor_continuous_checking"
   194 
   195   def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
   196   def continuous_checking_=(b: Boolean): Unit =
   197     GUI_Thread.require {
   198       if (continuous_checking != b) {
   199         PIDE.options.bool(CONTINUOUS_CHECKING) = b
   200         PIDE.session.update_options(PIDE.options.value)
   201       }
   202     }
   203 
   204   def set_continuous_checking() { continuous_checking = true }
   205   def reset_continuous_checking() { continuous_checking = false }
   206   def toggle_continuous_checking() { continuous_checking = !continuous_checking }
   207 
   208   class Continuous_Checking extends CheckBox("Continuous checking")
   209   {
   210     tooltip = "Continuous checking of proof document (visible and required parts)"
   211     reactions += { case ButtonClicked(_) => continuous_checking = selected }
   212     def load() { selected = continuous_checking }
   213     load()
   214   }
   215 
   216 
   217   /* update state */
   218 
   219   def update_state(view: View): Unit =
   220     state_dockable(view).foreach(_.update_request())
   221 
   222 
   223   /* ML statistics */
   224 
   225   class ML_Stats extends
   226     JEdit_Options.Check_Box("ML_statistics", "ML statistics", "Enable ML runtime system statistics")
   227 
   228 
   229   /* required document nodes */
   230 
   231   def set_node_required(view: View) { Document_Model.view_node_required(view, set = true) }
   232   def reset_node_required(view: View) { Document_Model.view_node_required(view, set = false) }
   233   def toggle_node_required(view: View) { Document_Model.view_node_required(view, toggle = true) }
   234 
   235 
   236   /* font size */
   237 
   238   def reset_font_size() {
   239     Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
   240   }
   241   def increase_font_size() { Font_Info.main_change.step(1) }
   242   def decrease_font_size() { Font_Info.main_change.step(-1) }
   243 
   244 
   245   /* structured edits */
   246 
   247   def newline(text_area: TextArea)
   248   {
   249     if (!text_area.isEditable()) text_area.getToolkit().beep()
   250     else {
   251       val buffer = text_area.getBuffer
   252       def nl { text_area.userInput('\n') }
   253 
   254       if (indent_rule(JEdit_Lib.buffer_mode(buffer)).isDefined &&
   255           buffer.getStringProperty("autoIndent") == "full" &&
   256           PIDE.options.bool("jedit_indent_newline"))
   257       {
   258         Isabelle.buffer_syntax(buffer) match {
   259           case Some(syntax) if buffer.isInstanceOf[Buffer] =>
   260             val keywords = syntax.keywords
   261 
   262             val caret = text_area.getCaretPosition
   263             val line = text_area.getCaretLine
   264             val line_range = JEdit_Lib.line_range(buffer, line)
   265 
   266             def line_content(start: Text.Offset, stop: Text.Offset, context: Scan.Line_Context)
   267               : (List[Token], Scan.Line_Context) =
   268             {
   269               val text = JEdit_Lib.try_get_text(buffer, Text.Range(start, stop)).getOrElse("")
   270               val (toks, context1) = Token.explode_line(keywords, text, context)
   271               val toks1 = toks.filterNot(_.is_space)
   272               (toks1, context1)
   273             }
   274 
   275             val context0 = Token_Markup.Line_Context.prev(buffer, line).get_context
   276             val (tokens1, context1) = line_content(line_range.start, caret, context0)
   277             val (tokens2, _) = line_content(caret, line_range.stop, context1)
   278 
   279             if (tokens1.nonEmpty && keywords.is_indent_command(tokens1.head))
   280               buffer.indentLine(line, true)
   281 
   282             if (tokens2.isEmpty || keywords.is_indent_command(tokens2.head))
   283               JEdit_Lib.buffer_edit(buffer) {
   284                 text_area.setSelectedText("\n")
   285                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
   286               }
   287             else nl
   288           case _ => nl
   289         }
   290       }
   291       else nl
   292     }
   293   }
   294 
   295   def insert_line_padding(text_area: JEditTextArea, text: String)
   296   {
   297     val buffer = text_area.getBuffer
   298     JEdit_Lib.buffer_edit(buffer) {
   299       val text1 =
   300         if (text_area.getSelectionCount == 0) {
   301           def pad(range: Text.Range): String =
   302             if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
   303 
   304           val caret = JEdit_Lib.caret_range(text_area)
   305           val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
   306           pad(before_caret) + text + pad(caret)
   307         }
   308         else text
   309       text_area.setSelectedText(text1)
   310     }
   311   }
   312 
   313   def edit_command(
   314     snapshot: Document.Snapshot,
   315     text_area: TextArea,
   316     padding: Boolean,
   317     id: Document_ID.Generic,
   318     text: String)
   319   {
   320     val buffer = text_area.getBuffer
   321     if (!snapshot.is_outdated && text != "") {
   322       (snapshot.find_command(id), Document_Model.get(buffer)) match {
   323         case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
   324           node.command_start(command) match {
   325             case Some(start) =>
   326               JEdit_Lib.buffer_edit(buffer) {
   327                 val range = command.proper_range + start
   328                 JEdit_Lib.buffer_edit(buffer) {
   329                   if (padding) {
   330                     text_area.moveCaretPosition(start + range.length)
   331                     val start_line = text_area.getCaretLine + 1
   332                     text_area.setSelectedText("\n" + text)
   333                     val end_line = text_area.getCaretLine
   334                     buffer.indentLines(start_line, end_line)
   335                   }
   336                   else {
   337                     buffer.remove(start, range.length)
   338                     text_area.moveCaretPosition(start)
   339                     text_area.setSelectedText(text)
   340                   }
   341                 }
   342               }
   343             case None =>
   344           }
   345         case _ =>
   346       }
   347     }
   348   }
   349 
   350 
   351   /* selection */
   352 
   353   def select_entity(text_area: JEditTextArea)
   354   {
   355     for {
   356       doc_view <- PIDE.document_view(text_area)
   357       rendering = doc_view.get_rendering()
   358     } {
   359       val caret_range = JEdit_Lib.caret_range(text_area)
   360       val buffer_range = JEdit_Lib.buffer_range(text_area.getBuffer)
   361       val active_focus = rendering.caret_focus_ranges(caret_range, buffer_range)
   362       if (active_focus.nonEmpty) {
   363         text_area.selectNone()
   364         for (r <- active_focus)
   365           text_area.addToSelection(new Selection.Range(r.start, r.stop))
   366       }
   367     }
   368   }
   369 
   370 
   371   /* completion */
   372 
   373   def complete(view: View, word_only: Boolean)
   374   {
   375     Completion_Popup.Text_Area.action(view.getTextArea, word_only)
   376   }
   377 
   378 
   379   /* control styles */
   380 
   381   def control_sub(text_area: JEditTextArea)
   382   { Token_Markup.edit_control_style(text_area, Symbol.sub) }
   383 
   384   def control_sup(text_area: JEditTextArea)
   385   { Token_Markup.edit_control_style(text_area, Symbol.sup) }
   386 
   387   def control_bold(text_area: JEditTextArea)
   388   { Token_Markup.edit_control_style(text_area, Symbol.bold) }
   389 
   390   def control_emph(text_area: JEditTextArea)
   391   { Token_Markup.edit_control_style(text_area, Symbol.emph) }
   392 
   393   def control_reset(text_area: JEditTextArea)
   394   { Token_Markup.edit_control_style(text_area, "") }
   395 
   396 
   397   /* block styles */
   398 
   399   private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
   400   {
   401     s1.foreach(text_area.userInput(_))
   402     s2.foreach(text_area.userInput(_))
   403     s2.foreach(_ => text_area.goToPrevCharacter(false))
   404   }
   405 
   406   def input_bsub(text_area: JEditTextArea)
   407   { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
   408 
   409   def input_bsup(text_area: JEditTextArea)
   410   { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
   411 
   412 
   413   /* spell-checker dictionary */
   414 
   415   def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
   416   {
   417     for {
   418       spell_checker <- PIDE.spell_checker.get
   419       doc_view <- PIDE.document_view(text_area)
   420       rendering = doc_view.get_rendering()
   421       range = JEdit_Lib.caret_range(text_area)
   422       Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
   423     } {
   424       spell_checker.update(word, include, permanent)
   425       JEdit_Lib.jedit_views().foreach(_.repaint())
   426     }
   427   }
   428 
   429   def reset_dictionary()
   430   {
   431     for (spell_checker <- PIDE.spell_checker.get)
   432     {
   433       spell_checker.reset()
   434       JEdit_Lib.jedit_views().foreach(_.repaint())
   435     }
   436   }
   437 
   438 
   439   /* debugger */
   440 
   441   def toggle_breakpoint(text_area: JEditTextArea): Unit =
   442     if (Debugger.is_active()) {
   443       for {
   444         (command, serial) <- Debugger_Dockable.get_breakpoint(text_area, text_area.getCaretPosition)
   445       } Debugger_Dockable.toggle_breakpoint(command, serial)
   446     }
   447 
   448 
   449   /* plugin options */
   450 
   451   def plugin_options(frame: Frame)
   452   {
   453     GUI_Thread.require {}
   454     jEdit.setProperty("Plugin Options.last", "isabelle-general")
   455     new CombinedOptions(frame, 1)
   456   }
   457 }