author | wenzelm |
Sat, 18 Jun 2011 12:58:41 +0200 | |
changeset 43434 | 2fd41645813d |
parent 43432 | 224006e5ac46 |
child 43435 | ae6b0c3e58a8 |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
42492
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/isabelle_markup.scala |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
3 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
4 |
Isabelle specific physical rendering and markup selection. |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
6 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
8 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
9 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
11 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
12 |
import java.awt.Color |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
13 |
|
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
14 |
import org.lobobrowser.util.gui.ColorFactory |
43414 | 15 |
import org.gjt.sp.jedit.syntax.{Token => JEditToken} |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
16 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
17 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
18 |
object Isabelle_Markup |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
19 |
{ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
20 |
/* physical rendering */ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
21 |
|
43377 | 22 |
// see http://www.w3schools.com/css/css_colornames.asp |
23 |
||
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
24 |
def get_color(s: String): Color = ColorFactory.getInstance.getColor(s) |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
25 |
|
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
26 |
val outdated_color = new Color(240, 240, 240) |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
27 |
val unfinished_color = new Color(255, 228, 225) |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
28 |
|
39690
6c6164b37fef
some attempts to improve visual appearance of bad text;
wenzelm
parents:
39512
diff
changeset
|
29 |
val light_color = new Color(240, 240, 240) |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
30 |
val regular_color = new Color(192, 192, 192) |
39692 | 31 |
val warning_color = new Color(255, 140, 0) |
39691 | 32 |
val error_color = new Color(178, 34, 34) |
39690
6c6164b37fef
some attempts to improve visual appearance of bad text;
wenzelm
parents:
39512
diff
changeset
|
33 |
val bad_color = new Color(255, 106, 106, 100) |
42171 | 34 |
val hilite_color = new Color(255, 204, 102, 100) |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
35 |
|
43388 | 36 |
val keyword1_color = get_color("#006699") |
37 |
val keyword2_color = get_color("#009966") |
|
38 |
||
39181
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
39 |
class Icon(val priority: Int, val icon: javax.swing.Icon) |
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
40 |
{ |
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
41 |
def >= (that: Icon): Boolean = this.priority >= that.priority |
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
42 |
} |
39241 | 43 |
val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-warning.png")) |
44 |
val error_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-error.png")) |
|
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
45 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
46 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
47 |
/* command status */ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
48 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
49 |
def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] = |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
50 |
{ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
51 |
val state = snapshot.state(command) |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
52 |
if (snapshot.is_outdated) Some(outdated_color) |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
53 |
else |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
54 |
Isar_Document.command_status(state.status) match { |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
55 |
case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color) |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
56 |
case Isar_Document.Unprocessed => Some(unfinished_color) |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
57 |
case _ => None |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
58 |
} |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
59 |
} |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
60 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
61 |
def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] = |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
62 |
{ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
63 |
val state = snapshot.state(command) |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
64 |
if (snapshot.is_outdated) None |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
65 |
else |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
66 |
Isar_Document.command_status(state.status) match { |
39512
31290f54be19
Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents:
39244
diff
changeset
|
67 |
case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
68 |
case Isar_Document.Unprocessed => Some(unfinished_color) |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
69 |
case Isar_Document.Failed => Some(error_color) |
39512
31290f54be19
Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents:
39244
diff
changeset
|
70 |
case Isar_Document.Finished => |
31290f54be19
Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents:
39244
diff
changeset
|
71 |
if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color) |
31290f54be19
Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents:
39244
diff
changeset
|
72 |
else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color) |
31290f54be19
Isabelle_Markup.overview_color: indicate error / warning messages;
wenzelm
parents:
39244
diff
changeset
|
73 |
else None |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
74 |
} |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
75 |
} |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
76 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
77 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
78 |
/* markup selectors */ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
79 |
|
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
80 |
val message: Markup_Tree.Select[Color] = |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
81 |
{ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
82 |
case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
83 |
case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
84 |
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
85 |
} |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
86 |
|
40338
e2f03de2b3c7
clarified tooltips: message output by default, extra info via control/command;
wenzelm
parents:
39740
diff
changeset
|
87 |
val popup: Markup_Tree.Select[String] = |
39740 | 88 |
{ |
89 |
case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _)) |
|
40338
e2f03de2b3c7
clarified tooltips: message output by default, extra info via control/command;
wenzelm
parents:
39740
diff
changeset
|
90 |
if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR => |
40339 | 91 |
Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin")) |
39740 | 92 |
} |
93 |
||
39181
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
94 |
val gutter_message: Markup_Tree.Select[Icon] = |
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
95 |
{ |
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
96 |
case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon |
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
97 |
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon |
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
98 |
} |
2257eded8323
Document_View: select gutter message icons from markup over line range, not full range results;
wenzelm
parents:
39179
diff
changeset
|
99 |
|
39700
fa55cf2c1ae4
more precise treatment of backgrounds vs. rectangles;
wenzelm
parents:
39692
diff
changeset
|
100 |
val background1: Markup_Tree.Select[Color] = |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
101 |
{ |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
102 |
case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color |
42171 | 103 |
case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
104 |
} |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
105 |
|
39700
fa55cf2c1ae4
more precise treatment of backgrounds vs. rectangles;
wenzelm
parents:
39692
diff
changeset
|
106 |
val background2: Markup_Tree.Select[Color] = |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
107 |
{ |
39690
6c6164b37fef
some attempts to improve visual appearance of bad text;
wenzelm
parents:
39512
diff
changeset
|
108 |
case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
109 |
} |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
110 |
|
43434 | 111 |
private val text_colors: Map[String, Color] = |
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
112 |
Map( |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
113 |
Markup.TCLASS -> get_color("red"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
114 |
Markup.TFREE -> get_color("#A020F0"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
115 |
Markup.TVAR -> get_color("#A020F0"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
116 |
Markup.CONST -> get_color("dimgrey"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
117 |
Markup.FREE -> get_color("blue"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
118 |
Markup.SKOLEM -> get_color("#D2691E"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
119 |
Markup.BOUND -> get_color("green"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
120 |
Markup.VAR -> get_color("#00009B"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
121 |
Markup.INNER_STRING -> get_color("#D2691E"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
122 |
Markup.INNER_COMMENT -> get_color("#8B0000"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
123 |
Markup.DYNAMIC_FACT -> get_color("yellowgreen"), |
43388 | 124 |
Markup.LITERAL -> keyword1_color, |
43432
224006e5ac46
inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents:
43431
diff
changeset
|
125 |
Markup.DELIMITER -> get_color("black"), |
43388 | 126 |
Markup.ML_KEYWORD -> keyword1_color, |
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
127 |
Markup.ML_DELIMITER -> get_color("black"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
128 |
Markup.ML_NUMERAL -> get_color("red"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
129 |
Markup.ML_CHAR -> get_color("#D2691E"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
130 |
Markup.ML_STRING -> get_color("#D2691E"), |
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
131 |
Markup.ML_COMMENT -> get_color("#8B0000"), |
43431 | 132 |
Markup.ML_MALFORMED -> get_color("#FF6A6A"), |
133 |
Markup.ANTIQ -> get_color("blue")) |
|
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
134 |
|
43434 | 135 |
val text_color: Markup_Tree.Select[Color] = |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43282
diff
changeset
|
136 |
{ |
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
43377
diff
changeset
|
137 |
case Text.Info(_, XML.Elem(Markup(m, _), _)) |
43434 | 138 |
if text_colors.isDefinedAt(m) => text_colors(m) |
43376
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43282
diff
changeset
|
139 |
} |
0f6880c1c759
some direct text foreground painting, instead of token marking;
wenzelm
parents:
43282
diff
changeset
|
140 |
|
43431 | 141 |
private val tooltips: Map[String, String] = |
142 |
Map( |
|
143 |
Markup.SORT -> "sort", |
|
144 |
Markup.TYP -> "type", |
|
145 |
Markup.TERM -> "term", |
|
146 |
Markup.PROP -> "proposition", |
|
147 |
Markup.TOKEN_RANGE -> "inner syntax token", |
|
148 |
Markup.FREE -> "free variable (globally fixed)", |
|
149 |
Markup.SKOLEM -> "skolem variable (locally fixed)", |
|
150 |
Markup.BOUND -> "bound variable (internally fixed)", |
|
151 |
Markup.VAR -> "schematic variable", |
|
152 |
Markup.TFREE -> "free type variable", |
|
153 |
Markup.TVAR -> "schematic type variable", |
|
154 |
Markup.ML_SOURCE -> "ML source", |
|
155 |
Markup.DOC_SOURCE -> "document source") |
|
156 |
||
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
157 |
val tooltip: Markup_Tree.Select[String] = |
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
158 |
{ |
42283 | 159 |
case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\"" |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
160 |
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) => |
40339 | 161 |
Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)), |
162 |
margin = Isabelle.Int_Property("tooltip-margin")) |
|
43431 | 163 |
case Text.Info(_, XML.Elem(Markup(name, _), _)) |
164 |
if tooltips.isDefinedAt(name) => tooltips(name) |
|
42302 | 165 |
} |
166 |
||
167 |
private val subexp_include = |
|
168 |
Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE, |
|
169 |
Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR, |
|
43431 | 170 |
Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE) |
42302 | 171 |
|
172 |
val subexp: Markup_Tree.Select[(Text.Range, Color)] = |
|
173 |
{ |
|
174 |
case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) => |
|
175 |
(range, Color.black) |
|
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
176 |
} |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
177 |
|
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
178 |
|
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
179 |
/* token markup -- text styles */ |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
180 |
|
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
181 |
private val command_style: Map[String, Byte] = |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
182 |
{ |
43414 | 183 |
import JEditToken._ |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
184 |
Map[String, Byte]( |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
185 |
Keyword.THY_END -> KEYWORD2, |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
186 |
Keyword.THY_SCRIPT -> LABEL, |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
187 |
Keyword.PRF_SCRIPT -> LABEL, |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
188 |
Keyword.PRF_ASM -> KEYWORD3, |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
189 |
Keyword.PRF_ASM_GOAL -> KEYWORD3 |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
190 |
).withDefaultValue(KEYWORD1) |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
191 |
} |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
192 |
|
43414 | 193 |
private val token_style: Map[Token.Kind.Value, Byte] = |
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
194 |
{ |
43414 | 195 |
import JEditToken._ |
196 |
Map[Token.Kind.Value, Byte]( |
|
197 |
Token.Kind.KEYWORD -> KEYWORD2, |
|
198 |
Token.Kind.IDENT -> NULL, |
|
199 |
Token.Kind.LONG_IDENT -> NULL, |
|
200 |
Token.Kind.SYM_IDENT -> NULL, |
|
201 |
Token.Kind.VAR -> NULL, |
|
202 |
Token.Kind.TYPE_IDENT -> NULL, |
|
203 |
Token.Kind.TYPE_VAR -> NULL, |
|
204 |
Token.Kind.NAT -> NULL, |
|
205 |
Token.Kind.FLOAT -> NULL, |
|
43431 | 206 |
Token.Kind.STRING -> LITERAL1, |
207 |
Token.Kind.ALT_STRING -> LITERAL2, |
|
43414 | 208 |
Token.Kind.VERBATIM -> COMMENT3, |
209 |
Token.Kind.SPACE -> NULL, |
|
210 |
Token.Kind.COMMENT -> COMMENT1, |
|
211 |
Token.Kind.UNPARSED -> INVALID |
|
39179
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
212 |
).withDefaultValue(NULL) |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
213 |
} |
591bbab9ef59
moved token markup tables to isabelle_markup.scala;
wenzelm
parents:
39178
diff
changeset
|
214 |
|
43414 | 215 |
def token_markup(syntax: Outer_Syntax, token: Token): Byte = |
43430
1ed88ddf1268
more uniform treatment of "keyword" vs. "operator";
wenzelm
parents:
43418
diff
changeset
|
216 |
if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse("")) |
1ed88ddf1268
more uniform treatment of "keyword" vs. "operator";
wenzelm
parents:
43418
diff
changeset
|
217 |
else if (token.is_operator) JEditToken.OPERATOR |
43414 | 218 |
else token_style(token.kind) |
39178
83e9f3ccea9f
concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;
wenzelm
parents:
diff
changeset
|
219 |
} |