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 |
|
|
12 |
import java.awt.{Font, Color}
|
|
13 |
import java.awt.font.TextAttribute
|
|
14 |
import java.awt.geom.AffineTransform
|
|
15 |
|
|
16 |
import org.gjt.sp.util.SyntaxUtilities
|
|
17 |
import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
|
|
18 |
|
|
19 |
|
|
20 |
object Syntax_Style
|
|
21 |
{
|
|
22 |
private val plain_range: Int = JEditToken.ID_COUNT
|
|
23 |
private val full_range = 6 * plain_range + 1
|
|
24 |
private def check_range(i: Int) { require(0 <= i && i < plain_range) }
|
|
25 |
|
|
26 |
def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
|
|
27 |
def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
|
|
28 |
def bold(i: Byte): Byte = { check_range(i); (i + 3 * plain_range).toByte }
|
|
29 |
def user_font(idx: Int, i: Byte): Byte = { check_range(i); (i + (4 + idx) * plain_range).toByte }
|
|
30 |
val hidden: Byte = (6 * plain_range).toByte
|
|
31 |
|
|
32 |
private def font_style(style: SyntaxStyle, f: Font => Font): SyntaxStyle =
|
|
33 |
new SyntaxStyle(style.getForegroundColor, style.getBackgroundColor, f(style.getFont))
|
|
34 |
|
|
35 |
private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
|
|
36 |
{
|
|
37 |
font_style(style, font0 =>
|
|
38 |
{
|
|
39 |
import scala.collection.JavaConversions._
|
|
40 |
val font1 = font0.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
|
|
41 |
|
|
42 |
def shift(y: Float): Font =
|
|
43 |
GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
|
|
44 |
|
|
45 |
val m0 = GUI.line_metrics(font0)
|
|
46 |
val m1 = GUI.line_metrics(font1)
|
|
47 |
val a = m1.getAscent - m0.getAscent
|
|
48 |
val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
|
|
49 |
if (a > 0.0f) shift(a)
|
|
50 |
else if (b > 0.0f) shift(- b)
|
|
51 |
else font1
|
|
52 |
})
|
|
53 |
}
|
|
54 |
|
|
55 |
private def bold_style(style: SyntaxStyle): SyntaxStyle =
|
|
56 |
font_style(style, font => font.deriveFont(if (font.isBold) Font.PLAIN else Font.BOLD))
|
|
57 |
|
|
58 |
val hidden_color: Color = new Color(255, 255, 255, 0)
|
|
59 |
|
|
60 |
class Extender extends SyntaxUtilities.StyleExtender
|
|
61 |
{
|
|
62 |
val max_user_fonts = 2
|
|
63 |
if (Symbol.font_names.length > max_user_fonts)
|
|
64 |
error("Too many user symbol fonts (" + max_user_fonts + " permitted): " +
|
|
65 |
Symbol.font_names.mkString(", "))
|
|
66 |
|
|
67 |
override def extendStyles(styles: Array[SyntaxStyle]): Array[SyntaxStyle] =
|
|
68 |
{
|
|
69 |
val new_styles = new Array[SyntaxStyle](full_range)
|
|
70 |
for (i <- 0 until plain_range) {
|
|
71 |
val style = styles(i)
|
|
72 |
new_styles(i) = style
|
|
73 |
new_styles(subscript(i.toByte)) = script_style(style, -1)
|
|
74 |
new_styles(superscript(i.toByte)) = script_style(style, 1)
|
|
75 |
new_styles(bold(i.toByte)) = bold_style(style)
|
|
76 |
for (idx <- 0 until max_user_fonts)
|
|
77 |
new_styles(user_font(idx, i.toByte)) = style
|
|
78 |
for ((family, idx) <- Symbol.font_index)
|
|
79 |
new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(_, family))
|
|
80 |
}
|
|
81 |
new_styles(hidden) =
|
|
82 |
new SyntaxStyle(hidden_color, null,
|
|
83 |
{ val font = styles(0).getFont
|
|
84 |
GUI.transform_font(new Font(font.getFamily, 0, 1),
|
|
85 |
AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
|
|
86 |
new_styles
|
|
87 |
}
|
|
88 |
}
|
|
89 |
|
|
90 |
def extended(text: CharSequence): Map[Text.Offset, Byte => Byte] =
|
|
91 |
{
|
|
92 |
// FIXME Symbol.bsub_decoded etc.
|
|
93 |
def control_style(sym: String): Option[Byte => Byte] =
|
|
94 |
if (sym == Symbol.sub_decoded) Some(subscript(_))
|
|
95 |
else if (sym == Symbol.sup_decoded) Some(superscript(_))
|
|
96 |
else if (sym == Symbol.bold_decoded) Some(bold(_))
|
|
97 |
else None
|
|
98 |
|
|
99 |
var result = Map[Text.Offset, Byte => Byte]()
|
|
100 |
def mark(start: Text.Offset, stop: Text.Offset, style: Byte => Byte)
|
|
101 |
{
|
|
102 |
for (i <- start until stop) result += (i -> style)
|
|
103 |
}
|
|
104 |
var offset = 0
|
|
105 |
var control = ""
|
|
106 |
for (sym <- Symbol.iterator(text)) {
|
|
107 |
if (control_style(sym).isDefined) control = sym
|
|
108 |
else if (control != "") {
|
|
109 |
if (Symbol.is_controllable(sym) && sym != "\"" && !Symbol.fonts.isDefinedAt(sym)) {
|
|
110 |
mark(offset - control.length, offset, _ => hidden)
|
|
111 |
mark(offset, offset + sym.length, control_style(control).get)
|
|
112 |
}
|
|
113 |
control = ""
|
|
114 |
}
|
|
115 |
Symbol.lookup_font(sym) match {
|
|
116 |
case Some(idx) => mark(offset, offset + sym.length, user_font(idx, _))
|
|
117 |
case _ =>
|
|
118 |
}
|
|
119 |
offset += sym.length
|
|
120 |
}
|
|
121 |
result
|
|
122 |
}
|
|
123 |
}
|