src/Tools/jEdit/src/isabelle.scala
author wenzelm
Tue Aug 05 12:42:38 2014 +0200 (2014-08-05 ago)
changeset 57861 287e3b1298b3
parent 57627 65fc7ae1bf66
child 58529 cd4439d8799c
permissions -rw-r--r--
restrict edit_command (for sendback) to current node -- no attempt to goto target buffer first, which might not be loaded;
wenzelm@50208
     1
/*  Title:      Tools/jEdit/src/isabelle.scala
wenzelm@50183
     2
    Author:     Makarius
wenzelm@50183
     3
wenzelm@53277
     4
Global configuration and convenience operations for Isabelle/jEdit.
wenzelm@50183
     5
*/
wenzelm@50183
     6
wenzelm@50183
     7
package isabelle.jedit
wenzelm@50183
     8
wenzelm@50183
     9
wenzelm@50183
    10
import isabelle._
wenzelm@50183
    11
wenzelm@57627
    12
import java.awt.Frame
wenzelm@57627
    13
wenzelm@53715
    14
import scala.swing.CheckBox
wenzelm@53715
    15
import scala.swing.event.ButtonClicked
wenzelm@53715
    16
wenzelm@50198
    17
import org.gjt.sp.jedit.{jEdit, View, Buffer}
wenzelm@50183
    18
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@53293
    19
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
wenzelm@57627
    20
import org.gjt.sp.jedit.options.PluginOptions
wenzelm@50183
    21
wenzelm@50183
    22
wenzelm@50208
    23
