src/Tools/jEdit/src/isabelle.scala
author wenzelm
Sat Mar 01 16:34:30 2014 +0100 (2014-03-01 ago)
changeset 55823 0331b6d2ab0c
parent 55749 75a48dc4383e
child 55824 22bc50a19afa
permissions -rw-r--r--
font size change with delay, to avoid GUI lagging behind user input;
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@53277
    32
      "isabelle-root")    // session ROOT
wenzelm@53274
    33
wenzelm@55616
    34
  private lazy val ml_syntax: Outer_Syntax =
wenzelm@55616
    35
    Outer_Syntax.init().no_tokens.
wenzelm@55749
    36
      set_language_context(Completion.Language_Context.ML_outer)
wenzelm@55616
    37
wenzelm@55616
    38
  private lazy val news_syntax: Outer_Syntax =
wenzelm@55616
    39
    Outer_Syntax.init().no_tokens
wenzelm@53276
    40
wenzelm@53274
    41
  def mode_syntax(name: String): Option[Outer_Syntax] =
wenzelm@53274
    42
    name match {
wenzelm@53281
    43
      case "isabelle" | "isabelle-markup" =>
wenzelm@53277
    44
        val syntax = PIDE.session.recent_syntax
wenzelm@53277
    45
        if (syntax == Outer_Syntax.empty) None else Some(syntax)
wenzelm@53274
    46
      case "isabelle-options" => Some(Options.options_syntax)
wenzelm@53274
    47
      case "isabelle-root" => Some(Build.root_syntax)
wenzelm@55616
    48
      case "isabelle-ml" => Some(ml_syntax)
wenzelm@55616
    49
      case "isabelle-news" => Some(news_syntax)
wenzelm@53277
    50
      case "isabelle-output" => None
wenzelm@53274
    51
      case _ => None
wenzelm@53274
    52
    }
wenzelm@53274
    53
wenzelm@53274
    54
wenzelm@53277
    55
  /* token markers */
wenzelm@53277
    56
wenzelm@53277
    57
  private val markers =
wenzelm@53280
    58
    Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
wenzelm@53277
    59
wenzelm@53277
    60
  def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
wenzelm@53277
    61
wenzelm@53277
    62
wenzelm@50208
    63
  /* dockable windows */
wenzelm@50208
    64
wenzelm@50208
    65
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
wenzelm@50208
    66
wenzelm@55560
    67
  def documentation_dockable(view: View): Option[Documentation_Dockable] =
wenzelm@55560
    68
    wm(view).getDockableWindow("isabelle-documentation") match {
wenzelm@55560
    69
      case dockable: Documentation_Dockable => Some(dockable)
wenzelm@50208
    70
      case _ => None
wenzelm@50208
    71
    }
wenzelm@50208
    72
wenzelm@55560
    73
  def find_dockable(view: View): Option[Find_Dockable] =
wenzelm@55560
    74
    wm(view).getDockableWindow("isabelle-find") match {
wenzelm@55560
    75
      case dockable: Find_Dockable => Some(dockable)
wenzelm@51533
    76
      case _ => None
wenzelm@51533
    77
    }
wenzelm@51533
    78
wenzelm@55560
    79
  def monitor_dockable(view: View): Option[Monitor_Dockable] =
wenzelm@55560
    80
    wm(view).getDockableWindow("isabelle-monitor") match {
wenzelm@55560
    81
      case dockable: Monitor_Dockable => Some(dockable)
wenzelm@55560
    82
      case _ => None
wenzelm@55560
    83
    }
wenzelm@55560
    84
wenzelm@55560
    85
  def output_dockable(view: View): Option[Output_Dockable] =
wenzelm@50208
    86
    wm(view).getDockableWindow("isabelle-output") match {
wenzelm@50208
    87
      case dockable: Output_Dockable => Some(dockable)
wenzelm@50208
    88
      case _ => None
wenzelm@50208
    89
    }
wenzelm@50208
    90
wenzelm@55560
    91
  def protocol_dockable(view: View): Option[Protocol_Dockable] =
