src/Tools/jEdit/src/syntax_style.scala
author wenzelm
Wed, 23 Jul 2025 14:53:21 +0200
changeset 82898 89da4dcd1fa8
parent 80441 c420429fdf4c
permissions -rw-r--r--
clarified colors, following d6a14ed060fb;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/syntax_style.scala
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     3
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     4
Support for extended syntax styles: subscript, superscript, bold, user fonts.
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     5
*/
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     6
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     8
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
     9
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    10
import isabelle._
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    11
73909
1d0d9772fff0 tuned imports;
wenzelm
parents: 73340
diff changeset
    12
import java.util.{Map => JMap}
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    13
import java.awt.{Font, Color}
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    14
import java.awt.font.TextAttribute
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    15
import java.awt.geom.AffineTransform
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    16
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    17
import org.gjt.sp.util.SyntaxUtilities
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    18
import org.gjt.sp.jedit.jEdit
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    19
import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
    20
import org.gjt.sp.jedit.textarea.TextArea
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    21
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    22
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
    23
object Syntax_Style {
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
    24
  /* extended syntax styles */
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
    25
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    26
  private val plain_range: Int = JEditToken.ID_COUNT
73995
de82b1251971 more robust (see 4d91b6d5d49c);
wenzelm
parents: 73987
diff changeset
    27
  private val full_range: Int = 6 * plain_range
73340
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
    28
  private def check_range(i: Int): Unit =
0ffcad1f6130 tuned --- fewer warnings;
wenzelm
parents: 73120
diff changeset
    29
    require(0 <= i && i < plain_range, "bad syntax style range")
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    30
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    31
  def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    32
  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    33
  def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    34
  def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
73995
de82b1251971 more robust (see 4d91b6d5d49c);
wenzelm
parents: 73987
diff changeset
    35
  val hidden: Byte = full_range.toByte
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
    36
  val control: Byte = (hidden + JEditToken.DIGIT).toByte
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    37
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    38
  private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    39
    new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    40
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
    41
  private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = {
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    42
    font_style(style, { font0 =>
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    43
      val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i)))
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    44
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    45
      def shift(y: Float): Font =
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    46
        GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    47
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    48
      val m0 = GUI.line_metrics(font0)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    49
      val m1 = GUI.line_metrics(font1)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    50
      val a = m1.getAscent - m0.getAscent
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    51
      val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    52
      if (a > 0.0f) shift(a)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    53
      else if (b > 0.0f) shift(- b)
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    54
      else font1
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
    55
    })
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    56
  }
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    57
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    58
  private def bold_style(style: SyntaxStyle): SyntaxStyle =
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    59
    font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD))
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    60
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    61
  val hidden_color: Color = new Color(255, 255, 255, 0)
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    62
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
    63
  def set_extender(extender: SyntaxUtilities.StyleExtender): Unit = {
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    64
    SyntaxUtilities.setStyleExtender(extender)
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    65
    GUI_Thread.later { jEdit.propertiesChanged }
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    66
  }
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    67
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
    68
  object Base_Extender extends SyntaxUtilities.StyleExtender {
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
    69
    override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = {
78243
0e221a8128e4 tuned: prefer Scala over Java;
wenzelm
parents: 75659
diff changeset
    70
      val new_styles = Array.fill[SyntaxStyle](Byte.MaxValue)(styles(0))
73987
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    71
      for (i <- 0 until full_range) {
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    72
        new_styles(i) = styles(i % plain_range)
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    73
      }
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    74
      new_styles
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    75
    }
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    76
  }
fc363a3b690a build.props for isabelle.jar, including isabelle.jedit;
wenzelm
parents: 73909
diff changeset
    77
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
    78
  object Main_Extender extends SyntaxUtilities.StyleExtender {
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    79
    val max_user_fonts = 2
75195
596e77cda169 clarified signature;
wenzelm
parents: 73997
diff changeset
    80
    if (Symbol.symbols.font_names.length > max_user_fonts)
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    81
      error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
75195
596e77cda169 clarified signature;
wenzelm
parents: 73997
diff changeset
    82
        Symbol.symbols.font_names.mkString(", "))
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    83
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
    84
    override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = {
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
    85
      val style0 = styles(0)
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
    86
      val font0 = style0.getFont
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
    87
78243
0e221a8128e4 tuned: prefer Scala over Java;
wenzelm
parents: 75659
diff changeset
    88
      val new_styles = Array.fill[SyntaxStyle](Byte.MaxValue)(styles(0))
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    89
      for (i <- 0 until plain_range) {
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    90
        val style = styles(i)
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    91
        new_styles(i) = style
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    92
        new_styles(subscript(i.toByte)) = script_style(style, -1)
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    93
        new_styles(superscript(i.toByte)) = script_style(style, 1)
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    94
        new_styles(bold(i.toByte)) = bold_style(style)
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    95
        for (idx <- 0 until max_user_fonts)
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    96
          new_styles(user_font(idx, i.toByte)) = style
75195
596e77cda169 clarified signature;
wenzelm
parents: 73997
diff changeset
    97
        for ((family, idx) <- Symbol.symbols.font_index)
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    98
          new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
    99
      }
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   100
      new_styles(hidden) =
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   101
        new SyntaxStyle(hidden_color, null,
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   102
          GUI.transform_font(new Font(font0.getFamily, 0, 1),
70124
af4f723823d8 visible hairline for cursor, even on OpenJDK 11 (amending 2fd73a1a0937);
wenzelm
parents: 69969
diff changeset
   103
            AffineTransform.getScaleInstance(2.0, font0.getSize.toDouble)))
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   104
      new_styles(control) =
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   105
        new SyntaxStyle(style0.getForegroundColor, style0.getBackgroundColor,
75659
9bd92ac9328f more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents: 75394
diff changeset
   106
          {
9bd92ac9328f more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents: 75394
diff changeset
   107
            val font_style =
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   108
              (if (font0.isItalic) 0 else Font.ITALIC) |
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   109
              (if (font0.isBold) 0 else Font.BOLD)
75659
9bd92ac9328f more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents: 75394
diff changeset
   110
            new Font(font0.getFamily, font_style, font0.getSize)
9bd92ac9328f more robust Scala 3 indentation, for the sake of IntelliJ IDEA;
wenzelm
parents: 75394
diff changeset
   111
          })
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   112
      new_styles
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   113
    }
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   114
  }
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   115
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   116
  private def control_style(sym: String): Option[Byte => Byte] =
