wenzelm@27958
|
1 |
/* Title: Pure/General/markup.scala
|
wenzelm@27958
|
2 |
Author: Makarius
|
wenzelm@27958
|
3 |
|
wenzelm@27958
|
4 |
Common markup elements.
|
wenzelm@27958
|
5 |
*/
|
wenzelm@27958
|
6 |
|
wenzelm@27958
|
7 |
package isabelle
|
wenzelm@27958
|
8 |
|
wenzelm@27970
|
9 |
|
wenzelm@32450
|
10 |
object Markup
|
wenzelm@32450
|
11 |
{
|
wenzelm@38792
|
12 |
/* empty */
|
wenzelm@38792
|
13 |
|
wenzelm@38792
|
14 |
val Empty = Markup("", Nil)
|
wenzelm@38792
|
15 |
|
wenzelm@38792
|
16 |
|
wenzelm@38994
|
17 |
/* misc properties */
|
wenzelm@29184
|
18 |
|
wenzelm@29184
|
19 |
val NAME = "name"
|
wenzelm@44654
|
20 |
val Name = new Properties.String(NAME)
|
wenzelm@43009
|
21 |
|
wenzelm@29184
|
22 |
val KIND = "kind"
|
wenzelm@44654
|
23 |
val Kind = new Properties.String(KIND)
|
wenzelm@29184
|
24 |
|
wenzelm@29184
|
25 |
|
wenzelm@33093
|
26 |
/* formal entities */
|
wenzelm@33093
|
27 |
|
wenzelm@39213
|
28 |
val BINDING = "binding"
|
wenzelm@33093
|
29 |
val ENTITY = "entity"
|
wenzelm@33093
|
30 |
val DEF = "def"
|
wenzelm@33093
|
31 |
val REF = "ref"
|
wenzelm@33093
|
32 |
|
wenzelm@43083
|
33 |
object Entity
|
wenzelm@43083
|
34 |
{
|
wenzelm@43083
|
35 |
def unapply(markup: Markup): Option[(String, String)] =
|
wenzelm@43083
|
36 |
markup match {
|
wenzelm@43083
|
37 |
case Markup(ENTITY, props @ Kind(kind)) =>
|
wenzelm@43083
|
38 |
props match {
|
wenzelm@43083
|
39 |
case Name(name) => Some(kind, name)
|
wenzelm@43083
|
40 |
case _ => None
|
wenzelm@43083
|
41 |
}
|
wenzelm@43083
|
42 |
case _ => None
|
wenzelm@43083
|
43 |
}
|
wenzelm@43083
|
44 |
}
|
wenzelm@43083
|
45 |
|
wenzelm@33093
|
46 |
|
wenzelm@27970
|
47 |
/* position */
|
wenzelm@27970
|
48 |
|
wenzelm@27970
|
49 |
val LINE = "line"
|
wenzelm@27970
|
50 |
val OFFSET = "offset"
|
wenzelm@27970
|
51 |
val END_OFFSET = "end_offset"
|
wenzelm@27970
|
52 |
val FILE = "file"
|
wenzelm@27970
|
53 |
val ID = "id"
|
wenzelm@27970
|
54 |
|
wenzelm@43198
|
55 |
val DEF_LINE = "def_line"
|
wenzelm@43198
|
56 |
val DEF_OFFSET = "def_offset"
|
wenzelm@43198
|
57 |
val DEF_END_OFFSET = "def_end_offset"
|
wenzelm@43198
|
58 |
val DEF_FILE = "def_file"
|
wenzelm@43198
|
59 |
val DEF_ID = "def_id"
|
wenzelm@43198
|
60 |
|
wenzelm@44581
|
61 |
val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
|
wenzelm@44466
|
62 |
val POSITION = "position"
|
wenzelm@29205
|
63 |
|
wenzelm@44466
|
64 |
|
wenzelm@44466
|
65 |
/* path */
|
wenzelm@44466
|
66 |
|
wenzelm@44466
|
67 |
val PATH = "path"
|
wenzelm@44466
|
68 |
|
wenzelm@44466
|
69 |
object Path
|
wenzelm@44466
|
70 |
{
|
wenzelm@44466
|
71 |
def unapply(markup: Markup): Option[String] =
|
wenzelm@44466
|
72 |
markup match {
|
wenzelm@44466
|
73 |
case Markup(PATH, Name(name)) => Some(name)
|
wenzelm@44466
|
74 |
case _ => None
|
wenzelm@44466
|
75 |
}
|
wenzelm@44466
|
76 |
}
|
wenzelm@29184
|
77 |
|
wenzelm@29184
|
78 |
|
wenzelm@36721
|
79 |
/* pretty printing */
|
wenzelm@36721
|
80 |
|
wenzelm@44654
|
81 |
val Indent = new Properties.Int("indent")
|
wenzelm@36721
|
82 |
val BLOCK = "block"
|
wenzelm@44654
|
83 |
val Width = new Properties.Int("width")
|
wenzelm@36721
|
84 |
val BREAK = "break"
|
wenzelm@36721
|
85 |
|
wenzelm@36721
|
86 |
|
wenzelm@33994
|
87 |
/* hidden text */
|
wenzelm@33994
|
88 |
|
wenzelm@33994
|
89 |
val HIDDEN = "hidden"
|
wenzelm@33994
|
90 |
|
wenzelm@33994
|
91 |
|
wenzelm@29184
|
92 |
/* logical entities */
|
wenzelm@29184
|
93 |
|
wenzelm@44422
|
94 |
val CLASS = "class"
|
wenzelm@44423
|
95 |
val TYPE = "type"
|
wenzelm@29184
|
96 |
val FIXED = "fixed"
|
wenzelm@44423
|
97 |
val CONSTANT = "constant"
|
wenzelm@44423
|
98 |
|
wenzelm@29184
|
99 |
val DYNAMIC_FACT = "dynamic_fact"
|
wenzelm@29184
|
100 |
|
wenzelm@29184
|
101 |
|
wenzelm@29184
|
102 |
/* inner syntax */
|
wenzelm@29184
|
103 |
|
wenzelm@29184
|
104 |
val TFREE = "tfree"
|
wenzelm@29184
|
105 |
val TVAR = "tvar"
|
wenzelm@29184
|
106 |
val FREE = "free"
|
wenzelm@29184
|
107 |
val SKOLEM = "skolem"
|
wenzelm@29184
|
108 |
val BOUND = "bound"
|
wenzelm@29184
|
109 |
val VAR = "var"
|
wenzelm@29184
|
110 |
val NUM = "num"
|
wenzelm@29184
|
111 |
val FLOAT = "float"
|
wenzelm@29184
|
112 |
val XNUM = "xnum"
|
wenzelm@29184
|
113 |
val XSTR = "xstr"
|
wenzelm@29184
|
114 |
val LITERAL = "literal"
|
wenzelm@44304
|
115 |
val DELIMITER = "delimiter"
|
wenzelm@44257
|
116 |
val INNER_STRING = "inner_string"
|
wenzelm@29184
|
117 |
val INNER_COMMENT = "inner_comment"
|
wenzelm@29184
|
118 |
|
wenzelm@39449
|
119 |
val TOKEN_RANGE = "token_range"
|
wenzelm@39449
|
120 |
|
wenzelm@29184
|
121 |
val SORT = "sort"
|
wenzelm@29184
|
122 |
val TYP = "typ"
|
wenzelm@29184
|
123 |
val TERM = "term"
|
wenzelm@29184
|
124 |
val PROP = "prop"
|
wenzelm@29184
|
125 |
|
wenzelm@29184
|
126 |
val ATTRIBUTE = "attribute"
|
wenzelm@29184
|
127 |
val METHOD = "method"
|
wenzelm@29184
|
128 |
|
wenzelm@29184
|
129 |
|
wenzelm@29184
|
130 |
/* embedded source text */
|
wenzelm@29184
|
131 |
|
wenzelm@29184
|
132 |
val ML_SOURCE = "ML_source"
|
wenzelm@29184
|
133 |
val DOC_SOURCE = "doc_source"
|
wenzelm@29184
|
134 |
|
wenzelm@29184
|
135 |
val ANTIQ = "antiq"
|
wenzelm@44446
|
136 |
val ML_ANTIQUOTATION = "ML antiquotation"
|
wenzelm@44450
|
137 |
val DOCUMENT_ANTIQUOTATION = "document antiquotation"
|
wenzelm@44450
|
138 |
val DOCUMENT_ANTIQUOTATION_OPTION = "document antiquotation option"
|
wenzelm@29184
|
139 |
|
wenzelm@29184
|
140 |
|
wenzelm@30615
|
141 |
/* ML syntax */
|
wenzelm@30615
|
142 |
|
wenzelm@30615
|
143 |
val ML_KEYWORD = "ML_keyword"
|
wenzelm@37196
|
144 |
val ML_DELIMITER = "ML_delimiter"
|
wenzelm@30615
|
145 |
val ML_IDENT = "ML_ident"
|
wenzelm@30615
|
146 |
val ML_TVAR = "ML_tvar"
|
wenzelm@30615
|
147 |
val ML_NUMERAL = "ML_numeral"
|
wenzelm@30615
|
148 |
val ML_CHAR = "ML_char"
|
wenzelm@30615
|
149 |
val ML_STRING = "ML_string"
|
wenzelm@30615
|
150 |
val ML_COMMENT = "ML_comment"
|
wenzelm@30615
|
151 |
val ML_MALFORMED = "ML_malformed"
|
wenzelm@30615
|
152 |
|
wenzelm@30704
|
153 |
val ML_DEF = "ML_def"
|
wenzelm@31472
|
154 |
val ML_OPEN = "ML_open"
|
wenzelm@31472
|
155 |
val ML_STRUCT = "ML_struct"
|
wenzelm@30704
|
156 |
val ML_TYPING = "ML_typing"
|
wenzelm@30704
|
157 |
|
wenzelm@30615
|
158 |
|
wenzelm@29184
|
159 |
/* outer syntax */
|
wenzelm@29184
|
160 |
|
wenzelm@29184
|
161 |
val KEYWORD_DECL = "keyword_decl"
|
wenzelm@29184
|
162 |
val COMMAND_DECL = "command_decl"
|
wenzelm@29184
|
163 |
|
wenzelm@29184
|
164 |
val KEYWORD = "keyword"
|
wenzelm@37195
|
165 |
val OPERATOR = "operator"
|
wenzelm@29184
|
166 |
val COMMAND = "command"
|
wenzelm@29184
|
167 |
val IDENT = "ident"
|
wenzelm@29184
|
168 |
val STRING = "string"
|
wenzelm@29184
|
169 |
val ALTSTRING = "altstring"
|
wenzelm@29184
|
170 |
val VERBATIM = "verbatim"
|
wenzelm@29184
|
171 |
val COMMENT = "comment"
|
wenzelm@29184
|
172 |
val CONTROL = "control"
|
wenzelm@29184
|
173 |
val MALFORMED = "malformed"
|
wenzelm@29184
|
174 |
|
wenzelm@29185
|
175 |
val COMMAND_SPAN = "command_span"
|
wenzelm@29185
|
176 |
val IGNORED_SPAN = "ignored_span"
|
wenzelm@29185
|
177 |
val MALFORMED_SPAN = "malformed_span"
|
wenzelm@29185
|
178 |
|
wenzelm@29184
|
179 |
|
wenzelm@44548
|
180 |
/* theory loader */
|
wenzelm@44548
|
181 |
|
wenzelm@44548
|
182 |
val LOADED_THEORY = "loaded_theory"
|
wenzelm@44548
|
183 |
|
wenzelm@44548
|
184 |
|
wenzelm@40673
|
185 |
/* timing */
|
wenzelm@40673
|
186 |
|
wenzelm@40673
|
187 |
val TIMING = "timing"
|
wenzelm@40673
|
188 |
val ELAPSED = "elapsed"
|
wenzelm@40673
|
189 |
val CPU = "cpu"
|
wenzelm@40673
|
190 |
val GC = "gc"
|
wenzelm@40673
|
191 |
|
wenzelm@40673
|
192 |
object Timing
|
wenzelm@40673
|
193 |
{
|
wenzelm@40673
|
194 |
def apply(timing: isabelle.Timing): Markup =
|
wenzelm@40673
|
195 |
Markup(TIMING, List(
|
wenzelm@44654
|
196 |
(ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
|
wenzelm@44654
|
197 |
(CPU, Properties.Value.Double(timing.cpu.seconds)),
|
wenzelm@44654
|
198 |
(GC, Properties.Value.Double(timing.gc.seconds))))
|
wenzelm@40673
|
199 |
def unapply(markup: Markup): Option[isabelle.Timing] =
|
wenzelm@40673
|
200 |
markup match {
|
wenzelm@40673
|
201 |
case Markup(TIMING, List(
|
wenzelm@44654
|
202 |
(ELAPSED, Properties.Value.Double(elapsed)),
|
wenzelm@44654
|
203 |
(CPU, Properties.Value.Double(cpu)),
|
wenzelm@44654
|
204 |
(GC, Properties.Value.Double(gc)))) =>
|
wenzelm@41119
|
205 |
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
|
wenzelm@40673
|
206 |
case _ => None
|
wenzelm@40673
|
207 |
}
|
wenzelm@40673
|
208 |
}
|
wenzelm@40673
|
209 |
|
wenzelm@40673
|
210 |
|
wenzelm@29184
|
211 |
/* toplevel */
|
wenzelm@29184
|
212 |
|
wenzelm@38994
|
213 |
val SUBGOALS = "subgoals"
|
wenzelm@38994
|
214 |
val PROOF_STATE = "proof_state"
|
wenzelm@38994
|
215 |
|
wenzelm@29184
|
216 |
val STATE = "state"
|
wenzelm@29184
|
217 |
val SUBGOAL = "subgoal"
|
wenzelm@29184
|
218 |
val SENDBACK = "sendback"
|
wenzelm@29184
|
219 |
val HILITE = "hilite"
|
wenzelm@29184
|
220 |
|
wenzelm@29184
|
221 |
|
wenzelm@29184
|
222 |
/* command status */
|
wenzelm@29184
|
223 |
|
wenzelm@29418
|
224 |
val TASK = "task"
|
wenzelm@29418
|
225 |
|
wenzelm@37186
|
226 |
val FORKED = "forked"
|
wenzelm@37186
|
227 |
val JOINED = "joined"
|
wenzelm@29184
|
228 |
val FAILED = "failed"
|
wenzelm@29184
|
229 |
val FINISHED = "finished"
|
wenzelm@29488
|
230 |
|
wenzelm@29488
|
231 |
|
wenzelm@29488
|
232 |
/* interactive documents */
|
wenzelm@29488
|
233 |
|
wenzelm@38660
|
234 |
val VERSION = "version"
|
wenzelm@38660
|
235 |
val EXEC = "exec"
|
wenzelm@38660
|
236 |
val ASSIGN = "assign"
|
wenzelm@29488
|
237 |
val EDIT = "edit"
|
wenzelm@29184
|
238 |
|
wenzelm@27970
|
239 |
|
wenzelm@44603
|
240 |
/* prover process */
|
wenzelm@44603
|
241 |
|
wenzelm@44603
|
242 |
val PROVER_COMMAND = "prover_command"
|
wenzelm@44603
|
243 |
val PROVER_ARG = "prover_arg"
|
wenzelm@44603
|
244 |
|
wenzelm@44603
|
245 |
|
wenzelm@27970
|
246 |
/* messages */
|
wenzelm@27970
|
247 |
|
wenzelm@44654
|
248 |
val Serial = new Properties.Long("serial")
|
wenzelm@27970
|
249 |
|
wenzelm@29195
|
250 |
val MESSAGE = "message"
|
wenzelm@29522
|
251 |
|
wenzelm@29522
|
252 |
val INIT = "init"
|
wenzelm@29522
|
253 |
val STATUS = "status"
|
wenzelm@39794
|
254 |
val REPORT = "report"
|
wenzelm@29522
|
255 |
val WRITELN = "writeln"
|
wenzelm@29522
|
256 |
val TRACING = "tracing"
|
wenzelm@29522
|
257 |
val WARNING = "warning"
|
wenzelm@29522
|
258 |
val ERROR = "error"
|
wenzelm@44622
|
259 |
val RAW = "raw"
|
wenzelm@29522
|
260 |
val SYSTEM = "system"
|
wenzelm@29522
|
261 |
val STDOUT = "stdout"
|
wenzelm@29522
|
262 |
val EXIT = "exit"
|
wenzelm@29195
|
263 |
|
wenzelm@39748
|
264 |
val NO_REPORT = "no_report"
|
wenzelm@39748
|
265 |
|
wenzelm@39452
|
266 |
val BAD = "bad"
|
wenzelm@39452
|
267 |
|
wenzelm@39855
|
268 |
val READY = "ready"
|
wenzelm@31384
|
269 |
|
wenzelm@27970
|
270 |
|
wenzelm@44624
|
271 |
/* raw message functions */
|
wenzelm@44624
|
272 |
|
wenzelm@44624
|
273 |
val FUNCTION = "function"
|
wenzelm@44654
|
274 |
val Function = new Properties.String(FUNCTION)
|
wenzelm@44624
|
275 |
|
wenzelm@44624
|
276 |
val INVOKE_SCALA = "invoke_scala"
|
wenzelm@44624
|
277 |
object Invoke_Scala
|
wenzelm@44624
|
278 |
{
|
wenzelm@44654
|
279 |
def unapply(props: Properties.T): Option[(String, String)] =
|
wenzelm@44624
|
280 |
props match {
|
wenzelm@44624
|
281 |
case List((FUNCTION, INVOKE_SCALA), (NAME, name), (ID, id)) => Some((name, id))
|
wenzelm@44624
|
282 |
case _ => None
|
wenzelm@44624
|
283 |
}
|
wenzelm@44624
|
284 |
}
|
wenzelm@44624
|
285 |
|
wenzelm@45173
|
286 |
val CANCEL_SCALA = "cancel_scala"
|
wenzelm@45173
|
287 |
object Cancel_Scala
|
wenzelm@45173
|
288 |
{
|
wenzelm@45173
|
289 |
def unapply(props: Properties.T): Option[String] =
|
wenzelm@45173
|
290 |
props match {
|
wenzelm@45173
|
291 |
case List((FUNCTION, CANCEL_SCALA), (ID, id)) => Some(id)
|
wenzelm@45173
|
292 |
case _ => None
|
wenzelm@45173
|
293 |
}
|
wenzelm@45173
|
294 |
}
|
wenzelm@45173
|
295 |
|
wenzelm@44624
|
296 |
|
wenzelm@34128
|
297 |
/* system data */
|
wenzelm@27970
|
298 |
|
wenzelm@38487
|
299 |
val Data = Markup("data", Nil)
|
wenzelm@27958
|
300 |
}
|
wenzelm@38486
|
301 |
|
wenzelm@44654
|
302 |
sealed case class Markup(name: String, properties: Properties.T)
|