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