src/Tools/jEdit/src/isabelle.scala
author wenzelm
Thu Aug 29 15:53:56 2013 +0200 (2013-08-29)
changeset 53281 251e1a2aa792
parent 53280 c63a016805b9
child 53293 fd27b8f5a479
permissions -rw-r--r--
clarified SideKick parser name, which serves as quasi "mode" here;
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@50198
    12
import org.gjt.sp.jedit.{jEdit, View, Buffer}
wenzelm@50183
    13
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@50208
    14
import org.gjt.sp.jedit.gui.DockableWindowManager
wenzelm@50183
    15
wenzelm@50183
    16
wenzelm@50208
    17
object Isabelle
wenzelm@50183
    18
{
wenzelm@53274
    19
  /* editor modes */
wenzelm@53274
    20
wenzelm@53277
    21
  val modes =
wenzelm@53277
    22
    List(
wenzelm@53277
    23
      "isabelle",         // theory source
wenzelm@53281
    24
      "isabelle-markup",  // SideKick markup tree
wenzelm@53277
    25
      "isabelle-news",    // NEWS
wenzelm@53277
    26
      "isabelle-options", // etc/options
wenzelm@53277
    27
      "isabelle-output",  // pretty text area output
wenzelm@53277
    28
      "isabelle-root")    // session ROOT
wenzelm@53274
    29
wenzelm@53280
    30
  private lazy val news_syntax = Outer_Syntax.init().no_tokens
wenzelm@53276
    31
wenzelm@53274
    32
  def mode_syntax(name: String): Option[Outer_Syntax] =
wenzelm@53274
    33
    name match {
wenzelm@53281
    34
      case "isabelle" | "isabelle-markup" =>
wenzelm@53277
    35
        val syntax = PIDE.session.recent_syntax
wenzelm@53277
    36
        if (syntax == Outer_Syntax.empty) None else Some(syntax)
wenzelm@53274
    37
      case "isabelle-options" => Some(Options.options_syntax)
wenzelm@53274
    38
      case "isabelle-root" => Some(Build.root_syntax)
wenzelm@53276
    39
      case "isabelle-news" => Some(news_syntax)
wenzelm@53277
    40
      case "isabelle-output" => None
wenzelm@53274
    41
      case _ => None
wenzelm@53274
    42
    }
wenzelm@53274
    43
wenzelm@53274
    44
wenzelm@53277
    45
  /* token markers */
wenzelm@53277
    46
wenzelm@53277
    47
  private val markers =
wenzelm@53280
    48
    Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
wenzelm@53277
    49
wenzelm@53277
    50
  def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
wenzelm@53277
    51
wenzelm@53277
    52
wenzelm@50208
    53
  /* dockable windows */
wenzelm@50208
    54
wenzelm@50208
    55
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
wenzelm@50208
    56
wenzelm@50299
    57
  def docked_theories(view: View): Option[Theories_Dockable] =
wenzelm@50299
    58
    wm(view).getDockableWindow("isabelle-theories") match {
wenzelm@50299
    59
      case dockable: Theories_Dockable => Some(dockable)
wenzelm@50208
    60
      case _ => None
wenzelm@50208
    61
    }
wenzelm@50208
    62
wenzelm@51533
    63
  def docked_timing(view: View): Option[Timing_Dockable] =
wenzelm@51533
    64
    wm(view).getDockableWindow("isabelle-timing") match {
wenzelm@51533
    65
      case dockable: Timing_Dockable => Some(dockable)
wenzelm@51533
    66
      case _ => None
wenzelm@51533
    67
    }
wenzelm@51533
    68
wenzelm@50208
    69
  def docked_output(view: View): Option[Output_Dockable] =
wenzelm@50208
    70
    wm(view).getDockableWindow("isabelle-output") match {
wenzelm@50208
    71
      case dockable: Output_Dockable => Some(dockable)
wenzelm@50208
    72
      case _ => None
wenzelm@50208
    73
    }
wenzelm@50208
    74
wenzelm@50208
    75
  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
wenzelm@50208
    76
    wm(view).getDockableWindow("isabelle-raw-output") match {
wenzelm@50208
    77
      case dockable: Raw_Output_Dockable => Some(dockable)
wenzelm@50208
    78
      case _ => None
wenzelm@50208
    79
    }
wenzelm@50208
    80
wenzelm@50208
    81
  def docked_protocol(view: View): Option[Protocol_Dockable] =
wenzelm@50208
    82
    wm(view).getDockableWindow("isabelle-protocol") match {
wenzelm@50208
    83
      case dockable: Protocol_Dockable => Some(dockable)
wenzelm@50208
    84
      case _ => None
wenzelm@50208
    85
    }
wenzelm@50208
    86
wenzelm@50433
    87
  def docked_monitor(view: View): Option[Monitor_Dockable] =
wenzelm@50433
    88
    wm(view).getDockableWindow("isabelle-monitor") match {
wenzelm@50433
    89
      case dockable: Monitor_Dockable => Some(dockable)
wenzelm@50433
    90
      case _ => None
wenzelm@50433
    91
    }
wenzelm@50433
    92
wenzelm@50208
    93
wenzelm@52815
    94
  /* continuous checking */
wenzelm@52815
    95
wenzelm@52815
    96
  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
wenzelm@52815
    97
wenzelm@52815
    98
  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
wenzelm@52815
    99
wenzelm@52815
   100
  def continuous_checking_=(b: Boolean)
wenzelm@52815
   101
  {
wenzelm@52815
   102
    Swing_Thread.require()
wenzelm@52815
   103
wenzelm@52815
   104
    if (continuous_checking != b) {
wenzelm@52815
   105
      PIDE.options.bool(CONTINUOUS_CHECKING) = b
wenzelm@52815
   106
      PIDE.options_changed()
wenzelm@52974
   107
      PIDE.editor.flush()
wenzelm@52815
   108
    }
wenzelm@52815
   109
  }
wenzelm@52815
   110
wenzelm@52815
   111
  def set_continuous_checking() { continuous_checking = true }
wenzelm@52815
   112
  def reset_continuous_checking() { continuous_checking = false }
wenzelm@52815
   113
  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
wenzelm@52815
   114
wenzelm@52815
   115
wenzelm@52815
   116
  /* required document nodes */
wenzelm@52815
   117
wenzelm@52815
   118
  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
wenzelm@52815
   119
  {
wenzelm@52815
   120
    Swing_Thread.require()
wenzelm@52815
   121
    PIDE.document_model(view.getBuffer) match {
wenzelm@52815
   122
      case Some(model) =>
wenzelm@52816
   123
        model.node_required = (if (toggle) !model.node_required else set)
wenzelm@52815
   124
      case None =>
wenzelm@52815
   125
    }
wenzelm@52815
   126
  }
wenzelm@52815
   127
wenzelm@52815
   128
  def set_node_required(view: View) { node_required_update(view, set = true) }
wenzelm@52815
   129
  def reset_node_required(view: View) { node_required_update(view, set = false) }
wenzelm@52815
   130
  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
wenzelm@52815
   131
wenzelm@52815
   132
wenzelm@50198
   133
  /* font size */
wenzelm@50198
   134
wenzelm@53272
   135
  def reset_font_size(view: View): Unit =
wenzelm@53272
   136
    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
wenzelm@50198
   137
wenzelm@53272
   138
  def increase_font_size(view: View): Unit =
wenzelm@53272
   139
    Rendering.font_size_change(view, i => i + ((i / 10) max 1))
wenzelm@53272
   140
wenzelm@53272
   141
  def decrease_font_size(view: View): Unit =
wenzelm@53272
   142
    Rendering.font_size_change(view, i => i - ((i / 10) max 1))
wenzelm@50198
   143
wenzelm@50198
   144
wenzelm@50341
   145
  /* structured insert */
wenzelm@50341
   146
wenzelm@50341
   147
  def insert_line_padding(text_area: JEditTextArea, text: String)
wenzelm@50341
   148
  {
wenzelm@50341
   149
    val buffer = text_area.getBuffer
wenzelm@50341
   150
    JEdit_Lib.buffer_edit(buffer) {
wenzelm@50341
   151
      val text1 =
wenzelm@50341
   152
        if (text_area.getSelectionCount == 0) {
wenzelm@50341
   153
          def pad(range: Text.Range): String =
wenzelm@50341
   154
            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
wenzelm@50341
   155
wenzelm@50341
   156
          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
wenzelm@50341
   157
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
wenzelm@50341
   158
          pad(before_caret) + text + pad(caret)
wenzelm@50341
   159
        }
wenzelm@50341
   160
        else text
wenzelm@50341
   161
      text_area.setSelectedText(text1)
wenzelm@50341
   162
    }
wenzelm@50341
   163
  }
wenzelm@50341
   164
wenzelm@50341
   165
wenzelm@50183
   166
  /* control styles */
wenzelm@50183
   167
wenzelm@50183
   168
  def control_sub(text_area: JEditTextArea)
wenzelm@50187
   169
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
   170
wenzelm@50183
   171
  def control_sup(text_area: JEditTextArea)
wenzelm@50187
   172
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
   173
wenzelm@50183
   174
  def control_bold(text_area: JEditTextArea)
wenzelm@50187
   175
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
   176
wenzelm@50183
   177
  def control_reset(text_area: JEditTextArea)
wenzelm@50187
   178
  { Token_Markup.edit_control_style(text_area, "") }
wenzelm@50183
   179
wenzelm@50183
   180
wenzelm@50183
   181
  /* block styles */
wenzelm@50183
   182
wenzelm@50183
   183
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
   184
  {
wenzelm@50183
   185
    s1.foreach(text_area.userInput(_))
wenzelm@50183
   186
    s2.foreach(text_area.userInput(_))
wenzelm@50183
   187
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
   188
  }
wenzelm@50183
   189
wenzelm@50183
   190
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
   191
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
   192
wenzelm@50183
   193
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
   194
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@50183
   195
}
wenzelm@50183
   196