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