71601
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71381
diff changeset
   117
    if (sym == Symbol.sub_decoded) Some(subscript)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71381
diff changeset
   118
    else if (sym == Symbol.sup_decoded) Some(superscript)
97ccf48c2f0c misc tuning based on hints by IntelliJ IDEA;
wenzelm
parents: 71381
diff changeset
   119
    else if (sym == Symbol.bold_decoded) Some(bold)
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   120
    else None
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   121
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
   122
  def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] = {
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   123
    var result = Map[Text.Offset, Byte => Byte]()
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
   124
    def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte): Unit = {
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   125
      for (i <- start until stop) result += (i -> style)
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   126
    }
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   127
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   128
    var offset = 0
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   129
    var control_sym = ""
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   130
    for (sym <- Symbol.iterator(text)) {
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   131
      val end_offset = offset + sym.length
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   132
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   133
      if (control_style(sym).isDefined) control_sym = sym
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   134
      else if (control_sym != "") {
75195
596e77cda169 clarified signature;
wenzelm
parents: 73997
diff changeset
   135
        if (Symbol.is_controllable(sym) && !Symbol.symbols.fonts.isDefinedAt(sym)) {
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   136
          mark(offset - control_sym.length, offset, _ => hidden)
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   137
          mark(offset, end_offset, control_style(control_sym).get)
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   138
        }
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   139
        control_sym = ""
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   140
      }
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   141
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   142
      if (Symbol.is_control_encoded(sym)) {
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   143
        val a = offset + Symbol.control_prefix.length
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   144
        val b = end_offset - Symbol.control_suffix.length
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   145
        mark(offset, a, _ => hidden)
67128
4d91b6d5d49c clarified control style;
wenzelm
parents: 67127
diff changeset
   146
        mark(a, b, _ => control)
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   147
        mark(b, end_offset, _ => hidden)
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   148
      }
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   149
75195
596e77cda169 clarified signature;
wenzelm
parents: 73997
diff changeset
   150
      Symbol.symbols.lookup_font(sym) match {
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   151
        case Some(idx) => mark(offset, end_offset, user_font(idx, _))
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   152
        case _ =>
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   153
      }
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   154
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   155
      offset = end_offset
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   156
    }
67127
cf111622c9f8 font style for literal control symbols, notably for antiquotations;
wenzelm
parents: 67125
diff changeset
   157
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   158
    result
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   159
  }
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   160
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   161
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   162
  /* editing support for control symbols */
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   163
75393
87ebf5a50283 clarified formatting, for the sake of scala3;
wenzelm
parents: 75195
diff changeset
   164
  def edit_control_style(text_area: TextArea, control_sym: String): Unit = {
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   165
    GUI_Thread.assert {}
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   166
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   167
    val buffer = text_area.getBuffer
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   168
69969
wenzelm
parents: 67130
diff changeset
   169
    val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control_sym)
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   170
80441
wenzelm
parents: 78243
diff changeset
   171
    def update_style(text: String): String =
wenzelm
parents: 78243
diff changeset
   172
      Library.string_builder() { result =>
wenzelm
parents: 78243
diff changeset
   173
        for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) {
wenzelm
parents: 78243
diff changeset
   174
          if (Symbol.is_controllable(sym)) result ++= control_decoded
wenzelm
parents: 78243
diff changeset
   175
          result ++= sym
wenzelm
parents: 78243
diff changeset
   176
        }
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   177
      }
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   178
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   179
    text_area.getSelection.foreach { sel =>
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   180
      val before = JEdit_Lib.point_range(buffer, sel.getStart - 1)
67014
e6a695d6a6b2 tuned signature;
wenzelm
parents: 66006
diff changeset
   181
      JEdit_Lib.get_text(buffer, before) match {
65997
e3dc9ea67a62 output control symbols like ML version, with optionally hidden source;
wenzelm
parents: 65265
diff changeset
   182
        case Some(s) if HTML.is_control(s) =>
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   183
          text_area.extendSelection(before.start, before.stop)
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   184
        case _ =>
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   185
      }
75394
42267c650205 tuned formatting;
wenzelm
parents: 75393
diff changeset
   186
    }
65259
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   187
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   188
    text_area.getSelection.toList match {
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   189
      case Nil =>
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   190
        text_area.setSelectedText(control_decoded)
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   191
      case sels =>
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   192
        JEdit_Lib.buffer_edit(buffer) {
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   193
          sels.foreach(sel =>
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   194
            text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel))))
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   195
        }
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   196
    }
41d12227d5dc clarified modules;
wenzelm
parents: 65258
diff changeset
   197
  }
65258
a0701669d159 clarified modules;
wenzelm
parents:
diff changeset
   198
}