author | wenzelm |
Thu, 25 Aug 2011 16:44:06 +0200 | |
changeset 44476 | e8a87398f35d |
parent 44298 | b8f8488704e2 |
child 44549 | 5e5e6ad3922c |
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 |
{ |
|
38474
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
12 |
/* empty */ |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
13 |
|
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
14 |
val Empty = Markup("", Nil) |
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
15 |
|
e498dc2eb576
uniform Markup.empty/Markup.Empty in ML and Scala;
wenzelm
parents:
38429
diff
changeset
|
16 |
|
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
17 |
/* misc properties */ |
29184 | 18 |
|
19 |
val NAME = "name" |
|
43780 | 20 |
val Name = new Properties.String(NAME) |
42136 | 21 |
|
29184 | 22 |
val KIND = "kind" |
43780 | 23 |
val Kind = new Properties.String(KIND) |
29184 | 24 |
|
25 |
||
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
26 |
/* formal entities */ |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
27 |
|
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
|
28 |
val BINDING = "binding" |
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
29 |
val ENTITY = "entity" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
30 |
val DEF = "def" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
31 |
val REF = "ref" |
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
32 |
|
42202 | 33 |
object Entity |
34 |
{ |
|
35 |
def unapply(markup: Markup): Option[(String, String)] = |
|
36 |
markup match { |
|
37 |
case Markup(ENTITY, props @ Kind(kind)) => |
|
38 |
props match { |
|
39 |
case Name(name) => Some(kind, name) |
|
40 |
case _ => None |
|
41 |
} |
|
42 |
case _ => None |
|
43 |
} |
|
44 |
} |
|
45 |
||
33088
757d7787b10c
markup for formal entities, with "def" or "ref" occurrences;
wenzelm
parents:
32450
diff
changeset
|
46 |
|
27970 | 47 |
/* position */ |
48 |
||
49 |
val LINE = "line" |
|
50 |
val OFFSET = "offset" |
|
51 |
val END_OFFSET = "end_offset" |
|
52 |
val FILE = "file" |
|
53 |
val ID = "id" |
|
54 |
||
42327
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
55 |
val DEF_LINE = "def_line" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
56 |
val DEF_OFFSET = "def_offset" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
57 |
val DEF_END_OFFSET = "def_end_offset" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
58 |
val DEF_FILE = "def_file" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
59 |
val DEF_ID = "def_id" |
7c7cc7590eb3
Name_Space.entry_markup: keep def position as separate properties;
wenzelm
parents:
42202
diff
changeset
|
60 |
|
43710
7270ae921cf2
discontinued odd Position.column -- left-over from attempts at PGIP implementation;
wenzelm
parents:
43673
diff
changeset
|
61 |
val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) |
43593 | 62 |
val POSITION = "position" |
29205 | 63 |
|
43593 | 64 |
|
65 |
/* path */ |
|
66 |
||
67 |
val PATH = "path" |
|
68 |
||
69 |
object Path |
|
70 |
{ |
|
71 |
def unapply(markup: Markup): Option[String] = |
|
72 |
markup match { |
|
73 |
case Markup(PATH, Name(name)) => Some(name) |
|
74 |
case _ => None |
|
75 |
} |
|
76 |
} |
|
29184 | 77 |
|
78 |
||
36683 | 79 |
/* pretty printing */ |
80 |
||
43780 | 81 |
val Indent = new Properties.Int("indent") |
36683 | 82 |
val BLOCK = "block" |
43780 | 83 |
val Width = new Properties.Int("width") |
36683 | 84 |
val BREAK = "break" |
85 |
||
86 |
||
33985 | 87 |
/* hidden text */ |
88 |
||
89 |
val HIDDEN = "hidden" |
|
90 |
||
91 |
||
29184 | 92 |
/* logical entities */ |
93 |
||
43551 | 94 |
val CLASS = "class" |
43552 | 95 |
val TYPE = "type" |
29184 | 96 |
val FIXED = "fixed" |
43552 | 97 |
val CONSTANT = "constant" |
98 |
||
29184 | 99 |
val DYNAMIC_FACT = "dynamic_fact" |
100 |
||
101 |
||
102 |
/* inner syntax */ |
|
103 |
||
104 |
val TFREE = "tfree" |
|
105 |
val TVAR = "tvar" |
|
106 |
val FREE = "free" |
|
107 |
val SKOLEM = "skolem" |
|
108 |
val BOUND = "bound" |
|
109 |
val VAR = "var" |
|
110 |
val NUM = "num" |
|
111 |
val FLOAT = "float" |
|
112 |
val XNUM = "xnum" |
|
113 |
val XSTR = "xstr" |
|
114 |
val LITERAL = "literal" |
|
43432
224006e5ac46
inner literal/delimiter corresponds to outer keyword/operator;
wenzelm
parents:
43386
diff
changeset
|
115 |
val DELIMITER = "delimiter" |
43386
4e78dd88c64f
more foreground markup, using actual CSS color names;
wenzelm
parents:
42492
diff
changeset
|
116 |
val INNER_STRING = "inner_string" |
29184 | 117 |
val INNER_COMMENT = "inner_comment" |
118 |
||
39168
e3ac771235f7
report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
wenzelm
parents:
38887
diff
changeset
|
119 |
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
|
120 |
|
29184 | 121 |
val SORT = "sort" |
122 |
val TYP = "typ" |
|
123 |
val TERM = "term" |
|
124 |
val PROP = "prop" |
|
125 |
||
126 |
val ATTRIBUTE = "attribute" |
|
127 |
val METHOD = "method" |
|
128 |
||
129 |
||
130 |
/* embedded source text */ |
|
131 |
||
132 |
val ML_SOURCE = "ML_source" |
|
133 |
val DOC_SOURCE = "doc_source" |
|
134 |
||
135 |
val ANTIQ = "antiq" |
|
43560
d1650e3720fd
ML antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43552
diff
changeset
|
136 |
val ML_ANTIQUOTATION = "ML antiquotation" |
43564
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset
|
137 |
val DOCUMENT_ANTIQUOTATION = "document antiquotation" |
9864182c6bad
document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents:
43560
diff
changeset
|
138 |
val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option" |
29184 | 139 |
|
140 |
||
30615 | 141 |
/* ML syntax */ |
142 |
||
143 |
val ML_KEYWORD = "ML_keyword" |
|
37195 | 144 |
val ML_DELIMITER = "ML_delimiter" |
30615 | 145 |
val ML_IDENT = "ML_ident" |
146 |
val ML_TVAR = "ML_tvar" |
|
147 |
val ML_NUMERAL = "ML_numeral" |
|
148 |
val ML_CHAR = "ML_char" |
|
149 |
val ML_STRING = "ML_string" |
|
150 |
val ML_COMMENT = "ML_comment" |
|
151 |
val ML_MALFORMED = "ML_malformed" |
|
152 |
||
30702 | 153 |
val ML_DEF = "ML_def" |
31472 | 154 |
val ML_OPEN = "ML_open" |
155 |
val ML_STRUCT = "ML_struct" |
|
30702 | 156 |
val ML_TYPING = "ML_typing" |
157 |
||
30615 | 158 |
|
29184 | 159 |
/* outer syntax */ |
160 |
||
161 |
val KEYWORD_DECL = "keyword_decl" |
|
162 |
val COMMAND_DECL = "command_decl" |
|
163 |
||
164 |
val KEYWORD = "keyword" |
|
37194 | 165 |
val OPERATOR = "operator" |
29184 | 166 |
val COMMAND = "command" |
167 |
val IDENT = "ident" |
|
168 |
val STRING = "string" |
|
169 |
val ALTSTRING = "altstring" |
|
170 |
val VERBATIM = "verbatim" |
|
171 |
val COMMENT = "comment" |
|
172 |
val CONTROL = "control" |
|
173 |
val MALFORMED = "malformed" |
|
174 |
||
29185 | 175 |
val COMMAND_SPAN = "command_span" |
176 |
val IGNORED_SPAN = "ignored_span" |
|
177 |
val MALFORMED_SPAN = "malformed_span" |
|
178 |
||
29184 | 179 |
|
43673
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset
|
180 |
/* theory loader */ |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset
|
181 |
|
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset
|
182 |
val LOADED_THEORY = "loaded_theory" |
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset
|
183 |
|
29eb1cd29961
Thy_Info.dependencies: ignore already loaded theories, according to initial prover session status;
wenzelm
parents:
43593
diff
changeset
|
184 |
|
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
185 |
/* timing */ |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
186 |
|
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
187 |
val TIMING = "timing" |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
188 |
val ELAPSED = "elapsed" |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
189 |
val CPU = "cpu" |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
190 |
val GC = "gc" |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
191 |
|
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
192 |
object Timing |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
193 |
{ |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
194 |
def apply(timing: isabelle.Timing): Markup = |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
195 |
Markup(TIMING, List( |
43780 | 196 |
(ELAPSED, Properties.Value.Double(timing.elapsed.seconds)), |
197 |
(CPU, Properties.Value.Double(timing.cpu.seconds)), |
|
198 |
(GC, Properties.Value.Double(timing.gc.seconds)))) |
|
40394
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
199 |
def unapply(markup: Markup): Option[isabelle.Timing] = |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
200 |
markup match { |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
201 |
case Markup(TIMING, List( |
43780 | 202 |
(ELAPSED, Properties.Value.Double(elapsed)), |
203 |
(CPU, Properties.Value.Double(cpu)), |
|
204 |
(GC, Properties.Value.Double(gc)))) => |
|
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40394
diff
changeset
|
205 |
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
|
206 |
case _ => None |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
207 |
} |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
208 |
} |
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
209 |
|
6dcb6cbf0719
somewhat more uniform timing markup in ML vs. Scala;
wenzelm
parents:
40392
diff
changeset
|
210 |
|
29184 | 211 |
/* toplevel */ |
212 |
||
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
213 |
val SUBGOALS = "subgoals" |
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
214 |
val PROOF_STATE = "proof_state" |
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38474
diff
changeset
|
215 |
|
29184 | 216 |
val STATE = "state" |
217 |
val SUBGOAL = "subgoal" |
|
218 |
val SENDBACK = "sendback" |
|
219 |
val HILITE = "hilite" |
|
220 |
||
221 |
||
222 |
/* command status */ |
|
223 |
||
29417 | 224 |
val TASK = "task" |
225 |
||
37186
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset
|
226 |
val FORKED = "forked" |
349e9223c685
explicit markup for forked goals, as indicated by Goal.fork;
wenzelm
parents:
37121
diff
changeset
|
227 |
val JOINED = "joined" |
29184 | 228 |
val FAILED = "failed" |
229 |
val FINISHED = "finished" |
|
29488 | 230 |
|
231 |
||
232 |
/* interactive documents */ |
|
233 |
||
38414
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
234 |
val VERSION = "version" |
49f1f657adc2
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
wenzelm
parents:
38355
diff
changeset
|
235 |
val ASSIGN = "assign" |
29184 | 236 |
|
27970 | 237 |
|
43721
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
238 |
/* prover process */ |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
239 |
|
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
240 |
val PROVER_COMMAND = "prover_command" |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
241 |
val PROVER_ARG = "prover_arg" |
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
242 |
|
fad8634cee62
echo prover input via raw_messages, for improved protocol tracing;
wenzelm
parents:
43710
diff
changeset
|
243 |
|
27970 | 244 |
/* messages */ |
245 |
||
43780 | 246 |
val Serial = new Properties.Long("serial") |
27970 | 247 |
|
29195 | 248 |
val MESSAGE = "message" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
249 |
|
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
250 |
val INIT = "init" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
251 |
val STATUS = "status" |
39525 | 252 |
val REPORT = "report" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
253 |
val WRITELN = "writeln" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
254 |
val TRACING = "tracing" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
255 |
val WARNING = "warning" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
256 |
val ERROR = "error" |
43746
a41f618c641d
some support for raw messages, which bypass standard Symbol/YXML decoding;
wenzelm
parents:
43721
diff
changeset
|
257 |
val RAW = "raw" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
258 |
val SYSTEM = "system" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
259 |
val STDOUT = "stdout" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
260 |
val EXIT = "exit" |
29195 | 261 |
|
39439
1c294d150ded
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
wenzelm
parents:
39171
diff
changeset
|
262 |
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
|
263 |
|
39171
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset
|
264 |
val BAD = "bad" |
525a13b9ac74
highlight bad range of nested error (here from inner parsing);
wenzelm
parents:
39168
diff
changeset
|
265 |
|
39591 | 266 |
val READY = "ready" |
31384
ce169bd37fc0
IsabelleProcess: emit status "ready" after initialization and reports;
wenzelm
parents:
30702
diff
changeset
|
267 |
|
27970 | 268 |
|
43748 | 269 |
/* raw message functions */ |
270 |
||
271 |
val FUNCTION = "function" |
|
43780 | 272 |
val Function = new Properties.String(FUNCTION) |
43748 | 273 |
|
274 |
val INVOKE_SCALA = "invoke_scala" |
|
275 |
object Invoke_Scala |
|
276 |
{ |
|
43780 | 277 |
def unapply(props: Properties.T): Option[(String, String)] = |
43748 | 278 |
props match { |
279 |
case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id)) |
|
280 |
case _ => None |
|
281 |
} |
|
282 |
} |
|
283 |
||
44298
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
284 |
val CANCEL_SCALA = "cancel_scala" |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
285 |
object Cancel_Scala |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
286 |
{ |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
287 |
def unapply(props: Properties.T): Option[String] = |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
288 |
props match { |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
289 |
case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id) |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
290 |
case _ => None |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
291 |
} |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
292 |
} |
b8f8488704e2
Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents:
43780
diff
changeset
|
293 |
|
43748 | 294 |
|
34119 | 295 |
/* system data */ |
27970 | 296 |
|
38231 | 297 |
val Data = Markup("data", Nil) |
27958 | 298 |
} |
38230
ed147003de4b
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
wenzelm
parents:
37195
diff
changeset
|
299 |
|
43780 | 300 |
sealed case class Markup(name: String, properties: Properties.T) |