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