src/Tools/jEdit/src/isabelle.scala
author wenzelm
Thu, 29 Aug 2013 13:14:00 +0200
changeset 53276 cbed0aa0b0db
parent 53274 1760c01f1c78
child 53277 6aa348237973
permissions -rw-r--r--
syntax for isabelle-news with symbol completion;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
     1
/*  Title:      Tools/jEdit/src/isabelle.scala
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     3
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
     4
Convenience operations for Isabelle/jEdit.
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     5
*/
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     6
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     8
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
     9
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    10
import isabelle._
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    11
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    12
import org.gjt.sp.jedit.{jEdit, View, Buffer}
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    13
import org.gjt.sp.jedit.textarea.JEditTextArea
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    14
import org.gjt.sp.jedit.gui.DockableWindowManager
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    15
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    16
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    17
object Isabelle
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    18
{
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    19
  /* editor modes */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    20
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    21
  val modes = List("isabelle", "isabelle-options", "isabelle-root", "isabelle-news")
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    22
53276
cbed0aa0b0db syntax for isabelle-news with symbol completion;
wenzelm
parents: 53274
diff changeset
    23
  private lazy val news_syntax = Outer_Syntax.init()
cbed0aa0b0db syntax for isabelle-news with symbol completion;
wenzelm
parents: 53274
diff changeset
    24
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    25
  def mode_syntax(name: String): Option[Outer_Syntax] =
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    26
    name match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    27
      case "isabelle" | "isabelle-raw" => PIDE.get_recent_syntax
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    28
      case "isabelle-options" => Some(Options.options_syntax)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    29
      case "isabelle-root" => Some(Build.root_syntax)
53276
cbed0aa0b0db syntax for isabelle-news with symbol completion;
wenzelm
parents: 53274
diff changeset
    30
      case "isabelle-news" => Some(news_syntax)
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    31
      case _ => None
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    32
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    33
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    34
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    35
  /* dockable windows */
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    36
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    37
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    38
50299
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50209
diff changeset
    39
  def docked_theories(view: View): Option[Theories_Dockable] =
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50209
diff changeset
    40
    wm(view).getDockableWindow("isabelle-theories") match {
f70b3712040f renamed dockable "Prover Session" to "Theories";
wenzelm
parents: 50209
diff changeset
    41
      case dockable: Theories_Dockable => Some(dockable)
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    42
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    43
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    44
51533
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    45
  def docked_timing(view: View): Option[Timing_Dockable] =
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    46
    wm(view).getDockableWindow("isabelle-timing") match {
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    47
      case dockable: Timing_Dockable => Some(dockable)
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    48
      case _ => None
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    49
    }
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    50
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    51
  def docked_output(view: View): Option[Output_Dockable] =
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    52
    wm(view).getDockableWindow("isabelle-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    53
      case dockable: Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    54
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    55
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    56
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    57
  def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    58
    wm(view).getDockableWindow("isabelle-raw-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    59
      case dockable: Raw_Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    60
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    61
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    62
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    63
  def docked_protocol(view: View): Option[Protocol_Dockable] =
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    64
    wm(view).getDockableWindow("isabelle-protocol") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    65
      case dockable: Protocol_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    66
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    67
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    68
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    69
  def docked_monitor(view: View): Option[Monitor_Dockable] =
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    70
    wm(view).getDockableWindow("isabelle-monitor") match {
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    71
      case dockable: Monitor_Dockable => Some(dockable)
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    72
      case _ => None
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    73
    }
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
    74
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    75
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    76
  /* continuous checking */
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    77
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    78
  private val CONTINUOUS_CHECKING = "editor_continuous_checking"
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    79
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    80
  def continuous_checking: Boolean = PIDE.options.bool(CONTINUOUS_CHECKING)
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    81
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    82
  def continuous_checking_=(b: Boolean)
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    83
  {
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    84
    Swing_Thread.require()
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    85
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    86
    if (continuous_checking != b) {
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    87
      PIDE.options.bool(CONTINUOUS_CHECKING) = b
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    88
      PIDE.options_changed()
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52816
diff changeset
    89
      PIDE.editor.flush()
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    90
    }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    91
  }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    92
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    93
  def set_continuous_checking() { continuous_checking = true }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    94
  def reset_continuous_checking() { continuous_checking = false }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    95
  def toggle_continuous_checking() { continuous_checking = !continuous_checking }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    96
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    97
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    98
  /* required document nodes */
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
    99
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   100
  private def node_required_update(view: View, toggle: Boolean = false, set: Boolean = false)
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   101
  {
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   102
    Swing_Thread.require()
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   103
    PIDE.document_model(view.getBuffer) match {
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   104
      case Some(model) =>
52816
c608e0ade554 home-grown mouse handling to pretend that the painted checkbox is actually a Swing component;
wenzelm
parents: 52815
diff changeset
   105
        model.node_required = (if (toggle) !model.node_required else set)
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   106
      case None =>
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   107
    }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   108
  }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   109
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   110
  def set_node_required(view: View) { node_required_update(view, set = true) }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   111
  def reset_node_required(view: View) { node_required_update(view, set = false) }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   112
  def toggle_node_required(view: View) { node_required_update(view, toggle = true) }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   113
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   114
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   115
  /* font size */
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   116
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53161
diff changeset
   117
  def reset_font_size(view: View): Unit =
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53161
diff changeset
   118
    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   119
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53161
diff changeset
   120
  def increase_font_size(view: View): Unit =
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53161
diff changeset
   121
    Rendering.font_size_change(view, i => i + ((i / 10) max 1))
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53161
diff changeset
   122
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53161
diff changeset
   123
  def decrease_font_size(view: View): Unit =
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53161
diff changeset
   124
    Rendering.font_size_change(view, i => i - ((i / 10) max 1))
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   125
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   126
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   127
  /* structured insert */
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   128
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   129
  def insert_line_padding(text_area: JEditTextArea, text: String)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   130
  {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   131
    val buffer = text_area.getBuffer
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   132
    JEdit_Lib.buffer_edit(buffer) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   133
      val text1 =
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   134
        if (text_area.getSelectionCount == 0) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   135
          def pad(range: Text.Range): String =
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   136
            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   137
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   138
          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   139
          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   140
          pad(before_caret) + text + pad(caret)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   141
        }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   142
        else text
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   143
      text_area.setSelectedText(text1)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   144
    }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   145
  }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   146
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   147
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   148
  /* control styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   149
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   150
  def control_sub(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   151
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   152
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   153
  def control_sup(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   154
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   155
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   156
  def control_bold(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   157
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   158
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   159
  def control_reset(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   160
  { Token_Markup.edit_control_style(text_area, "") }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   161
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   162
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   163
  /* block styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   164
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   165
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   166
  {
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   167
    s1.foreach(text_area.userInput(_))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   168
    s2.foreach(text_area.userInput(_))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   169
    s2.foreach(_ => text_area.goToPrevCharacter(false))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   170
  }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   171
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   172
  def input_bsub(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   173
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   174
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   175
  def input_bsup(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   176
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   177
}
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   178