1 /* Title: Pure/General/markup.scala |
1 /* Title: Pure/General/markup.scala |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Common markup elements. |
4 Generic markup elements. |
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Markup |
10 object Markup |
11 { |
11 { |
12 /* empty */ |
12 /* properties */ |
13 |
|
14 val Empty = Markup("", Nil) |
|
15 |
|
16 |
|
17 /* misc properties */ |
|
18 |
13 |
19 val NAME = "name" |
14 val NAME = "name" |
20 val Name = new Properties.String(NAME) |
15 val Name = new Properties.String(NAME) |
21 |
16 |
22 val KIND = "kind" |
17 val KIND = "kind" |
23 val Kind = new Properties.String(KIND) |
18 val Kind = new Properties.String(KIND) |
24 |
19 |
25 |
20 |
26 /* formal entities */ |
21 /* elements */ |
27 |
22 |
28 val BINDING = "binding" |
23 val Empty = Markup("", Nil) |
29 val ENTITY = "entity" |
24 val Data = Markup("data", Nil) |
30 val DEF = "def" |
25 val Broken = Markup("broken", Nil) |
31 val REF = "ref" |
|
32 |
|
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 |
|
46 |
|
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 |
|
55 val DEF_LINE = "def_line" |
|
56 val DEF_OFFSET = "def_offset" |
|
57 val DEF_END_OFFSET = "def_end_offset" |
|
58 val DEF_FILE = "def_file" |
|
59 val DEF_ID = "def_id" |
|
60 |
|
61 val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID) |
|
62 val POSITION = "position" |
|
63 |
|
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 } |
|
77 |
|
78 |
|
79 /* pretty printing */ |
|
80 |
|
81 val Indent = new Properties.Int("indent") |
|
82 val BLOCK = "block" |
|
83 val Width = new Properties.Int("width") |
|
84 val BREAK = "break" |
|
85 |
|
86 |
|
87 /* hidden text */ |
|
88 |
|
89 val HIDDEN = "hidden" |
|
90 |
|
91 |
|
92 /* logical entities */ |
|
93 |
|
94 val CLASS = "class" |
|
95 val TYPE = "type" |
|
96 val FIXED = "fixed" |
|
97 val CONSTANT = "constant" |
|
98 |
|
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" |
|
115 val DELIMITER = "delimiter" |
|
116 val INNER_STRING = "inner_string" |
|
117 val INNER_COMMENT = "inner_comment" |
|
118 |
|
119 val TOKEN_RANGE = "token_range" |
|
120 |
|
121 val SORT = "sort" |
|
122 val TYP = "typ" |
|
123 val TERM = "term" |
|
124 val PROP = "prop" |
|
125 |
|
126 val TYPING = "typing" |
|
127 |
|
128 val ATTRIBUTE = "attribute" |
|
129 val METHOD = "method" |
|
130 |
|
131 |
|
132 /* embedded source text */ |
|
133 |
|
134 val ML_SOURCE = "ML_source" |
|
135 val DOC_SOURCE = "doc_source" |
|
136 |
|
137 val ANTIQ = "antiq" |
|
138 val ML_ANTIQUOTATION = "ML antiquotation" |
|
139 val DOCUMENT_ANTIQUOTATION = "document antiquotation" |
|
140 val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option" |
|
141 |
|
142 |
|
143 /* ML syntax */ |
|
144 |
|
145 val ML_KEYWORD = "ML_keyword" |
|
146 val ML_DELIMITER = "ML_delimiter" |
|
147 val ML_TVAR = "ML_tvar" |
|
148 val ML_NUMERAL = "ML_numeral" |
|
149 val ML_CHAR = "ML_char" |
|
150 val ML_STRING = "ML_string" |
|
151 val ML_COMMENT = "ML_comment" |
|
152 val ML_MALFORMED = "ML_malformed" |
|
153 |
|
154 val ML_DEF = "ML_def" |
|
155 val ML_OPEN = "ML_open" |
|
156 val ML_STRUCT = "ML_struct" |
|
157 val ML_TYPING = "ML_typing" |
|
158 |
|
159 |
|
160 /* outer syntax */ |
|
161 |
|
162 val KEYWORD_DECL = "keyword_decl" |
|
163 val COMMAND_DECL = "command_decl" |
|
164 |
|
165 val KEYWORD = "keyword" |
|
166 val OPERATOR = "operator" |
|
167 val COMMAND = "command" |
|
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 |
|
175 val COMMAND_SPAN = "command_span" |
|
176 val IGNORED_SPAN = "ignored_span" |
|
177 val MALFORMED_SPAN = "malformed_span" |
|
178 |
|
179 |
|
180 /* theory loader */ |
|
181 |
|
182 val LOADED_THEORY = "loaded_theory" |
|
183 |
26 |
184 |
27 |
185 /* timing */ |
28 /* timing */ |
186 |
29 |
187 val TIMING = "timing" |
30 val TIMING = "timing" |
204 (GC, Properties.Value.Double(gc)))) => |
47 (GC, Properties.Value.Double(gc)))) => |
205 Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) |
48 Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc))) |
206 case _ => None |
49 case _ => None |
207 } |
50 } |
208 } |
51 } |
|
52 } |
209 |
53 |
210 |
54 |
211 /* toplevel */ |
55 sealed case class Markup(name: String, properties: Properties.T) |
212 |
56 |
213 val SUBGOALS = "subgoals" |
|
214 val PROOF_STATE = "proof_state" |
|
215 |
|
216 val STATE = "state" |
|
217 val SUBGOAL = "subgoal" |
|
218 val SENDBACK = "sendback" |
|
219 val HILITE = "hilite" |
|
220 |
|
221 |
|
222 /* command status */ |
|
223 |
|
224 val TASK = "task" |
|
225 |
|
226 val FORKED = "forked" |
|
227 val JOINED = "joined" |
|
228 val FAILED = "failed" |
|
229 val FINISHED = "finished" |
|
230 |
|
231 |
|
232 /* interactive documents */ |
|
233 |
|
234 val VERSION = "version" |
|
235 val ASSIGN = "assign" |
|
236 |
|
237 |
|
238 /* prover process */ |
|
239 |
|
240 val PROVER_COMMAND = "prover_command" |
|
241 val PROVER_ARG = "prover_arg" |
|
242 |
|
243 |
|
244 /* messages */ |
|
245 |
|
246 val Serial = new Properties.Long("serial") |
|
247 |
|
248 val MESSAGE = "message" |
|
249 |
|
250 val INIT = "init" |
|
251 val STATUS = "status" |
|
252 val REPORT = "report" |
|
253 val WRITELN = "writeln" |
|
254 val TRACING = "tracing" |
|
255 val WARNING = "warning" |
|
256 val ERROR = "error" |
|
257 val RAW = "raw" |
|
258 val SYSTEM = "system" |
|
259 val STDOUT = "stdout" |
|
260 val STDERR = "stderr" |
|
261 val EXIT = "exit" |
|
262 |
|
263 val LEGACY = "legacy" |
|
264 |
|
265 val NO_REPORT = "no_report" |
|
266 |
|
267 val BAD = "bad" |
|
268 |
|
269 val READY = "ready" |
|
270 |
|
271 |
|
272 /* raw message functions */ |
|
273 |
|
274 val FUNCTION = "function" |
|
275 val Function = new Properties.String(FUNCTION) |
|
276 |
|
277 val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs")) |
|
278 val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions")) |
|
279 |
|
280 val INVOKE_SCALA = "invoke_scala" |
|
281 object Invoke_Scala |
|
282 { |
|
283 def unapply(props: Properties.T): Option[(String, String)] = |
|
284 props match { |
|
285 case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id)) |
|
286 case _ => None |
|
287 } |
|
288 } |
|
289 |
|
290 val CANCEL_SCALA = "cancel_scala" |
|
291 object Cancel_Scala |
|
292 { |
|
293 def unapply(props: Properties.T): Option[String] = |
|
294 props match { |
|
295 case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id) |
|
296 case _ => None |
|
297 } |
|
298 } |
|
299 |
|
300 |
|
301 /* system data */ |
|
302 |
|
303 val Data = Markup("data", Nil) |
|
304 } |
|
305 |
|
306 sealed case class Markup(name: String, properties: Properties.T) |
|