author | wenzelm |
Wed, 23 Jul 2025 14:53:21 +0200 | |
changeset 82898 | 89da4dcd1fa8 |
parent 80441 | c420429fdf4c |
permissions | -rw-r--r-- |
65258 | 1 |
/* Title: Tools/jEdit/src/syntax_style.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Support for extended syntax styles: subscript, superscript, bold, user fonts. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
73909 | 12 |
import java.util.{Map => JMap} |
65258 | 13 |
import java.awt.{Font, Color} |
14 |
import java.awt.font.TextAttribute |
|
15 |
import java.awt.geom.AffineTransform |
|
16 |
||
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 | 19 |
import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle} |
65259 | 20 |
import org.gjt.sp.jedit.textarea.TextArea |
65258 | 21 |
|
22 |
||
75393 | 23 |
object Syntax_Style { |
65259 | 24 |
/* extended syntax styles */ |
25 |
||
65258 | 26 |
private val plain_range: Int = JEditToken.ID_COUNT |
73995 | 27 |
private val full_range: Int = 6 * plain_range |
73340 | 28 |
private def check_range(i: Int): Unit = |
29 |
require(0 <= i && i < plain_range, "bad syntax style range") |
|
65258 | 30 |
|
31 |
def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte } |
|
32 |
def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte } |
|
33 |
def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte } |
|
34 |
def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte } |
|
73995 | 35 |
val hidden: Byte = full_range.toByte |
67128 | 36 |
val control: Byte = (hidden + JEditToken.DIGIT).toByte |
65258 | 37 |
|
38 |
private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle = |
|
39 |
new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont)) |
|
40 |
||
75393 | 41 |
private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = { |
75394 | 42 |
font_style(style, { font0 => |
43 |
val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i))) |
|
65258 | 44 |
|
75394 | 45 |
def shift(y: Float): Font = |
46 |
GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble)) |
|
65258 | 47 |
|
75394 | 48 |
val m0 = GUI.line_metrics(font0) |
49 |
val m1 = GUI.line_metrics(font1) |
|
50 |
val a = m1.getAscent - m0.getAscent |
|
51 |
val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading) |
|
52 |
if (a > 0.0f) shift(a) |
|
53 |
else if (b > 0.0f) shift(- b) |
|
54 |
else font1 |
|
55 |
}) |
|
65258 | 56 |
} |
57 |
||
58 |
private def bold_style(style: SyntaxStyle): SyntaxStyle = |
|
59 |
font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD)) |
|
60 |
||
61 |
val hidden_color: Color = new Color(255, 255, 255, 0) |
|
62 |
||
75393 | 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 | 68 |
object Base_Extender extends SyntaxUtilities.StyleExtender { |
69 |
override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = { |
|
78243 | 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 | 78 |
object Main_Extender extends SyntaxUtilities.StyleExtender { |
65258 | 79 |
val max_user_fonts = 2 |
75195 | 80 |
if (Symbol.symbols.font_names.length > max_user_fonts) |
65258 | 81 |
error("Too many user symbol fonts (" + max_user_fonts + " permitted): " + |
75195 | 82 |
Symbol.symbols.font_names.mkString(", ")) |
65258 | 83 |
|
75393 | 84 |
override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] = { |
67128 | 85 |
val style0 = styles(0) |
86 |
val font0 = style0.getFont |
|
87 |
||
78243 | 88 |
val new_styles = Array.fill[SyntaxStyle](Byte.MaxValue)(styles(0)) |
65258 | 89 |
for (i <- 0 until plain_range) { |
90 |
val style = styles(i) |
|
91 |
new_styles(i) = style |
|
92 |
new_styles(subscript(i.toByte)) = script_style(style, -1) |
|
93 |
new_styles(superscript(i.toByte)) = script_style(style, 1) |
|
94 |
new_styles(bold(i.toByte)) = bold_style(style) |
|
95 |
for (idx <- 0 until max_user_fonts) |
|
96 |
new_styles(user_font(idx, i.toByte)) = style |
|
75195 | 97 |
for ((family, idx) <- Symbol.symbols.font_index) |
65258 | 98 |
new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family)) |
99 |
} |
|
100 |
new_styles(hidden) = |
|
101 |
new SyntaxStyle(hidden_color, null, |
|
67128 | 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 | 104 |
new_styles(control) = |
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 | 108 |
(if (font0.isItalic) 0 else Font.ITALIC) | |
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 | 112 |
new_styles |
113 |
} |
|
114 |
} |
|
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 | 117 |
if (sym == Symbol.sub_decoded) Some(subscript) |
118 |
else if (sym == Symbol.sup_decoded) Some(superscript) |
|
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 | 122 |
def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] = { |
65258 | 123 |
var result = Map[Text.Offset, Byte => Byte]() |
75393 | 124 |
def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte): Unit = { |
65258 | 125 |
for (i <- start until stop) result += (i -> style) |
126 |
} |
|
67127
cf111622c9f8
font style for literal control symbols, notably for antiquotations;
wenzelm
parents:
67125
diff
changeset
|
127 |
|
65258 | 128 |
var offset = 0 |
67128 | 129 |
var control_sym = "" |
65258 | 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 | 133 |
if (control_style(sym).isDefined) control_sym = sym |
134 |
else if (control_sym != "") { |
|
75195 | 135 |
if (Symbol.is_controllable(sym) && !Symbol.symbols.fonts.isDefinedAt(sym)) { |
67128 | 136 |
mark(offset - control_sym.length, offset, _ => hidden) |
137 |
mark(offset, end_offset, control_style(control_sym).get) |
|
65258 | 138 |
} |
67128 | 139 |
control_sym = "" |
65258 | 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 | 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 | 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 | 152 |
case _ => |
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 | 156 |
} |
67127
cf111622c9f8
font style for literal control symbols, notably for antiquotations;
wenzelm
parents:
67125
diff
changeset
|
157 |
|
65258 | 158 |
result |
159 |
} |
|
65259 | 160 |
|
161 |
||
162 |
/* editing support for control symbols */ |
|
163 |
||
75393 | 164 |
def edit_control_style(text_area: TextArea, control_sym: String): Unit = { |
65259 | 165 |
GUI_Thread.assert {} |
166 |
||
167 |
val buffer = text_area.getBuffer |
|
168 |
||
69969 | 169 |
val control_decoded = Isabelle_Encoding.perhaps_decode(buffer, control_sym) |
65259 | 170 |
|
80441 | 171 |
def update_style(text: String): String = |
172 |
Library.string_builder() { result => |
|
173 |
for (sym <- Symbol.iterator(text) if !HTML.is_control(sym)) { |
|
174 |
if (Symbol.is_controllable(sym)) result ++= control_decoded |
|
175 |
result ++= sym |
|
176 |
} |
|
65259 | 177 |
} |
178 |
||
75394 | 179 |
text_area.getSelection.foreach { sel => |
65259 | 180 |
val before = JEdit_Lib.point_range(buffer, sel.getStart - 1) |
67014 | 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 | 183 |
text_area.extendSelection(before.start, before.stop) |
184 |
case _ => |
|
185 |
} |
|
75394 | 186 |
} |
65259 | 187 |
|
188 |
text_area.getSelection.toList match { |
|
189 |
case Nil => |
|
190 |
text_area.setSelectedText(control_decoded) |
|
191 |
case sels => |
|
192 |
JEdit_Lib.buffer_edit(buffer) { |
|
193 |
sels.foreach(sel => |
|
194 |
text_area.setSelectedText(sel, update_style(text_area.getSelectedText(sel)))) |
|
195 |
} |
|
196 |
} |
|
197 |
} |
|
65258 | 198 |
} |