src/Tools/jEdit/src/isabelle.scala
author wenzelm
Wed Sep 18 20:09:26 2013 +0200 (2013-09-18)
changeset 53715 68c664737d04
parent 53497 07bb77881b8d
child 53843 88c6e630c15f
permissions -rw-r--r--
added option "jedit_auto_load";
allow in-place change of option "editor_continuous_checking";
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@53281
    27
      "isabelle-markup",  // SideKick markup tree
wenzelm@53277
    28
      "isabelle-news",    // NEWS
wenzelm@53277
    29
      "isabelle-options", // etc/options
wenzelm@53277
    30
      "isabelle-output",  // pretty text area output
wenzelm@53277
    31
      "isabelle-root")    // session ROOT
wenzelm@53274
    32
wenzelm@53280
    33
  private lazy val news_syntax = Outer_Syntax.init().no_tokens
wenzelm@53276
    34
wenzelm@53274
    35
  def mode_syntax(name: String): Option[Outer_Syntax] =
wenzelm@53274
    36
    name match {
wenzelm@53281
    37
      case "isabelle" | "isabelle-markup" =>
wenzelm@53277
    38
        val syntax = PIDE.session.recent_syntax
wenzelm@53277
    39
        if (syntax == Outer_Syntax.empty) None else Some(syntax)
wenzelm@53274
    40
      case "isabelle-options" => Some(Options.options_syntax)
wenzelm@53274
    41
      case "isabelle-root" => Some(Build.root_syntax)
wenzelm@53276
    42
      case "isabelle-news" => Some(news_syntax)
wenzelm@53277
    43
      case "isabelle-output" => None
wenzelm@53274
    44
      case _ => None
wenzelm@53274
    45
    }
wenzelm@53274
    46
wenzelm@53274
    47
wenzelm@53277
    48
  /* token markers */
wenzelm@53277
    49
wenzelm@53277
    50
  private val markers =
wenzelm@53280
    51
    Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
wenzelm@53277
    52
wenzelm@53277
    53
  def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
wenzelm@53277
    54
wenzelm@53277
    55
wenzelm@50208
    56
  /* dockable windows */
wenzelm@50208
    57
wenzelm@50208
    58
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
wenzelm@50208
    59
wenzelm@50299
    60
  def docked_theories(view: View): Option[Theories_Dockable] =
wenzelm@50299
    61
    wm(view).getDockableWindow("isabelle-theories") match {
wenzelm@50299
    62
      case dockable: Theories_Dockable => Some(dockable)
wenzelm@50208
    63
      case _ => None
wenzelm@50208
    64
    }
wenzelm@50208
    65
wenzelm@51533
    66
  def docked_timing(view: View): Option[Timing_Dockable] =
wenzelm@51533
    67
    wm(view).getDockableWindow("isabelle-timing") match {
wenzelm@51533
    68
      case dockable: Timing_Dockable => Some(dockable)
wenzelm@51533
    69
      case _ => None
wenzelm@51533
    70
    }
wenzelm@51533
    71
wenzelm@50208
    72
  def docked_output(view: View): Option[Output_Dockable] =
wenzelm@50208
    73
    wm(view).getDockableWindow("isabelle-output") match {
wenzelm@50208
    74
      case dockable: Output_Dockable => Some(dockable)
wenzelm@50208
    75
      case _ => None
wenzelm@50208
    76
    }
wenzelm@50208
    77
wenzelm@50208
    78
  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
wenzelm@50208
    79
    wm(view).getDockableWindow("isabelle-raw-output") match {
wenzelm@50208
    80
      case dockable: Raw_Output_Dockable => Some(dockable)
wenzelm@50208
    81
      case _ => None
wenzelm@50208
    82
    }
wenzelm@50208
    83
wenzelm@50208
    84
  def docked_protocol(view: View): Option[Protocol_Dockable] =
wenzelm@50208
    85
    wm(view).getDockableWindow("isabelle-protocol") match {
wenzelm@50208
    86
      case dockable: Protocol_Dockable => Some(dockable)
wenzelm@50208
    87
      case _ => None
wenzelm@50208
    88
    }
wenzelm@50208
    89