wenzelm@55560
    92
    wm(view).getDockableWindow("isabelle-protocol") match {
wenzelm@55560
    93
      case dockable: Protocol_Dockable => Some(dockable)
wenzelm@55560
    94
      case _ => None
wenzelm@55560
    95
    }
wenzelm@55560
    96
wenzelm@55560
    97
  def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
wenzelm@50208
    98
    wm(view).getDockableWindow("isabelle-raw-output") match {
wenzelm@50208
    99
      case dockable: Raw_Output_Dockable => Some(dockable)
wenzelm@50208
   100
      case _ => None
wenzelm@50208
   101
    }
wenzelm@50208
   102
wenzelm@55560
   103
  def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
wenzelm@55559
   104
    wm(view).getDockableWindow("isabelle-simplifier-trace") match {
lars@55316
   105
      case dockable: Simplifier_Trace_Dockable => Some(dockable)
lars@55316
   106
      case _ => None
lars@55316
   107
    }
lars@55316
   108
wenzelm@55560
   109
  def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
wenzelm@55560
   110
    wm(view).getDockableWindow("isabelle-sledgehammer") match {
wenzelm@55560
   111
      case dockable: Sledgehammer_Dockable => Some(dockable)
wenzelm@55560
   112
      case _ => None
wenzelm@55560
   113
    }
wenzelm@55560
   114
wenzelm@55560
   115
  def symbols_dockable(view: View): Option[Symbols_Dockable] =
wenzelm@55560
   116
    wm(view).getDockableWindow("isabelle-symbols") match {
wenzelm@55560
   117
      case dockable: Symbols_Dockable => Some(dockable)
wenzelm@50208
   118
      case _ => None
wenzelm@50208
   119
    }
wenzelm@50208
   120
wenzelm@55560
   121
  def syslog_dockable(view: View): Option[Syslog_Dockable] =
wenzelm@55560
   122
    wm(view).getDockableWindow("isabelle-syslog") match {
wenzelm@55560
   123
      case dockable: Syslog_Dockable => Some(dockable)
wenzelm@55560
   124
      case _ => None
wenzelm@55560
   125
    }
wenzelm@55560
   126
wenzelm@55560
   127
  def theories_dockable(view: View): Option[Theories_Dockable] =
wenzelm@55560
   128
    wm(view).getDockableWindow("isabelle-theories") match {
wenzelm@55560
   129
      case dockable: Theories_Dockable => Some(dockable)
wenzelm@55560
   130
      case _ => None
wenzelm@55560
   131
    }
wenzelm@55560
   132
wenzelm@55560
   133
  def timing_dockable(view: View): Option[Timing_Dockable] =
wenzelm@55560
   134
    wm(view).getDockableWindow("isabelle-timing") match {
wenzelm@55560
   135
      case dockable: Timing_Dockable => Some(dockable)
wenzelm@50433
   136
      case _ => None
wenzelm@50433
   137
    }
wenzelm@50433
   138
wenzelm@50208
   139
wenzelm@52815
   140
  /* continuous checking */
wenzelm@52815
   141
wenzelm@52815
   142
  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
wenzelm@52815
   143
wenzelm@52815
   144
  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
wenzelm@52815
   145
wenzelm@52815
   146
  def continuous_checking_=(b: Boolean)
wenzelm@52815
   147
  {
wenzelm@52815
   148
    Swing_Thread.require()
wenzelm@52815
   149
wenzelm@52815
   150
    if (continuous_checking != b) {
wenzelm@52815
   151
      PIDE.options.bool(CONTINUOUS_CHECKING) = b
wenzelm@52815
   152
      PIDE.options_changed()
wenzelm@52974
   153
      PIDE.editor.flush()
wenzelm@52815
   154
    }
wenzelm@52815
   155
  }
wenzelm@52815
   156
wenzelm@52815
   157
  def set_continuous_checking() { continuous_checking = true }
wenzelm@52815
   158
  def reset_continuous_checking() { continuous_checking = false }
