src/Tools/jEdit/src/isabelle.scala
author wenzelm
Sat, 01 Mar 2014 18:33:49 +0100
changeset 55824 22bc50a19afa
parent 55823 0331b6d2ab0c
child 55825 694833e3e4a0
permissions -rw-r--r--
tuned;
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
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
     4
Global configuration and 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
53715
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
    12
import scala.swing.CheckBox
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
    13
import scala.swing.event.ButtonClicked
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
    14
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
    15
import org.gjt.sp.jedit.{jEdit, View, Buffer}
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    16
import org.gjt.sp.jedit.textarea.JEditTextArea
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
    17
import org.gjt.sp.jedit.gui.{DockableWindowManager, CompleteWord}
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    18
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    19
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    20
object Isabelle
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
    21
{
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    22
  /* editor modes */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    23
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    24
  val modes =
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    25
    List(
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    26
      "isabelle",         // theory source
55500
cdbbaa3074a8 isabelle-ml mode with separate token marker;
wenzelm
parents: 55316
diff changeset
    27
      "isabelle-ml",      // ML source
53281
251e1a2aa792 clarified SideKick parser name, which serves as quasi "mode" here;
wenzelm
parents: 53280
diff changeset
    28
      "isabelle-markup",  // SideKick markup tree
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    29
      "isabelle-news",    // NEWS
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    30
      "isabelle-options", // etc/options
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    31
      "isabelle-output",  // pretty text area output
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    32
      "isabelle-root")    // session ROOT
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    33
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    34
  private lazy val ml_syntax: Outer_Syntax =
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    35
    Outer_Syntax.init().no_tokens.
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55666
diff changeset
    36
      set_language_context(Completion.Language_Context.ML_outer)
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    37
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    38
  private lazy val news_syntax: Outer_Syntax =
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    39
    Outer_Syntax.init().no_tokens
53276
cbed0aa0b0db syntax for isabelle-news with symbol completion;
wenzelm
parents: 53274
diff changeset
    40
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    41
  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
    42
    name match {
53281
251e1a2aa792 clarified SideKick parser name, which serves as quasi "mode" here;
wenzelm
parents: 53280
diff changeset
    43
      case "isabelle" | "isabelle-markup" =>
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    44
        val syntax = PIDE.session.recent_syntax
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    45
        if (syntax == Outer_Syntax.empty) None else Some(syntax)
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    46
      case "isabelle-options" => Some(Options.options_syntax)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    47
      case "isabelle-root" => Some(Build.root_syntax)
55616
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    48
      case "isabelle-ml" => Some(ml_syntax)
25a7a998852a default completion context via outer syntax;
wenzelm
parents: 55558
diff changeset
    49
      case "isabelle-news" => Some(news_syntax)
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    50
      case "isabelle-output" => None
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    51
      case _ => None
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    52
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    53
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53272
diff changeset
    54
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    55
  /* token markers */
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    56
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    57
  private val markers =
53280
c63a016805b9 explicit indication of outer syntax with no tokens;
wenzelm
parents: 53277
diff changeset
    58
    Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*)
53277
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    59
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    60
  def token_marker(name: String): Option[Token_Markup.Marker] = markers.get(name)
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    61
6aa348237973 more uniform configuration of editor modes and token markers;
wenzelm
parents: 53276
diff changeset
    62
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    63
  /* dockable windows */
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    64
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    65
  private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    66
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    67
  def documentation_dockable(view: View): Option[Documentation_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    68
    wm(view).getDockableWindow("isabelle-documentation") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    69
      case dockable: Documentation_Dockable => Some(dockable)
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    70
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    71
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    72
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    73
  def find_dockable(view: View): Option[Find_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    74
    wm(view).getDockableWindow("isabelle-find") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    75
      case dockable: Find_Dockable => Some(dockable)
51533
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    76
      case _ => None
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    77
    }
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 50775
diff changeset
    78
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    79
  def monitor_dockable(view: View): Option[Monitor_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    80
    wm(view).getDockableWindow("isabelle-monitor") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    81
      case dockable: Monitor_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    82
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    83
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    84
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    85
  def output_dockable(view: View): Option[Output_Dockable] =
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    86
    wm(view).getDockableWindow("isabelle-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    87
      case dockable: Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    88
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    89
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    90
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    91
  def protocol_dockable(view: View): Option[Protocol_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    92
    wm(view).getDockableWindow("isabelle-protocol") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    93
      case dockable: Protocol_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    94
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    95
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    96
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
    97
  def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    98
    wm(view).getDockableWindow("isabelle-raw-output") match {
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
    99
      case dockable: Raw_Output_Dockable => Some(dockable)
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   100
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   101
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   102
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   103
  def simplifier_trace_dockable(view: View): Option[Simplifier_Trace_Dockable] =
55557
aa1adeca714b standardized action and panel names;
wenzelm
parents: 55500
diff changeset
   104
    wm(view).getDockableWindow("isabelle-simplifier-trace") match {
55316
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
   105
      case dockable: Simplifier_Trace_Dockable => Some(dockable)
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
   106
      case _ => None
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
   107
    }
885500f4aa6a interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
Lars Hupel <lars.hupel@mytum.de>
parents: 54640
diff changeset
   108
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   109
  def sledgehammer_dockable(view: View): Option[Sledgehammer_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   110
    wm(view).getDockableWindow("isabelle-sledgehammer") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   111
      case dockable: Sledgehammer_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   112
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   113
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   114
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   115
  def symbols_dockable(view: View): Option[Symbols_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   116
    wm(view).getDockableWindow("isabelle-symbols") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   117
      case dockable: Symbols_Dockable => Some(dockable)
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   118
      case _ => None
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   119
    }
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   120
55558
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   121
  def syslog_dockable(view: View): Option[Syslog_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   122
    wm(view).getDockableWindow("isabelle-syslog") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   123
      case dockable: Syslog_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   124
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   125
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   126
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   127
  def theories_dockable(view: View): Option[Theories_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   128
    wm(view).getDockableWindow("isabelle-theories") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   129
      case dockable: Theories_Dockable => Some(dockable)
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   130
      case _ => None
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   131
    }
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   132
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   133
  def timing_dockable(view: View): Option[Timing_Dockable] =
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   134
    wm(view).getDockableWindow("isabelle-timing") match {
298274c970b6 more uniform treatment of dockables and their standard actions;
wenzelm
parents: 55557
diff changeset
   135
      case dockable: Timing_Dockable => Some(dockable)
50433
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   136
      case _ => None
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   137
    }
9131dadb2bf7 basic monitor panel, using the powerful jfreechart library;
wenzelm
parents: 50341
diff changeset
   138
50208
1382ad6d4774 tuned signature;
wenzelm
parents: 50206
diff changeset
   139
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   140
  /* continuous checking */
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   141
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   142
  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
   143
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   144
  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
   145
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   146
  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
   147
  {
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   148
    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
   149
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   150
    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
   151
      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
   152
      PIDE.options_changed()
52974
908e8a36e975 tuned signature;
wenzelm
parents: 52816
diff changeset
   153
      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
   154
    }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   155
  }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   156
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   157
  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
   158
  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
   159
  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
   160
53715
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   161
  class Continuous_Checking extends CheckBox("Continuous checking")
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   162
  {
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   163
    tooltip = "Continuous checking of proof document (visible and required parts)"
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   164
    reactions += { case ButtonClicked(_) => continuous_checking = selected }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   165
    def load() { selected = continuous_checking }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   166
    load()
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   167
  }
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53497
diff changeset
   168
52815
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   169
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   170
  /* 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
   171
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   172
  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
   173
  {
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   174
    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
   175
    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
   176
      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
   177
        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
   178
      case None =>
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   179
    }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   180
  }
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   181
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   182
  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
   183
  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
   184
  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
   185
eaad5fe7bb1b actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents: 51533
diff changeset
   186
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   187
  /* font size */
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   188
55823
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   189
  private object font_size
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   190
  {
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   191
    // owned by Swing thread
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   192
    private var steps = 0
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   193
    private val delay = Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay"))
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   194
    {
55824
wenzelm
parents: 55823
diff changeset
   195
      Rendering.font_size_change(i =>
55823
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   196
        {
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   197
          var j = i
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   198
          while (steps != 0 && j > 0) {
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   199
            if (steps > 0)
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   200
              { j += (j / 10) max 1; steps -= 1 }
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   201
            else
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   202
              { j -= (j / 10) max 1; steps += 1 }
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   203
          }
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   204
          steps = 0
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   205
          j
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   206
        })
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   207
    }
55824
wenzelm
parents: 55823
diff changeset
   208
    def step(i: Int) { steps += i; delay.invoke() }
wenzelm
parents: 55823
diff changeset
   209
    def reset() { delay.revoke(); steps = 0 }
55823
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   210
  }
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   211
55824
wenzelm
parents: 55823
diff changeset
   212
  def reset_font_size()
55823
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   213
  {
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   214
    font_size.reset()
55824
wenzelm
parents: 55823
diff changeset
   215
    Rendering.font_size_change(_ => PIDE.options.int("jedit_reset_font_size"))
55823
0331b6d2ab0c font size change with delay, to avoid GUI lagging behind user input;
wenzelm
parents: 55749
diff changeset
   216
  }
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53161
diff changeset
   217
55824
wenzelm
parents: 55823
diff changeset
   218
  def increase_font_size() { font_size.step(1) }
wenzelm
parents: 55823
diff changeset
   219
  def decrease_font_size() { font_size.step(-1) }
50198
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   220
0c7b351a6871 added convenience actions isabelle.increase-font-size and isabelle.decrease-font-size;
wenzelm
parents: 50187
diff changeset
   221
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   222
  /* structured edits */
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   223
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   224
  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
   225
  {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   226
    val buffer = text_area.getBuffer
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   227
    JEdit_Lib.buffer_edit(buffer) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   228
      val text1 =
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   229
        if (text_area.getSelectionCount == 0) {
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   230
          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
   231
            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
   232
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   233
          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
   234
          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
   235
          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
   236
        }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   237
        else text
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   238
      text_area.setSelectedText(text1)
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   239
    }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   240
  }
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   241
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   242
  def edit_command(
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   243
    snapshot: Document.Snapshot,
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   244
    buffer: Buffer,
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   245
    padding: Boolean,
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   246
    id: Document_ID.Generic,
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   247
    s: String)
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   248
  {
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   249
    if (!snapshot.is_outdated) {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   250
      snapshot.state.find_command(snapshot.version, id) match {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   251
        case Some((node, command)) =>
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   252
          node.command_start(command) match {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   253
            case Some(start) =>
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   254
              JEdit_Lib.buffer_edit(buffer) {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   255
                val range = command.proper_range + start
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   256
                if (padding) {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   257
                  buffer.insert(start + range.length, "\n" + s)
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   258
                }
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   259
                else {
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   260
                  buffer.remove(start, range.length)
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   261
                  buffer.insert(start, s)
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   262
                }
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   263
              }
54640
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   264
            case None =>
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   265
          }
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   266
        case None =>
bbd2fa353809 back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
wenzelm
parents: 53843
diff changeset
   267
      }
53497
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   268
    }
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   269
  }
07bb77881b8d tuned signature;
wenzelm
parents: 53322
diff changeset
   270
50341
0c65a7cfc0f3 provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
wenzelm
parents: 50299
diff changeset
   271
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   272
  /* completion */
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   273
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   274
  def complete(view: View)
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   275
  {
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   276
    Completion_Popup.Text_Area(view.getTextArea) match {
53322
a4cd032172e0 allow short words for explicit completion;
wenzelm
parents: 53293
diff changeset
   277
      case Some(text_area_completion) =>
a4cd032172e0 allow short words for explicit completion;
wenzelm
parents: 53293
diff changeset
   278
        text_area_completion.action(immediate = true, explicit = true)
53293
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   279
      case None => CompleteWord.completeWord(view)
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   280
    }
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   281
  }
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   282
fd27b8f5a479 added action isabelle.complete, using standard jEdit keyboard shortcut;
wenzelm
parents: 53281
diff changeset
   283
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   284
  /* control styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   285
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   286
  def control_sub(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   287
  { Token_Markup.edit_control_style(text_area, Symbol.sub_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   288
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   289
  def control_sup(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   290
  { Token_Markup.edit_control_style(text_area, Symbol.sup_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   291
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   292
  def control_bold(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   293
  { Token_Markup.edit_control_style(text_area, Symbol.bold_decoded) }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   294
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   295
  def control_reset(text_area: JEditTextArea)
50187
b5a09812abc4 special handling of control symbols in Symbols dockable;
wenzelm
parents: 50183
diff changeset
   296
  { Token_Markup.edit_control_style(text_area, "") }
50183
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   297
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   298
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   299
  /* block styles */
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   300
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   301
  private def enclose_input(text_area: JEditTextArea, s1: String, s2: String)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   302
  {
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   303
    s1.foreach(text_area.userInput(_))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   304
    s2.foreach(text_area.userInput(_))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   305
    s2.foreach(_ => text_area.goToPrevCharacter(false))
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   306
  }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   307
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   308
  def input_bsub(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   309
  { enclose_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   310
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   311
  def input_bsup(text_area: JEditTextArea)
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   312
  { enclose_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) }
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   313
}
2b3e24e1c9e7 improved editing support for control styles;
wenzelm
parents:
diff changeset
   314