src/Tools/jEdit/src/isabelle.scala
author wenzelm
Mon Aug 12 12:06:48 2013 +0200 (2013-08-12)
changeset 52974 908e8a36e975
parent 52816 c608e0ade554
child 53021 d0fa3f446b9d
permissions -rw-r--r--
tuned signature;
wenzelm@50208
     1
/*  Title:      Tools/jEdit/src/isabelle.scala
wenzelm@50183
     2
    Author:     Makarius
wenzelm@50183
     3
wenzelm@50208
     4
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@50208
    19
  /* dockable windows */
wenzelm@50208
    20
wenzelm@50208
    21
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
wenzelm@50208
    22
wenzelm@50299
    23
  def docked_theories(view: View): Option[Theories_Dockable] =
wenzelm@50299
    24
    wm(view).getDockableWindow("isabelle-theories") match {
wenzelm@50299
    25
      case dockable: Theories_Dockable => Some(dockable)
wenzelm@50208
    26
      case _ => None
wenzelm@50208
    27
    }
wenzelm@50208
    28
wenzelm@51533
    29
  def docked_timing(view: View): Option[Timing_Dockable] =
wenzelm@51533
    30
    wm(view).getDockableWindow("isabelle-timing") match {
wenzelm@51533
    31
      case dockable: Timing_Dockable => Some(dockable)
wenzelm@51533
    32
      case _ => None
wenzelm@51533
    33
    }
wenzelm@51533
    34
wenzelm@50208
    35
  def docked_output(view: View): Option[Output_Dockable] =
wenzelm@50208
    36
    wm(view).getDockableWindow("isabelle-output") match {
wenzelm@50208
    37
      case dockable: Output_Dockable => Some(dockable)
wenzelm@50208
    38
      case _ => None
wenzelm@50208
    39
    }
wenzelm@50208
    40
wenzelm@50208
    41
  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
wenzelm@50208
    42
    wm(view).getDockableWindow("isabelle-raw-output") match {
wenzelm@50208
    43
      case dockable: Raw_Output_Dockable => Some(dockable)
wenzelm@50208
    44
      case _ => None
wenzelm@50208
    45
    }
wenzelm@50208
    46
wenzelm@50208
    47
  def docked_protocol(view: View): Option[Protocol_Dockable] =
wenzelm@50208
    48
    wm(view).getDockableWindow("isabelle-protocol") match {
wenzelm@50208
    49
      case dockable: Protocol_Dockable => Some(dockable)
wenzelm@50208
    50
      case _ => None
wenzelm@50208
    51
    }
wenzelm@50208
    52
wenzelm@50433
    53
  def docked_monitor(view: View): Option[Monitor_Dockable] =
wenzelm@50433
    54
    wm(view).getDockableWindow("isabelle-monitor") match {
wenzelm@50433
    55
      case dockable: Monitor_Dockable => Some(dockable)
wenzelm@50433
    56
      case _ => None
wenzelm@50433
    57
    }
wenzelm@50433
    58
wenzelm@50208
    59
wenzelm@52815
    60
  /* continuous checking */
wenzelm@52815
    61
wenzelm@52815
    62
  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
wenzelm@52815
    63
wenzelm@52815
    64
  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
wenzelm@52815
    65
wenzelm@52815
    66
  def continuous_checking_=(b: Boolean)
wenzelm@52815
    67
  {
wenzelm@52815
    68
    Swing_Thread.require()
wenzelm@52815
    69
wenzelm@52815
    70
    if (continuous_checking != b) {
wenzelm@52815
    71
      PIDE.options.bool(CONTINUOUS_CHECKING) = b
wenzelm@52815
    72
      PIDE.options_changed()
wenzelm@52974
    73
      PIDE.editor.flush()
wenzelm@52815
    74
    }
wenzelm@52815
    75
  }
wenzelm@52815
    76
wenzelm@52815
    77
  def set_continuous_checking() { continuous_checking = true }
wenzelm@52815
    78
  def reset_continuous_checking() { continuous_checking = false }
wenzelm@52815
    79
  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
wenzelm@52815
    80
wenzelm@52815
    81
wenzelm@52815
    82
  /* required document nodes */
wenzelm@52815
    83
wenzelm@52815
    84
  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