wenzelm@52815
   159
  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
wenzelm@52815
   160
wenzelm@53715
   161
  class Continuous_Checking extends CheckBox("Continuous checking")
wenzelm@53715
   162
  {
wenzelm@53715
   163
    tooltip = "Continuous checking of proof document (visible and required parts)"
wenzelm@53715
   164
    reactions += { case ButtonClicked(_) => continuous_checking = selected }
wenzelm@53715
   165
    def load() { selected = continuous_checking }
wenzelm@53715
   166
    load()
wenzelm@53715
   167
  }
wenzelm@53715
   168
wenzelm@52815
   169
wenzelm@52815
   170
  /* required document nodes */
wenzelm@52815
   171
wenzelm@52815
   172
  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
wenzelm@52815
   173
  {
wenzelm@52815
   174
    Swing_Thread.require()
wenzelm@52815
   175
    PIDE.document_model(view.getBuffer) match {
wenzelm@52815
   176
      case Some(model) =>
wenzelm@52816
   177
        model.node_required = (if (toggle) !model.node_required else set)
wenzelm@52815
   178
      case None =>
wenzelm@52815
   179
    }
wenzelm@52815
   180
  }
wenzelm@52815
   181
wenzelm@52815
   182
  def set_node_required(view: View) { node_required_update(view, set = true) }
wenzelm@52815
   183
  def reset_node_required(view: View) { node_required_update(view, set = false) }
wenzelm@52815
   184
  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
wenzelm@52815
   185
wenzelm@52815
   186
wenzelm@50198
   187
  /* font size */
wenzelm@50198
   188
wenzelm@55823
   189
  private object font_size
wenzelm@55823
   190
  {
wenzelm@55823
   191
    // owned by Swing thread
wenzelm@55823
   192
    private var last_view: Option[View] = None
wenzelm@55823
   193
    private var steps = 0
wenzelm@55823
   194
    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
wenzelm@55823
   195
    {
wenzelm@55823
   196
      val view = last_view getOrElse jEdit.getActiveView()
wenzelm@55823
   197
      Rendering.font_size_change(view, i =>
wenzelm@55823
   198
        {
wenzelm@55823
   199
          var j = i
wenzelm@55823
   200
          while (steps != 0 && j > 0) {
wenzelm@55823
   201
            if (steps > 0)
wenzelm@55823
   202
              { j += (j / 10) max 1; steps -= 1 }
wenzelm@55823
   203
            else
wenzelm@55823
   204
              { j -= (j / 10) max 1; steps += 1 }
wenzelm@55823
   205
          }
wenzelm@55823
   206
          steps = 0
wenzelm@55823
   207
          j
wenzelm@55823
   208
        })
wenzelm@55823
   209
    }
wenzelm@55823
   210
    def step(view: View, i: Int) { last_view = Some(view); steps += i; delay.invoke() }
wenzelm@55823
   211
    def reset() { delay.revoke(); last_view = None; steps = 0 }
wenzelm@55823
   212
  }
wenzelm@50198
   213
wenzelm@55823
   214
  def reset_font_size(view: View): Unit =
wenzelm@55823
   215
  {
wenzelm@55823
   216
    font_size.reset()
wenzelm@55823
   217
    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
wenzelm@55823
   218
  }
wenzelm@53272
   219
wenzelm@55823
   220
  def increase_font_size(view: View): Unit = font_size.step(view, 1)
wenzelm@55823
   221
  def decrease_font_size(view: View): Unit = font_size.step(view, -1)
wenzelm@50198
   222
wenzelm@50198
   223
wenzelm@53497
   224
  /* structured edits */
wenzelm@50341
   225
wenzelm@50341
   226
  def insert_line_padding(text_area: JEditTextArea, text: String)