object Isabelle
wenzelm@50183
    24
{
wenzelm@53274
    25
  /* editor modes */
wenzelm@53274
    26
wenzelm@53277
    27
  val modes =
wenzelm@53277
    28
    List(
wenzelm@53277
    29
      "isabelle",         // theory source
wenzelm@55500
    30
      "isabelle-ml",      // ML source
wenzelm@53281
    31
      "isabelle-markup",  // SideKick markup tree
wenzelm@53277
    32
      "isabelle-news",    // NEWS
wenzelm@53277
    33
      "isabelle-options", // etc/options
wenzelm@53277
    34
      "isabelle-output",  // pretty text area output
wenzelm@56277
    35
      "isabelle-root",    // session ROOT
wenzelm@56277
    36
      "sml")              // Standard ML (not Isabelle/ML)
wenzelm@53274
    37
wenzelm@55616
    38
  private lazy val ml_syntax: Outer_Syntax =
wenzelm@55616
    39
    Outer_Syntax.init().no_tokens.
wenzelm@55749
    40
      set_language_context(Completion.Language_Context.ML_outer)
wenzelm@55616
    41
wenzelm@56278
    42
  private lazy val sml_syntax: Outer_Syntax =
wenzelm@56278
    43
    Outer_Syntax.init().no_tokens.
wenzelm@56278
    44
      set_language_context(Completion.Language_Context.SML_outer)
wenzelm@56278
    45
wenzelm@55616
    46
  private lazy val news_syntax: Outer_Syntax =
wenzelm@55616
    47
    Outer_Syntax.init().no_tokens
wenzelm@53276
    48
wenzelm@53274
    49
  def mode_syntax(name: String): Option[Outer_Syntax] =
wenzelm@53274
    50
    name match {
wenzelm@53281
    51
      case "isabelle" | "isabelle-markup" =>
wenzelm@56393
    52
        PIDE.session.recent_syntax match {
wenzelm@56394
    53
          case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
wenzelm@56393
    54
          case _ => None
wenzelm@56393
    55
        }
wenzelm@53274
    56
      case "isabelle-options" => Some(Options.options_syntax)
wenzelm@53274
    57
      case "isabelle-root" => Some(Build.root_syntax)
wenzelm@55616
    58
      case "isabelle-ml" => Some(ml_syntax)
wenzelm@55616
    59
      case "isabelle-news" => Some(news_syntax)
wenzelm@53277
    60
      case "isabelle-output" => None
wenzelm@56278
    61
      case "sml" => Some(sml_syntax)
wenzelm@53274
    62
      case _ => None
wenzelm@53274
    63
    }
wenzelm@53274
    64
wenzelm@53274
    65
wenzelm@53277
    66
  /* token markers */
wenzelm@53277
    67
wenzelm@53277
    68
  private val markers =
wenzelm@53280
    69
    Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
wenzelm@53277
    70
wenzelm@53277
    71
  def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
wenzelm@53277
    72
wenzelm@53277
    73
wenzelm@50208
    74
  /* dockable windows */
wenzelm@50208
    75
wenzelm@50208
    76
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
wenzelm@50208
    77
wenzelm@55560
    78
  def documentation_dockable(view: View): Option[Documentation_Dockable] =
wenzelm@55560
    79
    wm(view).getDockableWindow("isabelle-documentation") match {
wenzelm@55560
    80
      case dockable: Documentation_Dockable => Some(dockable)
wenzelm@50208
    81
      case _ => None
wenzelm@50208
    82
    }
wenzelm@50208
    83
wenzelm@55560
    84
  def monitor_dockable(view: View): Option[Monitor_Dockable] =
wenzelm@55560
    85
    wm(view).getDockableWindow("isabelle-monitor") match {
wenzelm@55560
    86
      case dockable: Monitor_Dockable => Some(dockable)
wenzelm@55560
    87
      case _ => None
wenzelm@55560
    88
    }
wenzelm@55560
    89
wenzelm@55560
    90
  def output_dockable(view: View): Option[Output_Dockable] =
wenzelm@50208
    91
    wm(view).getDockableWindow("isabelle-output") match {
wenzelm@50208
    92
      case dockable: Output_Dockable => Some(dockable)
wenzelm@50208
    93
      case _ => None
wenzelm@50208
    94
    }
wenzelm@50208
    95
wenzelm@55560
    96
  def protocol_dockable(view: View): Option[Protocol_Dockable] =
wenzelm@55560
    97
    wm(view).getDockableWindow("isabelle-protocol") match {
wenzelm@55560
    98
      case dockable: Protocol_Dockable => Some(dockable)
wenzelm@55560
    99
      case _ => None
wenzelm@55560
   100
    }
wenzelm@55560
   101
wenzelm@56879
   102
  def query_dockable(view: View): Option[Query_Dockable] =
wenzelm@56879
   103
    wm(view).getDockableWindow("isabelle-query") match {
wenzelm@56879
   104
      case dockable: Query_Dockable => Some(dockable)
wenzelm@56879
   105
      case _ => None
wenzelm@56879
   106
    }
wenzelm@56879
   107
wenzelm@55560
   108
  def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
wenzelm@50208
   109
    wm(view).getDockableWindow("isabelle-raw-output") match {
wenzelm@50208
   110
      case dockable: Raw_Output_Dockable => Some(dockable)
wenzelm@50208
   111
      case _ => None
wenzelm@50208
   112
    }
wenzelm@50208
   113
wenzelm@55560
   114
  def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
wenzelm@55559
   115
    wm(view).getDockableWindow("isabelle-simplifier-trace") match {
lars@55316
   116
      case dockable: Simplifier_Trace_Dockable => Some(dockable)
lars@55316
   117
      case _ => None
lars@55316
   118
    }
lars@55316
   119
wenzelm@55560
   120
  def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
wenzelm@55560
   121
    wm(view).getDockableWindow("isabelle-sledgehammer") match {
wenzelm@55560
   122
      case dockable: Sledgehammer_Dockable => Some(dockable)
wenzelm@55560
   123
      case _ => None
wenzelm@55560
   124
    }
wenzelm@55560
   125
wenzelm@55560
   126
  def symbols_dockable(view: View): Option[Symbols_Dockable] =
wenzelm@55560
   127
    wm(view).getDockableWindow("isabelle-symbols") match {
wenzelm@55560
   128
      case dockable: Symbols_Dockable => Some(dockable)
wenzelm@50208
   129
      case _ => None
wenzelm@50208
   130
    }
wenzelm@50208
   131
wenzelm@55560
   132
  def syslog_dockable(view: View): Option[Syslog_Dockable] =
wenzelm@55560
   133
    wm(view).getDockableWindow("isabelle-syslog") match {
wenzelm@55560
   134
      case dockable: Syslog_Dockable => Some(dockable)
wenzelm@55560
   135
      case _ => None
wenzelm@55560
   136
    }
wenzelm@55560
   137
wenzelm@55560
   138
  def theories_dockable(view: View): Option[Theories_Dockable] =
wenzelm@55560
   139
    wm(view).getDockableWindow("isabelle-theories") match {
wenzelm@55560
   140
      case dockable: Theories_Dockable => Some(dockable)
wenzelm@55560
   141
      case _ => None
wenzelm@55560
   142
    }
wenzelm@55560
   143
wenzelm@55560
   144
  def timing_dockable(view: View): Option[Timing_Dockable] =
wenzelm@55560
   145
    wm(view).getDockableWindow("isabelle-timing") match {
wenzelm@55560
   146
      case dockable: Timing_Dockable => Some(dockable)
wenzelm@50433
   147
      case _ => None
wenzelm@50433
   148
    }
wenzelm@50433
   149
wenzelm@50208
   150
wenzelm@52815
   151
  /* continuous checking */
wenzelm@52815
   152
wenzelm@52815
   153
  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
wenzelm@52815
   154
wenzelm@52815
   155
  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
wenzelm@52815
   156
wenzelm@52815
   157
  def continuous_checking_=(b: Boolean)
wenzelm@52815
   158
  {
wenzelm@57612
   159
    GUI_Thread.require {}
wenzelm@52815
   160
wenzelm@52815
   161
    if (continuous_checking != b) {
wenzelm@52815
   162
      PIDE.options.bool(CONTINUOUS_CHECKING) = b
wenzelm@52815
   163
      PIDE.options_changed()
wenzelm@52974
   164
      PIDE.editor.flush()
wenzelm@52815
   165
    }
wenzelm@52815
   166
  }
wenzelm@52815
   167
wenzelm@52815
   168
  def set_continuous_checking() { continuous_checking = true }
wenzelm@52815
   169
  def reset_continuous_checking() { continuous_checking = false }
wenzelm@52815
   170
  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
wenzelm@52815
   171
wenzelm@53715
   172
  class Continuous_Checking extends CheckBox("Continuous checking")
wenzelm@53715
   173
  {
wenzelm@53715
   174
    tooltip = "Continuous checking of proof document (visible and required parts)"
wenzelm@53715
   175
    reactions += { case ButtonClicked(_) => continuous_checking = selected }
wenzelm@53715
   176
    def load() { selected = continuous_checking }
wenzelm@53715
   177
    load()
wenzelm@53715
   178
  }
wenzelm@53715
   179
wenzelm@52815
   180
wenzelm@52815
   181
  /* required document nodes */
wenzelm@52815
   182
wenzelm@52815
   183
  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
wenzelm@52815
   184
  {
wenzelm@57612
   185
    GUI_Thread.require {}
wenzelm@52815
   186
    PIDE.document_model(view.getBuffer) match {
wenzelm@52815
   187
      case Some(model) =>
wenzelm@52816
   188
        model.node_required = (if (toggle) !model.node_required else set)
wenzelm@52815
   189
      case None =>
wenzelm@52815
   190
    }
wenzelm@52815
   191
  }
wenzelm@52815
   192
wenzelm@52815
   193
  def set_node_required(view: View) { node_required_update(view, set = true) }
wenzelm@52815
   194
  def reset_node_required(view: View) { node_required_update(view, set = false) }
wenzelm@52815
   195
  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
wenzelm@52815
   196
wenzelm@52815
   197
wenzelm@50198
   198
  /* font size */
wenzelm@50198
   199
wenzelm@55827
   200
  def reset_font_size() {
wenzelm@55827
   201
    Font_Info.main_change.reset(PIDE.options.int("jedit_reset_font_size").toFloat)
wenzelm@55823
   202
  }
wenzelm@55827
   203
  def increase_font_size() { Font_Info.main_change.step(1) }
wenzelm@55827
   204
  def decrease_font_size() { Font_Info.main_change.step(-1) }
wenzelm@50198
   205
wenzelm@50198
   206
wenzelm@53497
   207
  /* structured edits */
wenzelm@50341
   208
wenzelm@50341
   209
  def insert_line_padding(text_area: JEditTextArea, text: String)
wenzelm@50341
   210
  {
wenzelm@50341
   211
    val buffer = text_area.getBuffer
wenzelm@50341
   212
    JEdit_Lib.buffer_edit(buffer) {
wenzelm@50341
   213
      val text1 =
wenzelm@50341
   214
        if (text_area.getSelectionCount == 0) {
wenzelm@50341
   215
          def pad(range: Text.Range): String =
wenzelm@50341
   216
            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
wenzelm@50341
   217
wenzelm@56592
   218
          val caret = JEdit_Lib.caret_range(text_area)
wenzelm@50341
   219
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
wenzelm@50341
   220
          pad(before_caret) + text + pad(caret)
wenzelm@50341
   221
        }
wenzelm@50341
   222
        else text
wenzelm@50341
   223
      text_area.setSelectedText(text1)
wenzelm@50341
   224
    }
wenzelm@50341
   225
  }
wenzelm@50341
   226
wenzelm@53497
   227
  def edit_command(
wenzelm@53497
   228
    snapshot: Document.Snapshot,
wenzelm@53497
   229
    buffer: Buffer,
wenzelm@53497
   230
    padding: Boolean,
wenzelm@54640
   231
    id: Document_ID.Generic,
wenzelm@53497
   232
    s: String)
wenzelm@53497
   233
  {
wenzelm@54640
   234
    if (!snapshot.is_outdated) {
wenzelm@57861
   235
      (snapshot.state.find_command(snapshot.version, id), PIDE.document_model(buffer)) match {
wenzelm@57861
   236
        case (Some((node, command)), Some(model)) if command.node_name == model.node_name =>
wenzelm@54640
   237
          node.command_start(command) match {
wenzelm@54640
   238
            case Some(start) =>
wenzelm@54640
   239
              JEdit_Lib.buffer_edit(buffer) {
wenzelm@54640
   240
                val range = command.proper_range + start
wenzelm@54640
   241
                if (padding) {
wenzelm@54640
   242
                  buffer.insert(start + range.length, "\n" + s)
wenzelm@54640
   243
                }
wenzelm@54640
   244
                else {
wenzelm@54640
   245
                  buffer.remove(start, range.length)
wenzelm@54640
   246
                  buffer.insert(start, s)
wenzelm@54640
   247
                }
wenzelm@53497
   248
              }
wenzelm@54640
   249
            case None =>
wenzelm@54640
   250
          }
wenzelm@57861
   251
        case _ =>
wenzelm@54640
   252
      }
wenzelm@53497
   253
    }
wenzelm@53497
   254
  }
wenzelm@53497
   255
wenzelm@50341
   256
wenzelm@53293
   257
  /* completion */
wenzelm@53293
   258
wenzelm@56586
   259
  def complete(view: View, word_only: Boolean)
wenzelm@53293
   260
  {
wenzelm@57424
   261
    Completion_Popup.Text_Area.action(view.getTextArea, word_only)
wenzelm@53293
   262
  }
wenzelm@53293
   263
wenzelm@53293
   264
wenzelm@50183
   265
  /* control styles */
wenzelm@50183
   266
wenzelm@50183
   267
  def control_sub(text_area: JEditTextArea)
wenzelm@50187
   268
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
   269
wenzelm@50183
   270
  def control_sup(text_area: JEditTextArea)
wenzelm@50187
   271
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
   272
wenzelm@50183
   273
  def control_bold(text_area: JEditTextArea)
wenzelm@50187
   274
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
   275
wenzelm@50183
   276
  def control_reset(text_area: JEditTextArea)
wenzelm@50187
   277
  { Token_Markup.edit_control_style(text_area, "") }
wenzelm@50183
   278
wenzelm@50183
   279
wenzelm@50183
   280
  /* block styles */
wenzelm@50183
   281
wenzelm@50183
   282
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
   283
  {
wenzelm@50183
   284
    s1.foreach(text_area.userInput(_))
wenzelm@50183
   285
    s2.foreach(text_area.userInput(_))
wenzelm@50183
   286
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
   287
  }
wenzelm@50183
   288
wenzelm@50183
   289
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
   290
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
   291
wenzelm@50183
   292
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
   293
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@56574
   294
wenzelm@56574
   295
wenzelm@56574
   296
  /* spell-checker dictionary */
wenzelm@56574
   297
wenzelm@56574
   298
  def update_dictionary(text_area: JEditTextArea, include: Boolean, permanent: Boolean)
wenzelm@56574
   299
  {
wenzelm@56574
   300
    for {
wenzelm@56574
   301
      spell_checker <- PIDE.spell_checker.get
wenzelm@56574
   302
      doc_view <- PIDE.document_view(text_area)
wenzelm@56576
   303
      rendering = doc_view.get_rendering()
wenzelm@56592
   304
      range = JEdit_Lib.caret_range(text_area)
wenzelm@56576
   305
      Text.Info(_, word) <- Spell_Checker.current_word(text_area, rendering, range)
wenzelm@56575
   306
    } {
wenzelm@56575
   307
      spell_checker.update(word, include, permanent)
wenzelm@56575
   308
      JEdit_Lib.jedit_views().foreach(_.repaint())
wenzelm@56575
   309
    }
wenzelm@56574
   310
  }
wenzelm@56574
   311
wenzelm@56578
   312
  def reset_dictionary()
wenzelm@56575
   313
  {
wenzelm@56575
   314
    for (spell_checker <- PIDE.spell_checker.get)
wenzelm@56575
   315
    {
wenzelm@56575
   316
      spell_checker.reset()
wenzelm@56575
   317
      JEdit_Lib.jedit_views().foreach(_.repaint())
wenzelm@56575
   318
    }
wenzelm@56575
   319
  }
wenzelm@57627
   320
wenzelm@57627
   321
wenzelm@57627
   322
  /* plugin options */
wenzelm@57627
   323
wenzelm@57627
   324
  def plugin_options(frame: Frame)
wenzelm@57627
   325
  {
wenzelm@57627
   326
    GUI_Thread.require {}
wenzelm@57627
   327
    new org.gjt.sp.jedit.options.PluginOptions(frame, "plugin.isabelle.jedit.Plugin")
wenzelm@57627
   328
  }
wenzelm@50183
   329
}
wenzelm@50183
   330