wenzelm@52815
    85
  {
wenzelm@52815
    86
    Swing_Thread.require()
wenzelm@52815
    87
    PIDE.document_model(view.getBuffer) match {
wenzelm@52815
    88
      case Some(model) =>
wenzelm@52816
    89
        model.node_required = (if (toggle) !model.node_required else set)
wenzelm@52815
    90
      case None =>
wenzelm@52815
    91
    }
wenzelm@52815
    92
  }
wenzelm@52815
    93
wenzelm@52815
    94
  def set_node_required(view: View) { node_required_update(view, set = true) }
wenzelm@52815
    95
  def reset_node_required(view: View) { node_required_update(view, set = false) }
wenzelm@52815
    96
  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
wenzelm@52815
    97
wenzelm@52815
    98
wenzelm@50198
    99
  /* font size */
wenzelm@50198
   100
wenzelm@50198
   101
  def change_font_size(view: View, change: Int => Int)
wenzelm@50198
   102
  {
wenzelm@50775
   103
    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
wenzelm@50206
   104
    jEdit.setIntegerProperty("view.fontsize", size)
wenzelm@50198
   105
    jEdit.propertiesChanged()
wenzelm@50198
   106
    jEdit.saveSettings()
wenzelm@50198
   107
    view.getStatus.setMessageAndClear("Text font size: " + size)
wenzelm@50198
   108
  }
wenzelm@50198
   109
wenzelm@50198
   110
  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
wenzelm@50198
   111
  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
wenzelm@50198
   112
wenzelm@50198
   113
wenzelm@50341
   114
  /* structured insert */
wenzelm@50341
   115
wenzelm@50341
   116
  def insert_line_padding(text_area: JEditTextArea, text: String)
wenzelm@50341
   117
  {
wenzelm@50341
   118
    val buffer = text_area.getBuffer
wenzelm@50341
   119
    JEdit_Lib.buffer_edit(buffer) {
wenzelm@50341
   120
      val text1 =
wenzelm@50341
   121
        if (text_area.getSelectionCount == 0) {
wenzelm@50341
   122
          def pad(range: Text.Range): String =
wenzelm@50341
   123
            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
wenzelm@50341
   124
wenzelm@50341
   125
          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
wenzelm@50341
   126
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
wenzelm@50341
   127
          pad(before_caret) + text + pad(caret)
wenzelm@50341
   128
        }
wenzelm@50341
   129
        else text
wenzelm@50341
   130
      text_area.setSelectedText(text1)
wenzelm@50341
   131
    }
wenzelm@50341
   132
  }
wenzelm@50341
   133
wenzelm@50341
   134
wenzelm@50183
   135
  /* control styles */
wenzelm@50183
   136
wenzelm@50183
   137
  def control_sub(text_area: JEditTextArea)
wenzelm@50187
   138
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
wenzelm@50183
   139
wenzelm@50183
   140
  def control_sup(text_area: JEditTextArea)
wenzelm@50187
   141
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
wenzelm@50183
   142
wenzelm@50183
   143
  def control_isub(text_area: JEditTextArea)
wenzelm@50187
   144
  { Token_Markup.edit_control_style(text_area, Symbol.isub_decoded) }
wenzelm@50183
   145
wenzelm@50183
   146
  def control_isup(text_area: JEditTextArea)
wenzelm@50187
   147
  { Token_Markup.edit_control_style(text_area, Symbol.isup_decoded) }
wenzelm@50183
   148
wenzelm@50183
   149
  def control_bold(text_area: JEditTextArea)
wenzelm@50187
   150
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
wenzelm@50183
   151
wenzelm@50183
   152
  def control_reset(text_area: JEditTextArea)
wenzelm@50187
   153
  { Token_Markup.edit_control_style(text_area, "") }
wenzelm@50183
   154
wenzelm@50183
   155
wenzelm@50183
   156
  /* block styles */
wenzelm@50183
   157
wenzelm@50183
   158
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
wenzelm@50183
   159
  {
wenzelm@50183
   160
    s1.foreach(text_area.userInput(_))
wenzelm@50183
   161
    s2.foreach(text_area.userInput(_))
wenzelm@50183
   162
    s2.foreach(_ => text_area.goToPrevCharacter(false))
wenzelm@50183
   163
  }
wenzelm@50183
   164
wenzelm@50183
   165
  def input_bsub(text_area: JEditTextArea)
wenzelm@50183
   166
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
wenzelm@50183
   167
wenzelm@50183
   168
  def input_bsup(text_area: JEditTextArea)
wenzelm@50183
   169
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
wenzelm@50183
   170
}
wenzelm@50183
   171