wenzelm@50341
   227
  {
wenzelm@50341
   228
    val buffer = text_area.getBuffer
wenzelm@50341
   229
    JEdit_Lib.buffer_edit(buffer) {
wenzelm@50341
   230
      val text1 =
wenzelm@50341
   231
        if (text_area.getSelectionCount == 0) {
wenzelm@50341
   232
          def pad(range: Text.Range): String =
wenzelm@50341
   233
            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
wenzelm@50341
   234
wenzelm@50341
   235
          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
wenzelm@50341
   236
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
wenzelm@50341
   237
          pad(before_caret) + text + pad(caret)
wenzelm@50341
   238
        }
wenzelm@50341
   239
        else text
wenzelm@50341
   240
      text_area.setSelectedText(text1)
wenzelm@50341
   241
    }
wenzelm@50341
   242
  }
wenzelm@50341
   243
wenzelm@53497
   244
  def edit_command(
wenzelm@53497
   245
    snapshot: Document.Snapshot,
wenzelm@53497
   246
    buffer: Buffer,
wenzelm@53497
   247
    padding: Boolean,
wenzelm@54640
   248
    id: Document_ID.Generic,
wenzelm@53497
   249
    s: String)
wenzelm@53497
   250
  {
wenzelm@54640
   251
    if (!snapshot.is_outdated) {
wenzelm@54640
   252
      snapshot.state.find_command(snapshot.version, id) match {
wenzelm@54640
   253
        case Some((node, command)) =>
wenzelm@54640
   254
          node.command_start(command) match {
wenzelm@54640
   255
            case Some(start) =>
wenzelm@54640
   256
              JEdit_Lib.buffer_edit(buffer) {
wenzelm@54640
   257
                val range = command.proper_range + start
wenzelm@54640
   258
                if (padding) {
wenzelm@54640
   259
                  buffer.insert(start + range.length, "\n" + s)
wenzelm@54640
   260
                }
wenzelm@54640
   261
                else {
wenzelm@54640
   262
                  buffer.remove(start, range.length)
wenzelm@54640
   263
                  buffer.insert(start, s)
wenzelm@54640
   264
                }
wenzelm@53497
   265
              }
wenzelm@54640
   266
            case None =>
wenzelm@54640
   267
          }
wenzelm@54640
   268
        case None =>
wenzelm@54640
   269
      }
wenzelm@53497
   270
    }
wenzelm@53497
   271
  }
wenzelm@53497
   272
wenzelm@50341
   273
wenzelm@53293
   274
  /* completion */
wenzelm@53293
   275
wenzelm@53293
   276
  def complete(view: View)
wenzelm@53293
   277
  {
wenzelm@53293
   278
    Completion_Popup.Text_Area(view.getTextArea) match {
wenzelm@53322
   279
      case Some(text_area_completion) =>
wenzelm@53322
   280
        text_area_completion.action(immediate = true, explicit = true)
wenzelm@53293
   281
      case None => CompleteWord.completeWord(view)
wenzelm@53293
   282
    }
wenzelm@53293
   283
  }
wenzelm@53293
   284
wenzelm@53293
   285
wenzelm@50183
   286
  /* control styles */
wenzelm@50183
   287
wenzelm@50183
   288
  def control_sub(text_area: JEditTextArea)
wenzelm@50187
   289
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
   290
wenzelm@50183
   291
  def control_sup(text_area: JEditTextArea)
wenzelm@50187
   292
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
   293
wenzelm@50183
   294
  def control_bold(text_area: JEditTextArea)
wenzelm@50187
   295
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
   296
wenzelm@50183
   297
  def control_reset(text_area: JEditTextArea)
wenzelm@50187
   298
  { Token_Markup.edit_control_style(text_area, "") }
wenzelm@50183
   299
wenzelm@50183
   300
wenzelm@50183
   301
  /* block styles */
wenzelm@50183
   302
wenzelm@50183
   303
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
   304
  {
wenzelm@50183
   305
    s1.foreach(text_area.userInput(_))
wenzelm@50183
   306
    s2.foreach(text_area.userInput(_))
wenzelm@50183
   307
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
   308
  }
wenzelm@50183
   309
wenzelm@50183
   310
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
   311
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
   312
wenzelm@50183
   313
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
   314
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@50183
   315
}
wenzelm@50183
   316