wenzelm@50433
    90
  def docked_monitor(view: View): Option[Monitor_Dockable] =
wenzelm@50433
    91
    wm(view).getDockableWindow("isabelle-monitor") match {
wenzelm@50433
    92
      case dockable: Monitor_Dockable => Some(dockable)
wenzelm@50433
    93
      case _ => None
wenzelm@50433
    94
    }
wenzelm@50433
    95
wenzelm@50208
    96
wenzelm@52815
    97
  /* continuous checking */
wenzelm@52815
    98
wenzelm@52815
    99
  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
wenzelm@52815
   100
wenzelm@52815
   101
  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
wenzelm@52815
   102
wenzelm@52815
   103
  def continuous_checking_=(b: Boolean)
wenzelm@52815
   104
  {
wenzelm@52815
   105
    Swing_Thread.require()
wenzelm@52815
   106
wenzelm@52815
   107
    if (continuous_checking != b) {
wenzelm@52815
   108
      PIDE.options.bool(CONTINUOUS_CHECKING) = b
wenzelm@52815
   109
      PIDE.options_changed()
wenzelm@52974
   110
      PIDE.editor.flush()
wenzelm@52815
   111
    }
wenzelm@52815
   112
  }
wenzelm@52815
   113
wenzelm@52815
   114
  def set_continuous_checking() { continuous_checking = true }
wenzelm@52815
   115
  def reset_continuous_checking() { continuous_checking = false }
wenzelm@52815
   116
  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
wenzelm@52815
   117
wenzelm@53715
   118
  class Continuous_Checking extends CheckBox("Continuous checking")
wenzelm@53715
   119
  {
wenzelm@53715
   120
    tooltip = "Continuous checking of proof document (visible and required parts)"
wenzelm@53715
   121
    reactions += { case ButtonClicked(_) => continuous_checking = selected }
wenzelm@53715
   122
    def load() { selected = continuous_checking }
wenzelm@53715
   123
    load()
wenzelm@53715
   124
  }
wenzelm@53715
   125
wenzelm@52815
   126
wenzelm@52815
   127
  /* required document nodes */
wenzelm@52815
   128
wenzelm@52815
   129
  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
wenzelm@52815
   130
  {
wenzelm@52815
   131
    Swing_Thread.require()
wenzelm@52815
   132
    PIDE.document_model(view.getBuffer) match {
wenzelm@52815
   133
      case Some(model) =>
wenzelm@52816
   134
        model.node_required = (if (toggle) !model.node_required else set)
wenzelm@52815
   135
      case None =>
wenzelm@52815
   136
    }
wenzelm@52815
   137
  }
wenzelm@52815
   138
wenzelm@52815
   139
  def set_node_required(view: View) { node_required_update(view, set = true) }
wenzelm@52815
   140
  def reset_node_required(view: View) { node_required_update(view, set = false) }
wenzelm@52815
   141
  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
wenzelm@52815
   142
wenzelm@52815
   143
wenzelm@50198
   144
  /* font size */
wenzelm@50198
   145
wenzelm@53272
   146
  def reset_font_size(view: View): Unit =
wenzelm@53272
   147
    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
wenzelm@50198
   148
wenzelm@53272
   149
  def increase_font_size(view: View): Unit =
wenzelm@53272
   150
    Rendering.font_size_change(view, i => i + ((i / 10) max 1))
wenzelm@53272
   151
wenzelm@53272
   152
  def decrease_font_size(view: View): Unit =
wenzelm@53272
   153
    Rendering.font_size_change(view, i => i - ((i / 10) max 1))
wenzelm@50198
   154
wenzelm@50198
   155
wenzelm@53497
   156
  /* structured edits */
wenzelm@50341
   157
wenzelm@50341
   158
  def insert_line_padding(text_area: JEditTextArea, text: String)
wenzelm@50341
   159
  {
wenzelm@50341
   160
    val buffer = text_area.getBuffer
wenzelm@50341
   161
    JEdit_Lib.buffer_edit(buffer) {
wenzelm@50341
   162
      val text1 =
wenzelm@50341
   163
        if (text_area.getSelectionCount == 0) {
wenzelm@50341
   164
          def pad(range: Text.Range): String =
wenzelm@50341
   165
            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
wenzelm@50341
   166
wenzelm@50341
   167
          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
wenzelm@50341
   168
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
wenzelm@50341
   169
          pad(before_caret) + text + pad(caret)
wenzelm@50341
   170
        }
wenzelm@50341
   171
        else text
wenzelm@50341
   172
      text_area.setSelectedText(text1)
wenzelm@50341
   173
    }
wenzelm@50341
   174
  }
