equal
deleted
inserted
replaced
7 package isabelle.jedit |
7 package isabelle.jedit |
8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
|
12 import java.util.{Map => JMap} |
12 import java.awt.{Font, Color} |
13 import java.awt.{Font, Color} |
13 import java.awt.font.TextAttribute |
14 import java.awt.font.TextAttribute |
14 import java.awt.geom.AffineTransform |
15 import java.awt.geom.AffineTransform |
15 |
16 |
16 import org.gjt.sp.util.SyntaxUtilities |
17 import org.gjt.sp.util.SyntaxUtilities |
38 |
39 |
39 private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = |
40 private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle = |
40 { |
41 { |
41 font_style(style, font0 => |
42 font_style(style, font0 => |
42 { |
43 { |
43 val font1 = |
44 val font1 = font0.deriveFont(JMap.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i))) |
44 font0.deriveFont(java.util.Map.of(TextAttribute.SUPERSCRIPT, java.lang.Integer.valueOf(i))) |
|
45 |
45 |
46 def shift(y: Float): Font = |
46 def shift(y: Float): Font = |
47 GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble)) |
47 GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble)) |
48 |
48 |
49 val m0 = GUI.line_metrics(font0) |
49 val m0 = GUI.line_metrics(font0) |