wenzelm@44162
|
1 |
/* Title: Tools/jEdit/src/isabelle_markup.scala
|
wenzelm@39459
|
2 |
Author: Makarius
|
wenzelm@39459
|
3 |
|
wenzelm@39459
|
4 |
Isabelle specific physical rendering and markup selection.
|
wenzelm@39459
|
5 |
*/
|
wenzelm@39459
|
6 |
|
wenzelm@39459
|
7 |
package isabelle.jedit
|
wenzelm@39459
|
8 |
|
wenzelm@39459
|
9 |
|
wenzelm@39459
|
10 |
import isabelle._
|
wenzelm@39459
|
11 |
|
wenzelm@39459
|
12 |
import java.awt.Color
|
wenzelm@39459
|
13 |
|
wenzelm@44257
|
14 |
import org.lobobrowser.util.gui.ColorFactory
|
wenzelm@44288
|
15 |
import org.gjt.sp.jedit.syntax.{Token => JEditToken}
|
wenzelm@39459
|
16 |
|
wenzelm@39459
|
17 |
|
wenzelm@39459
|
18 |
object Isabelle_Markup
|
wenzelm@39459
|
19 |
{
|
wenzelm@39459
|
20 |
/* physical rendering */
|
wenzelm@39459
|
21 |
|
wenzelm@44248
|
22 |
// see http://www.w3schools.com/css/css_colornames.asp
|
wenzelm@44248
|
23 |
|
wenzelm@44257
|
24 |
def get_color(s: String): Color = ColorFactory.getInstance.getColor(s)
|
wenzelm@44257
|
25 |
|
wenzelm@45466
|
26 |
val outdated_color = new Color(238, 227, 227)
|
wenzelm@39459
|
27 |
val unfinished_color = new Color(255, 228, 225)
|
wenzelm@39459
|
28 |
|
wenzelm@39938
|
29 |
val light_color = new Color(240, 240, 240)
|
wenzelm@39459
|
30 |
val regular_color = new Color(192, 192, 192)
|
wenzelm@39940
|
31 |
val warning_color = new Color(255, 140, 0)
|
wenzelm@39939
|
32 |
val error_color = new Color(178, 34, 34)
|
wenzelm@39938
|
33 |
val bad_color = new Color(255, 106, 106, 100)
|
wenzelm@43042
|
34 |
val hilite_color = new Color(255, 204, 102, 100)
|
wenzelm@39459
|
35 |
|
wenzelm@45417
|
36 |
val quoted_color = new Color(139, 139, 139, 25)
|
wenzelm@45416
|
37 |
val subexp_color = new Color(80, 80, 80, 50)
|
wenzelm@44307
|
38 |
|
wenzelm@44259
|
39 |
val keyword1_color = get_color("#006699")
|
wenzelm@44259
|
40 |
val keyword2_color = get_color("#009966")
|
wenzelm@44259
|
41 |
|
wenzelm@39462
|
42 |
class Icon(val priority: Int, val icon: javax.swing.Icon)
|
wenzelm@39462
|
43 |
{
|
wenzelm@39462
|
44 |
def >= (that: Icon): Boolean = this.priority >= that.priority
|
wenzelm@39462
|
45 |
}
|
wenzelm@45418
|
46 |
val warning_icon = new Icon(1, Isabelle.load_icon("16x16/status/dialog-information.png"))
|
wenzelm@45420
|
47 |
val legacy_icon = new Icon(2, Isabelle.load_icon("16x16/status/dialog-warning.png"))
|
wenzelm@45420
|
48 |
val error_icon = new Icon(3, Isabelle.load_icon("16x16/status/dialog-error.png"))
|
wenzelm@39459
|
49 |
|
wenzelm@39459
|
50 |
|
wenzelm@39459
|
51 |
/* command status */
|
wenzelm@39459
|
52 |
|
wenzelm@39459
|
53 |
def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
|
wenzelm@39459
|
54 |
{
|
wenzelm@39459
|
55 |
val state = snapshot.state(command)
|
wenzelm@39459
|
56 |
if (snapshot.is_outdated) Some(outdated_color)
|
wenzelm@39459
|
57 |
else
|
wenzelm@39459
|
58 |
Isar_Document.command_status(state.status) match {
|
wenzelm@39459
|
59 |
case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
|
wenzelm@39459
|
60 |
case Isar_Document.Unprocessed => Some(unfinished_color)
|
wenzelm@39459
|
61 |
case _ => None
|
wenzelm@39459
|
62 |
}
|
wenzelm@39459
|
63 |
}
|
wenzelm@39459
|
64 |
|
wenzelm@39459
|
65 |
def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
|
wenzelm@39459
|
66 |
{
|
wenzelm@39459
|
67 |
val state = snapshot.state(command)
|
wenzelm@39459
|
68 |
if (snapshot.is_outdated) None
|
wenzelm@39459
|
69 |
else
|
wenzelm@39459
|
70 |
Isar_Document.command_status(state.status) match {
|
wenzelm@39781
|
71 |
case Isar_Document.Forked(i) => if (i > 0) Some(unfinished_color) else None
|
wenzelm@39459
|
72 |
case Isar_Document.Unprocessed => Some(unfinished_color)
|
wenzelm@39459
|
73 |
case Isar_Document.Failed => Some(error_color)
|
wenzelm@39781
|
74 |
case Isar_Document.Finished =>
|
wenzelm@39781
|
75 |
if (state.results.exists(r => Isar_Document.is_error(r._2))) Some(error_color)
|
wenzelm@39781
|
76 |
else if (state.results.exists(r => Isar_Document.is_warning(r._2))) Some(warning_color)
|
wenzelm@39781
|
77 |
else None
|
wenzelm@39459
|
78 |
}
|
wenzelm@39459
|
79 |
}
|
wenzelm@39459
|
80 |
|
wenzelm@39459
|
81 |
|
wenzelm@39459
|
82 |
/* markup selectors */
|
wenzelm@39459
|
83 |
|
wenzelm@39459
|
84 |
val message: Markup_Tree.Select[Color] =
|
wenzelm@39459
|
85 |
{
|
wenzelm@39459
|
86 |
case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
|
wenzelm@39459
|
87 |
case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
|
wenzelm@39459
|
88 |
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
|
wenzelm@39459
|
89 |
}
|
wenzelm@39459
|
90 |
|
wenzelm@40600
|
91 |
val popup: Markup_Tree.Select[String] =
|
wenzelm@40033
|
92 |
{
|
wenzelm@40033
|
93 |
case Text.Info(_, msg @ XML.Elem(Markup(markup, _), _))
|
wenzelm@40600
|
94 |
if markup == Markup.WRITELN || markup == Markup.WARNING || markup == Markup.ERROR =>
|
wenzelm@40601
|
95 |
Pretty.string_of(List(msg), margin = Isabelle.Int_Property("tooltip-margin"))
|
wenzelm@40033
|
96 |
}
|
wenzelm@40033
|
97 |
|
wenzelm@39462
|
98 |
val gutter_message: Markup_Tree.Select[Icon] =
|
wenzelm@39462
|
99 |
{
|
wenzelm@45420
|
100 |
case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), body)) =>
|
wenzelm@45420
|
101 |
body match {
|
wenzelm@45420
|
102 |
case List(XML.Elem(Markup(Markup.LEGACY, _), _)) => legacy_icon
|
wenzelm@45420
|
103 |
case _ => warning_icon
|
wenzelm@45420
|
104 |
}
|
wenzelm@39462
|
105 |
case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
|
wenzelm@39462
|
106 |
}
|
wenzelm@39462
|
107 |
|
wenzelm@39965
|
108 |
val background1: Markup_Tree.Select[Color] =
|
wenzelm@39459
|
109 |
{
|
wenzelm@39459
|
110 |
case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
|
wenzelm@43042
|
111 |
case Text.Info(_, XML.Elem(Markup(Markup.HILITE, _), _)) => hilite_color
|
wenzelm@39459
|
112 |
}
|
wenzelm@39459
|
113 |
|
wenzelm@39965
|
114 |
val background2: Markup_Tree.Select[Color] =
|
wenzelm@39459
|
115 |
{
|
wenzelm@39938
|
116 |
case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
|
wenzelm@39459
|
117 |
}
|
wenzelm@39459
|
118 |
|
wenzelm@45416
|
119 |
val foreground: Markup_Tree.Select[Color] =
|
wenzelm@45416
|
120 |
{
|
wenzelm@45417
|
121 |
case Text.Info(_, XML.Elem(Markup(Markup.STRING, _), _)) => quoted_color
|
wenzelm@45417
|
122 |
case Text.Info(_, XML.Elem(Markup(Markup.ALTSTRING, _), _)) => quoted_color
|
wenzelm@45417
|
123 |
case Text.Info(_, XML.Elem(Markup(Markup.VERBATIM, _), _)) => quoted_color
|
wenzelm@45416
|
124 |
}
|
wenzelm@45416
|
125 |
|
wenzelm@44419
|
126 |
private val text_entity_colors: Map[String, Color] =
|
wenzelm@44419
|
127 |
Map(
|
wenzelm@44423
|
128 |
Markup.CLASS -> get_color("red"),
|
wenzelm@44423
|
129 |
Markup.TYPE -> get_color("black"),
|
wenzelm@44460
|
130 |
Markup.CONSTANT -> get_color("black"))
|
wenzelm@44419
|
131 |
|
wenzelm@44306
|
132 |
private val text_colors: Map[String, Color] =
|
wenzelm@44257
|
133 |
Map(
|
wenzelm@45416
|
134 |
Markup.STRING -> get_color("black"),
|
wenzelm@45416
|
135 |
Markup.ALTSTRING -> get_color("black"),
|
wenzelm@45416
|
136 |
Markup.VERBATIM -> get_color("black"),
|
wenzelm@44308
|
137 |
Markup.LITERAL -> keyword1_color,
|
wenzelm@44308
|
138 |
Markup.DELIMITER -> get_color("black"),
|
wenzelm@44308
|
139 |
Markup.IDENT -> get_color("black"),
|
wenzelm@44257
|
140 |
Markup.TFREE -> get_color("#A020F0"),
|
wenzelm@44257
|
141 |
Markup.TVAR -> get_color("#A020F0"),
|
wenzelm@44257
|
142 |
Markup.FREE -> get_color("blue"),
|
wenzelm@44257
|
143 |
Markup.SKOLEM -> get_color("#D2691E"),
|
wenzelm@44257
|
144 |
Markup.BOUND -> get_color("green"),
|
wenzelm@44257
|
145 |
Markup.VAR -> get_color("#00009B"),
|
wenzelm@44257
|
146 |
Markup.INNER_STRING -> get_color("#D2691E"),
|
wenzelm@44257
|
147 |
Markup.INNER_COMMENT -> get_color("#8B0000"),
|
wenzelm@44257
|
148 |
Markup.DYNAMIC_FACT -> get_color("yellowgreen"),
|
wenzelm@44259
|
149 |
Markup.ML_KEYWORD -> keyword1_color,
|
wenzelm@44257
|
150 |
Markup.ML_DELIMITER -> get_color("black"),
|
wenzelm@44257
|
151 |
Markup.ML_NUMERAL -> get_color("red"),
|
wenzelm@44257
|
152 |
Markup.ML_CHAR -> get_color("#D2691E"),
|
wenzelm@44257
|
153 |
Markup.ML_STRING -> get_color("#D2691E"),
|
wenzelm@44257
|
154 |
Markup.ML_COMMENT -> get_color("#8B0000"),
|
wenzelm@44303
|
155 |
Markup.ML_MALFORMED -> get_color("#FF6A6A"),
|
wenzelm@44303
|
156 |
Markup.ANTIQ -> get_color("blue"))
|
wenzelm@44257
|
157 |
|
wenzelm@44306
|
158 |
val text_color: Markup_Tree.Select[Color] =
|
wenzelm@44247
|
159 |
{
|
wenzelm@44419
|
160 |
case Text.Info(_, XML.Elem(Markup.Entity(kind, _), _))
|
wenzelm@44419
|
161 |
if text_entity_colors.isDefinedAt(kind) => text_entity_colors(kind)
|
wenzelm@44257
|
162 |
case Text.Info(_, XML.Elem(Markup(m, _), _))
|
wenzelm@44306
|
163 |
if text_colors.isDefinedAt(m) => text_colors(m)
|
wenzelm@44247
|
164 |
}
|
wenzelm@44247
|
165 |
|
wenzelm@44303
|
166 |
private val tooltips: Map[String, String] =
|
wenzelm@44303
|
167 |
Map(
|
wenzelm@44303
|
168 |
Markup.SORT -> "sort",
|
wenzelm@44303
|
169 |
Markup.TYP -> "type",
|
wenzelm@44303
|
170 |
Markup.TERM -> "term",
|
wenzelm@44303
|
171 |
Markup.PROP -> "proposition",
|
wenzelm@44303
|
172 |
Markup.TOKEN_RANGE -> "inner syntax token",
|
wenzelm@44303
|
173 |
Markup.FREE -> "free variable (globally fixed)",
|
wenzelm@44303
|
174 |
Markup.SKOLEM -> "skolem variable (locally fixed)",
|
wenzelm@44303
|
175 |
Markup.BOUND -> "bound variable (internally fixed)",
|
wenzelm@44303
|
176 |
Markup.VAR -> "schematic variable",
|
wenzelm@44303
|
177 |
Markup.TFREE -> "free type variable",
|
wenzelm@44303
|
178 |
Markup.TVAR -> "schematic type variable",
|
wenzelm@44303
|
179 |
Markup.ML_SOURCE -> "ML source",
|
wenzelm@44303
|
180 |
Markup.DOC_SOURCE -> "document source")
|
wenzelm@44303
|
181 |
|
wenzelm@39459
|
182 |
val tooltip: Markup_Tree.Select[String] =
|
wenzelm@39459
|
183 |
{
|
wenzelm@45054
|
184 |
case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " " + quote(name)
|
wenzelm@39459
|
185 |
case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
|
wenzelm@40601
|
186 |
Pretty.string_of(List(Pretty.block(XML.Text("ML:") :: Pretty.Break(1) :: body)),
|
wenzelm@40601
|
187 |
margin = Isabelle.Int_Property("tooltip-margin"))
|
wenzelm@44303
|
188 |
case Text.Info(_, XML.Elem(Markup(name, _), _))
|
wenzelm@44303
|
189 |
if tooltips.isDefinedAt(name) => tooltips(name)
|
wenzelm@43193
|
190 |
}
|
wenzelm@43193
|
191 |
|
wenzelm@43193
|
192 |
private val subexp_include =
|
wenzelm@43193
|
193 |
Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING, Markup.TOKEN_RANGE,
|
wenzelm@43193
|
194 |
Markup.ENTITY, Markup.FREE, Markup.SKOLEM, Markup.BOUND, Markup.VAR,
|
wenzelm@44303
|
195 |
Markup.TFREE, Markup.TVAR, Markup.ML_SOURCE, Markup.DOC_SOURCE)
|
wenzelm@43193
|
196 |
|
wenzelm@43193
|
197 |
val subexp: Markup_Tree.Select[(Text.Range, Color)] =
|
wenzelm@43193
|
198 |
{
|
wenzelm@43193
|
199 |
case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
|
wenzelm@44307
|
200 |
(range, subexp_color)
|
wenzelm@39459
|
201 |
}
|
wenzelm@39460
|
202 |
|
wenzelm@39460
|
203 |
|
wenzelm@39460
|
204 |
/* token markup -- text styles */
|
wenzelm@39460
|
205 |
|
wenzelm@39460
|
206 |
private val command_style: Map[String, Byte] =
|
wenzelm@39460
|
207 |
{
|
wenzelm@44288
|
208 |
import JEditToken._
|
wenzelm@39460
|
209 |
Map[String, Byte](
|
wenzelm@39460
|
210 |
Keyword.THY_END -> KEYWORD2,
|
wenzelm@39460
|
211 |
Keyword.THY_SCRIPT -> LABEL,
|
wenzelm@39460
|
212 |
Keyword.PRF_SCRIPT -> LABEL,
|
wenzelm@39460
|
213 |
Keyword.PRF_ASM -> KEYWORD3,
|
wenzelm@39460
|
214 |
Keyword.PRF_ASM_GOAL -> KEYWORD3
|
wenzelm@39460
|
215 |
).withDefaultValue(KEYWORD1)
|
wenzelm@39460
|
216 |
}
|
wenzelm@39460
|
217 |
|
wenzelm@44288
|
218 |
private val token_style: Map[Token.Kind.Value, Byte] =
|
wenzelm@39460
|
219 |
{
|
wenzelm@44288
|
220 |
import JEditToken._
|
wenzelm@44288
|
221 |
Map[Token.Kind.Value, Byte](
|
wenzelm@44288
|
222 |
Token.Kind.KEYWORD -> KEYWORD2,
|
wenzelm@44288
|
223 |
Token.Kind.IDENT -> NULL,
|
wenzelm@44288
|
224 |
Token.Kind.LONG_IDENT -> NULL,
|
wenzelm@44288
|
225 |
Token.Kind.SYM_IDENT -> NULL,
|
wenzelm@44288
|
226 |
Token.Kind.VAR -> NULL,
|
wenzelm@44288
|
227 |
Token.Kind.TYPE_IDENT -> NULL,
|
wenzelm@44288
|
228 |
Token.Kind.TYPE_VAR -> NULL,
|
wenzelm@44288
|
229 |
Token.Kind.NAT -> NULL,
|
wenzelm@44288
|
230 |
Token.Kind.FLOAT -> NULL,
|
wenzelm@44303
|
231 |
Token.Kind.STRING -> LITERAL1,
|
wenzelm@44303
|
232 |
Token.Kind.ALT_STRING -> LITERAL2,
|
wenzelm@44288
|
233 |
Token.Kind.VERBATIM -> COMMENT3,
|
wenzelm@44288
|
234 |
Token.Kind.SPACE -> NULL,
|
wenzelm@44288
|
235 |
Token.Kind.COMMENT -> COMMENT1,
|
wenzelm@44288
|
236 |
Token.Kind.UNPARSED -> INVALID
|
wenzelm@39460
|
237 |
).withDefaultValue(NULL)
|
wenzelm@39460
|
238 |
}
|
wenzelm@39460
|
239 |
|
wenzelm@44288
|
240 |
def token_markup(syntax: Outer_Syntax, token: Token): Byte =
|
wenzelm@44302
|
241 |
if (token.is_command) command_style(syntax.keyword_kind(token.content).getOrElse(""))
|
wenzelm@44302
|
242 |
else if (token.is_operator) JEditToken.OPERATOR
|
wenzelm@44288
|
243 |
else token_style(token.kind)
|
wenzelm@39459
|
244 |
}
|