wenzelm@50341
   175
wenzelm@53497
   176
  def edit_command(
wenzelm@53497
   177
    snapshot: Document.Snapshot,
wenzelm@53497
   178
    buffer: Buffer,
wenzelm@53497
   179
    padding: Boolean,
wenzelm@53497
   180
    exec_id: Document_ID.Exec,
wenzelm@53497
   181
    s: String)
wenzelm@53497
   182
  {
wenzelm@53497
   183
    snapshot.state.execs.get(exec_id).map(_.command) match {
wenzelm@53497
   184
      case Some(command) =>
wenzelm@53497
   185
        snapshot.node.command_start(command) match {
wenzelm@53497
   186
          case Some(start) =>
wenzelm@53497
   187
            JEdit_Lib.buffer_edit(buffer) {
wenzelm@53497
   188
              val range = command.proper_range + start
wenzelm@53497
   189
              if (padding) {
wenzelm@53497
   190
                val pad =
wenzelm@53497
   191
                  JEdit_Lib.try_get_text(buffer, Text.Range(range.length - 1, range.length))
wenzelm@53497
   192
                    match {
wenzelm@53497
   193
                      case None => ""
wenzelm@53497
   194
                      case Some(s) => if (Symbol.is_blank(s)) "" else " "
wenzelm@53497
   195
                    }
wenzelm@53497
   196
                buffer.insert(start + range.length, pad + s)
wenzelm@53497
   197
              }
wenzelm@53497
   198
              else {
wenzelm@53497
   199
                buffer.remove(start, range.length)
wenzelm@53497
   200
                buffer.insert(start, s)
wenzelm@53497
   201
              }
wenzelm@53497
   202
            }
wenzelm@53497
   203
          case None =>
wenzelm@53497
   204
        }
wenzelm@53497
   205
      case None =>
wenzelm@53497
   206
    }
wenzelm@53497
   207
  }
wenzelm@53497
   208
wenzelm@50341
   209
wenzelm@53293
   210
  /* completion */
wenzelm@53293
   211
wenzelm@53293
   212
  def complete(view: View)
wenzelm@53293
   213
  {
wenzelm@53293
   214
    Completion_Popup.Text_Area(view.getTextArea) match {
wenzelm@53322
   215
      case Some(text_area_completion) =>
wenzelm@53322
   216
        text_area_completion.action(immediate = true, explicit = true)
wenzelm@53293
   217
      case None => CompleteWord.completeWord(view)
wenzelm@53293
   218
    }
wenzelm@53293
   219
  }
wenzelm@53293
   220
wenzelm@53293
   221
wenzelm@50183
   222
  /* control styles */
wenzelm@50183
   223
wenzelm@50183
   224
  def control_sub(text_area: JEditTextArea)
wenzelm@50187
   225
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
   226
wenzelm@50183
   227
  def control_sup(text_area: JEditTextArea)
wenzelm@50187
   228
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
   229
wenzelm@50183
   230
  def control_bold(text_area: JEditTextArea)
wenzelm@50187
   231
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
   232
wenzelm@50183
   233
  def control_reset(text_area: JEditTextArea)
wenzelm@50187
   234
  { Token_Markup.edit_control_style(text_area, "") }
wenzelm@50183
   235
wenzelm@50183
   236
wenzelm@50183
   237
  /* block styles */
wenzelm@50183
   238
wenzelm@50183
   239
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
   240
  {
wenzelm@50183
   241
    s1.foreach(text_area.userInput(_))
wenzelm@50183
   242
    s2.foreach(text_area.userInput(_))
wenzelm@50183
   243
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
   244
  }
wenzelm@50183
   245
wenzelm@50183
   246
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
   247
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
   248
wenzelm@50183
   249
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
   250
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@50183
   251
}
wenzelm@50183
   252