author | wenzelm |
Sat, 25 Jun 2011 19:38:35 +0200 | |
changeset 43552 | 156c822f181a |
parent 43551 | 07a9cbf2376f |
child 43560 | d1650e3720fd |
permissions | -rw-r--r-- |
27958 | 1 |
/* Title: Pure/General/markup.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Common markup elements. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
27970 | 9 |
|
32450 | 10 |
object Markup |
11 |
{ |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
12 |
/* plain values */ |
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
13 |
|
40392 | 14 |
object Int |
15 |
{ |
|
16 |
def apply(x: scala.Int): String = x.toString |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
17 |
def unapply(s: String): Option[scala.Int] = |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
18 |
try { Some(Integer.parseInt(s)) } |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
19 |
catch { case _: NumberFormatException => None } |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
20 |
} |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
21 |
|
40392 | 22 |
object Long |
23 |
{ |
|
24 |
def apply(x: scala.Long): String = x.toString |
|
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
25 |
def unapply(s: String): Option[scala.Long] = |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
26 |
try { Some(java.lang.Long.parseLong(s)) } |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
27 |
catch { case _: NumberFormatException => None } |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
28 |
} |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
29 |
|
40392 | 30 |
object Double |
31 |
{ |
|
32 |
def apply(x: scala.Double): String = x.toString |
|
33 |
def unapply(s: String): Option[scala.Double] = |
|
34 |
try { Some(java.lang.Double.parseDouble(s)) } |
|
35 |
catch { case _: NumberFormatException => None } |
|
36 |
} |
|
37 |
||
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
38 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
39 |
/* named properties */ |
36683 | 40 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
41 |
class Property(val name: String) |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
42 |
{ |
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
43 |
def apply(value: String): List[(String, String)] = List((name, value)) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
44 |
def unapply(props: List[(String, String)]): Option[String] = |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
45 |
props.find(_._1 == name).map(_._2) |
38355
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
46 |
} |
8cb265fb12fe
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
wenzelm
parents:
38259
diff
changeset
|
47 |
|
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
48 |
class Int_Property(name: String) |
36683 | 49 |
{ |
38722
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
50 |
def apply(value: scala.Int): List[(String, String)] = List((name, Int(value))) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
51 |
def unapply(props: List[(String, String)]): Option[Int] = |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
52 |
props.find(_._1 == name) match { |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
53 |
case None => None |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
54 |
case Some((_, value)) => Int.unapply(value) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
55 |
} |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
56 |
} |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
57 |
|
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
58 |
class Long_Property(name: String) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
59 |
{ |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
60 |
def apply(value: scala.Long): List[(String, String)] = List((name, Long(value))) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
61 |
def unapply(props: List[(String, String)]): Option[Long] = |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
62 |
props.find(_._1 == name) match { |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
63 |
case None => None |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
64 |
case Some((_, value)) => Long.unapply(value) |
ba31936497c2
organized markup properties via apply/unapply patterns;
wenzelm
parents:
38721
diff
changeset
|
65 |
} |
36683 | 66 |
} |
67 |
||
40392 | 68 |
class Double_Property(name: String) |
69 |
{ |
|
70 |
def apply(value: scala.Double): List[(String, String)] = List((name, Double(value))) |
|
71 |
def unapply(props: List[(String, String)]): Option[Double] = |
|
72 |
props.find(_._1 == name) match { |
|
73 |
case None => None |
|
74 |
case Some((_, value)) => Double.unapply(value) |
|
75 |
} |
|
76 |
} |
|
77 |
||
36683 | 78 |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
79 |
/* empty */ |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
80 |
|
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
81 |
val Empty = Markup("", Nil) |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
82 |
|
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
83 |
|
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
84 |
/* misc properties */ |
29184 | 85 |
|
86 |
val NAME = "name" |
|
42136 | 87 |
val Name = new Property(NAME) |
88 |
||
29184 | 89 |
val KIND = "kind" |
42136 | 90 |
val Kind = new Property(KIND) |
29184 | 91 |
|
92 |
||
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
93 |
/* formal entities */ |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
94 |
|
38887
1261481ef5e5
Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
wenzelm
parents:
38872
diff
changeset
|
95 |
val BINDING = "binding" |
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
96 |
val ENTITY = "entity" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
97 |
val DEF = "def" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
98 |
val REF = "ref" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
99 |
|
42202 | 100 |
object Entity |
101 |
{ |
|
102 |
def unapply(markup: Markup): Option[(String, String)] = |
|
103 |
markup match { |
|
104 |
case Markup(ENTITY, props @ Kind(kind)) => |
|
105 |
props match { |
|
106 |
case Name(name) => Some(kind, name) |
|
107 |
case _ => None |
|
108 |
} |
|
109 |
case _ => None |
|
110 |
} |
|
111 |
} |
|
112 |
||
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
113 |
|
27970 | 114 |
/* position */ |
115 |
||
116 |
val LINE = "line" |
|
117 |
val COLUMN = "column" |
|
118 |
val OFFSET = "offset" |
|
119 |
val END_OFFSET = "end_offset" |
|
120 |
val FILE = "file" |
|
121 |
val ID = "id" |
|
122 |
||
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
123 |
val DEF_LINE = "def_line" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
124 |
val DEF_COLUMN = "def_column" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
125 |
val DEF_OFFSET = "def_offset" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
126 |
val DEF_END_OFFSET = "def_end_offset" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
127 |
val DEF_FILE = "def_file" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
128 |
val DEF_ID = "def_id" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
129 |
|
41483 | 130 |
val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_OFFSET, FILE, ID) |
29205 | 131 |
|
29184 | 132 |
val POSITION = "position" |
133 |
||
134 |
||
36683 | 135 |
/* pretty printing */ |
136 |
||
38724 | 137 |
val Indent = new Int_Property("indent") |
36683 | 138 |
val BLOCK = "block" |
38724 | 139 |
val Width = new Int_Property("width") |
36683 | 140 |
val BREAK = "break" |
141 |
||
142 |
||
33985 | 143 |
/* hidden text */ |
144 |
||
145 |
val HIDDEN = "hidden" |
|
146 |
||
147 |
||
29184 | 148 |
/* logical entities */ |
149 |
||
43551 | 150 |
val CLASS = "class" |
43552 | 151 |
val TYPE = "type" |
29184 | 152 |
val FIXED = "fixed" |
43552 | 153 |
val CONSTANT = "constant" |
154 |
||
29184 | 155 |
val DYNAMIC_FACT = "dynamic_fact" |
156 |
||
157 |
||
158 |
/* inner syntax */ |
|
159 |
||
160 |
val TFREE = "tfree" |
|
161 |
val TVAR = "tvar" |
|
162 |
val FREE = "free" |
|
163 |
val SKOLEM = "skolem" |
|
164 |
val BOUND = "bound" |
|
165 |
val VAR = "var" |
|
166 |
val NUM = "num" |
|
167 |
val FLOAT = "float" |
|
168 |
val XNUM = "xnum" |
|
169 |
val XSTR = "xstr" |
|
170 |
val LITERAL = "literal" |
|
43432
224006e5ac46
inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents:
43386
diff
changeset
|
171 |
val DELIMITER = "delimiter" |
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
42492
diff
changeset
|
172 |
val INNER_STRING = "inner_string" |
29184 | 173 |
val INNER_COMMENT = "inner_comment" |
174 |
||
39168
e3ac771235f7
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38887
diff
changeset
|
175 |
val TOKEN_RANGE = "token_range" |
e3ac771235f7
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38887
diff
changeset
|
176 |
|
29184 | 177 |
val SORT = "sort" |
178 |
val TYP = "typ" |
|
179 |
val TERM = "term" |
|
180 |
val PROP = "prop" |
|
181 |
||
182 |
val ATTRIBUTE = "attribute" |
|
183 |
val METHOD = "method" |
|
184 |
||
185 |
||
186 |
/* embedded source text */ |
|
187 |
||
188 |
val ML_SOURCE = "ML_source" |
|
189 |
val DOC_SOURCE = "doc_source" |
|
190 |
||
191 |
val ANTIQ = "antiq" |
|
192 |
val ML_ANTIQ = "ML_antiq" |
|
193 |
val DOC_ANTIQ = "doc_antiq" |
|
194 |
||
195 |
||
30615 | 196 |
/* ML syntax */ |
197 |
||
198 |
val ML_KEYWORD = "ML_keyword" |
|
37195 | 199 |
val ML_DELIMITER = "ML_delimiter" |
30615 | 200 |
val ML_IDENT = "ML_ident" |
201 |
val ML_TVAR = "ML_tvar" |
|
202 |
val ML_NUMERAL = "ML_numeral" |
|
203 |
val ML_CHAR = "ML_char" |
|
204 |
val ML_STRING = "ML_string" |
|
205 |
val ML_COMMENT = "ML_comment" |
|
206 |
val ML_MALFORMED = "ML_malformed" |
|
207 |
||
30702 | 208 |
val ML_DEF = "ML_def" |
31472 | 209 |
val ML_OPEN = "ML_open" |
210 |
val ML_STRUCT = "ML_struct" |
|
30702 | 211 |
val ML_TYPING = "ML_typing" |
212 |
||
30615 | 213 |
|
29184 | 214 |
/* outer syntax */ |
215 |
||
216 |
val KEYWORD_DECL = "keyword_decl" |
|
217 |
val COMMAND_DECL = "command_decl" |
|
218 |
||
219 |
val KEYWORD = "keyword" |
|
37194 | 220 |
val OPERATOR = "operator" |
29184 | 221 |
val COMMAND = "command" |
222 |
val IDENT = "ident" |
|
223 |
val STRING = "string" |
|
224 |
val ALTSTRING = "altstring" |
|
225 |
val VERBATIM = "verbatim" |
|
226 |
val COMMENT = "comment" |
|
227 |
val CONTROL = "control" |
|
228 |
val MALFORMED = "malformed" |
|
229 |
||
29185 | 230 |
val COMMAND_SPAN = "command_span" |
231 |
val IGNORED_SPAN = "ignored_span" |
|
232 |
val MALFORMED_SPAN = "malformed_span" |
|
233 |
||
29184 | 234 |
|
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
235 |
/* timing */ |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
236 |
|
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
237 |
val TIMING = "timing" |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
238 |
val ELAPSED = "elapsed" |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
239 |
val CPU = "cpu" |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
240 |
val GC = "gc" |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
241 |
|
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
242 |
object Timing |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
243 |
{ |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
244 |
def apply(timing: isabelle.Timing): Markup = |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
245 |
Markup(TIMING, List( |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset
|
246 |
(ELAPSED, Double(timing.elapsed.seconds)), |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset
|
247 |
(CPU, Double(timing.cpu.seconds)), |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset
|
248 |
(GC, Double(timing.gc.seconds)))) |
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
249 |
def unapply(markup: Markup): Option[isabelle.Timing] = |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
250 |
markup match { |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
251 |
case Markup(TIMING, List( |
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset
|
252 |
(ELAPSED, Double(elapsed)), (CPU, Double(cpu)), (GC, Double(gc)))) => |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset
|
253 |
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) |
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
254 |
case _ => None |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
255 |
} |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
256 |
} |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
257 |
|
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
258 |
|
29184 | 259 |
/* toplevel */ |
260 |
||
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
261 |
val SUBGOALS = "subgoals" |
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
262 |
val PROOF_STATE = "proof_state" |
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
263 |
|
29184 | 264 |
val STATE = "state" |
265 |
val SUBGOAL = "subgoal" |
|
266 |
val SENDBACK = "sendback" |
|
267 |
val HILITE = "hilite" |
|
268 |
||
269 |
||
270 |
/* command status */ |
|
271 |
||
29417 | 272 |
val TASK = "task" |
273 |
||
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset
|
274 |
val FORKED = "forked" |
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset
|
275 |
val JOINED = "joined" |
29184 | 276 |
val FAILED = "failed" |
277 |
val FINISHED = "finished" |
|
29488 | 278 |
|
279 |
||
280 |
/* interactive documents */ |
|
281 |
||
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
282 |
val VERSION = "version" |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
283 |
val EXEC = "exec" |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
284 |
val ASSIGN = "assign" |
29488 | 285 |
val EDIT = "edit" |
29184 | 286 |
|
27970 | 287 |
|
288 |
/* messages */ |
|
289 |
||
38872 | 290 |
val Serial = new Long_Property("serial") |
27970 | 291 |
|
29195 | 292 |
val MESSAGE = "message" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
293 |
|
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
294 |
val INIT = "init" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
295 |
val STATUS = "status" |
39525 | 296 |
val REPORT = "report" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
297 |
val WRITELN = "writeln" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
298 |
val TRACING = "tracing" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
299 |
val WARNING = "warning" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
300 |
val ERROR = "error" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
301 |
val SYSTEM = "system" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
302 |
val STDOUT = "stdout" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
303 |
val EXIT = "exit" |
29195 | 304 |
|
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39171
diff
changeset
|
305 |
val NO_REPORT = "no_report" |
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39171
diff
changeset
|
306 |
|
39171
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset
|
307 |
val BAD = "bad" |
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset
|
308 |
|
39591 | 309 |
val READY = "ready" |
31384
ce169bd37fc0
IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents:
30702
diff
changeset
|
310 |
|
27970 | 311 |
|
34119 | 312 |
/* system data */ |
27970 | 313 |
|
38231 | 314 |
val Data = Markup("data", Nil) |
27958 | 315 |
} |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset
|
316 |
|
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset
|
317 |
sealed case class Markup(name: String, properties: List[(String, String)]) |