wenzelm@46545
|
1 |
/* Title: Pure/PIDE/markup.scala
|
wenzelm@46548
|
2 |
Module: PIDE
|
wenzelm@27958
|
3 |
Author: Makarius
|
wenzelm@27958
|
4 |
|
wenzelm@51216
|
5 |
Isabelle-specific implementation of quasi-abstract markup elements.
|
wenzelm@27958
|
6 |
*/
|
wenzelm@27958
|
7 |
|
wenzelm@27958
|
8 |
package isabelle
|
wenzelm@27958
|
9 |
|
wenzelm@27970
|
10 |
|
wenzelm@32450
|
11 |
object Markup
|
wenzelm@32450
|
12 |
{
|
wenzelm@46537
|
13 |
/* properties */
|
wenzelm@29184
|
14 |
|
wenzelm@29184
|
15 |
val NAME = "name"
|
wenzelm@44654
|
16 |
val Name = new Properties.String(NAME)
|
wenzelm@43009
|
17 |
|
wenzelm@29184
|
18 |
val KIND = "kind"
|
wenzelm@44654
|
19 |
val Kind = new Properties.String(KIND)
|
wenzelm@29184
|
20 |
|
wenzelm@29184
|
21 |
|
wenzelm@51216
|
22 |
/* basic markup */
|
wenzelm@33093
|
23 |
|
wenzelm@46537
|
24 |
val Empty = Markup("", Nil)
|
wenzelm@46537
|
25 |
val Broken = Markup("broken", Nil)
|
wenzelm@51216
|
26 |
|
wenzelm@51216
|
27 |
|
wenzelm@51216
|
28 |
/* formal entities */
|
wenzelm@51216
|
29 |
|
wenzelm@51216
|
30 |
val BINDING = "binding"
|
wenzelm@51216
|
31 |
val ENTITY = "entity"
|
wenzelm@51216
|
32 |
val DEF = "def"
|
wenzelm@51216
|
33 |
val REF = "ref"
|
wenzelm@51216
|
34 |
|
wenzelm@51216
|
35 |
object Entity
|
wenzelm@51216
|
36 |
{
|
wenzelm@51216
|
37 |
def unapply(markup: Markup): Option[(String, String)] =
|
wenzelm@51216
|
38 |
markup match {
|
wenzelm@51216
|
39 |
case Markup(ENTITY, props @ Kind(kind)) =>
|
wenzelm@51216
|
40 |
props match {
|
wenzelm@51216
|
41 |
case Name(name) => Some(kind, name)
|
wenzelm@51216
|
42 |
case _ => None
|
wenzelm@51216
|
43 |
}
|
wenzelm@51216
|
44 |
case _ => None
|
wenzelm@51216
|
45 |
}
|
wenzelm@51216
|
46 |
}
|
wenzelm@51216
|
47 |
|
wenzelm@51216
|
48 |
|
wenzelm@51216
|
49 |
/* position */
|
wenzelm@51216
|
50 |
|
wenzelm@51216
|
51 |
val LINE = "line"
|
wenzelm@51216
|
52 |
val OFFSET = "offset"
|
wenzelm@51216
|
53 |
val END_OFFSET = "end_offset"
|
wenzelm@51216
|
54 |
val FILE = "file"
|
wenzelm@51216
|
55 |
val ID = "id"
|
wenzelm@51216
|
56 |
|
wenzelm@51216
|
57 |
val DEF_LINE = "def_line"
|
wenzelm@51216
|
58 |
val DEF_OFFSET = "def_offset"
|
wenzelm@51216
|
59 |
val DEF_END_OFFSET = "def_end_offset"
|
wenzelm@51216
|
60 |
val DEF_FILE = "def_file"
|
wenzelm@51216
|
61 |
val DEF_ID = "def_id"
|
wenzelm@51216
|
62 |
|
wenzelm@51216
|
63 |
val POSITION_PROPERTIES = Set(LINE, OFFSET, END_OFFSET, FILE, ID)
|
wenzelm@51216
|
64 |
val POSITION = "position"
|
wenzelm@51216
|
65 |
|
wenzelm@51216
|
66 |
|
wenzelm@51216
|
67 |
/* path */
|
wenzelm@51216
|
68 |
|
wenzelm@51216
|
69 |
val PATH = "path"
|
wenzelm@51216
|
70 |
|
wenzelm@51216
|
71 |
object Path
|
wenzelm@51216
|
72 |
{
|
wenzelm@51216
|
73 |
def unapply(markup: Markup): Option[String] =
|
wenzelm@51216
|
74 |
markup match {
|
wenzelm@51216
|
75 |
case Markup(PATH, Name(name)) => Some(name)
|
wenzelm@51216
|
76 |
case _ => None
|
wenzelm@51216
|
77 |
}
|
wenzelm@51216
|
78 |
}
|
wenzelm@51216
|
79 |
|
wenzelm@51216
|
80 |
|
wenzelm@51216
|
81 |
/* pretty printing */
|
wenzelm@51216
|
82 |
|
wenzelm@51216
|
83 |
val Indent = new Properties.Int("indent")
|
wenzelm@51216
|
84 |
val BLOCK = "block"
|
wenzelm@51216
|
85 |
val Width = new Properties.Int("width")
|
wenzelm@51216
|
86 |
val BREAK = "break"
|
wenzelm@51216
|
87 |
|
wenzelm@51216
|
88 |
val SEPARATOR = "separator"
|
wenzelm@51216
|
89 |
|
wenzelm@51216
|
90 |
|
wenzelm@51216
|
91 |
/* hidden text */
|
wenzelm@51216
|
92 |
|
wenzelm@51216
|
93 |
val HIDDEN = "hidden"
|
wenzelm@51216
|
94 |
|
wenzelm@51216
|
95 |
|
wenzelm@51216
|
96 |
/* logical entities */
|
wenzelm@51216
|
97 |
|
wenzelm@51216
|
98 |
val CLASS = "class"
|
wenzelm@51216
|
99 |
val TYPE_NAME = "type_name"
|
wenzelm@51216
|
100 |
val FIXED = "fixed"
|
wenzelm@51216
|
101 |
val CONSTANT = "constant"
|
wenzelm@51216
|
102 |
|
wenzelm@51216
|
103 |
val DYNAMIC_FACT = "dynamic_fact"
|
wenzelm@51216
|
104 |
|
wenzelm@51216
|
105 |
|
wenzelm@51216
|
106 |
/* inner syntax */
|
wenzelm@51216
|
107 |
|
wenzelm@51216
|
108 |
val TFREE = "tfree"
|
wenzelm@51216
|
109 |
val TVAR = "tvar"
|
wenzelm@51216
|
110 |
val FREE = "free"
|
wenzelm@51216
|
111 |
val SKOLEM = "skolem"
|
wenzelm@51216
|
112 |
val BOUND = "bound"
|
wenzelm@51216
|
113 |
val VAR = "var"
|
wenzelm@51216
|
114 |
val NUMERAL = "numeral"
|
wenzelm@51216
|
115 |
val LITERAL = "literal"
|
wenzelm@51216
|
116 |
val DELIMITER = "delimiter"
|
wenzelm@51216
|
117 |
val INNER_STRING = "inner_string"
|
wenzelm@51216
|
118 |
val INNER_COMMENT = "inner_comment"
|
wenzelm@51216
|
119 |
|
wenzelm@51216
|
120 |
val TOKEN_RANGE = "token_range"
|
wenzelm@51216
|
121 |
|
wenzelm@51216
|
122 |
val SORT = "sort"
|
wenzelm@51216
|
123 |
val TYP = "typ"
|
wenzelm@51216
|
124 |
val TERM = "term"
|
wenzelm@51216
|
125 |
val PROP = "prop"
|
wenzelm@51216
|
126 |
|
wenzelm@51216
|
127 |
val SORTING = "sorting"
|
wenzelm@51216
|
128 |
val TYPING = "typing"
|
wenzelm@51216
|
129 |
|
wenzelm@51216
|
130 |
val ATTRIBUTE = "attribute"
|
wenzelm@51216
|
131 |
val METHOD = "method"
|
wenzelm@51216
|
132 |
|
wenzelm@51216
|
133 |
|
wenzelm@51216
|
134 |
/* embedded source text */
|
wenzelm@51216
|
135 |
|
wenzelm@51216
|
136 |
val ML_SOURCE = "ML_source"
|
wenzelm@51216
|
137 |
val DOCUMENT_SOURCE = "document_source"
|
wenzelm@51216
|
138 |
|
wenzelm@51216
|
139 |
val ANTIQ = "antiq"
|
wenzelm@51216
|
140 |
val ML_ANTIQUOTATION = "ML_antiquotation"
|
wenzelm@51216
|
141 |
val DOCUMENT_ANTIQUOTATION = "document_antiquotation"
|
wenzelm@51216
|
142 |
val DOCUMENT_ANTIQUOTATION_OPTION = "document_antiquotation_option"
|
wenzelm@51216
|
143 |
|
wenzelm@51216
|
144 |
|
wenzelm@51216
|
145 |
/* text structure */
|
wenzelm@51216
|
146 |
|
wenzelm@51216
|
147 |
val PARAGRAPH = "paragraph"
|
wenzelm@51216
|
148 |
|
wenzelm@51216
|
149 |
|
wenzelm@51216
|
150 |
/* ML syntax */
|
wenzelm@51216
|
151 |
|
wenzelm@51216
|
152 |
val ML_KEYWORD = "ML_keyword"
|
wenzelm@51216
|
153 |
val ML_DELIMITER = "ML_delimiter"
|
wenzelm@51216
|
154 |
val ML_TVAR = "ML_tvar"
|
wenzelm@51216
|
155 |
val ML_NUMERAL = "ML_numeral"
|
wenzelm@51216
|
156 |
val ML_CHAR = "ML_char"
|
wenzelm@51216
|
157 |
val ML_STRING = "ML_string"
|
wenzelm@51216
|
158 |
val ML_COMMENT = "ML_comment"
|
wenzelm@51216
|
159 |
|
wenzelm@51216
|
160 |
val ML_DEF = "ML_def"
|
wenzelm@51216
|
161 |
val ML_OPEN = "ML_open"
|
wenzelm@51216
|
162 |
val ML_STRUCT = "ML_struct"
|
wenzelm@51216
|
163 |
val ML_TYPING = "ML_typing"
|
wenzelm@51216
|
164 |
|
wenzelm@51216
|
165 |
|
wenzelm@51216
|
166 |
/* outer syntax */
|
wenzelm@51216
|
167 |
|
wenzelm@51216
|
168 |
val KEYWORD = "keyword"
|
wenzelm@51216
|
169 |
val OPERATOR = "operator"
|
wenzelm@51216
|
170 |
val COMMAND = "command"
|
wenzelm@51216
|
171 |
val STRING = "string"
|
wenzelm@51216
|
172 |
val ALTSTRING = "altstring"
|
wenzelm@51216
|
173 |
val VERBATIM = "verbatim"
|
wenzelm@51216
|
174 |
val COMMENT = "comment"
|
wenzelm@51216
|
175 |
val CONTROL = "control"
|
wenzelm@51216
|
176 |
|
wenzelm@51216
|
177 |
val KEYWORD1 = "keyword1"
|
wenzelm@51216
|
178 |
val KEYWORD2 = "keyword2"
|
wenzelm@51216
|
179 |
|
wenzelm@51216
|
180 |
|
wenzelm@51216
|
181 |
/* timing */
|
wenzelm@51216
|
182 |
|
wenzelm@51216
|
183 |
val TIMING = "timing"
|
wenzelm@51216
|
184 |
val ELAPSED = "elapsed"
|
wenzelm@51216
|
185 |
val CPU = "cpu"
|
wenzelm@51216
|
186 |
val GC = "gc"
|
wenzelm@51216
|
187 |
|
wenzelm@51216
|
188 |
object Timing
|
wenzelm@51216
|
189 |
{
|
wenzelm@51216
|
190 |
def apply(timing: isabelle.Timing): Markup =
|
wenzelm@51216
|
191 |
Markup(TIMING, List(
|
wenzelm@51216
|
192 |
(ELAPSED, Properties.Value.Double(timing.elapsed.seconds)),
|
wenzelm@51216
|
193 |
(CPU, Properties.Value.Double(timing.cpu.seconds)),
|
wenzelm@51216
|
194 |
(GC, Properties.Value.Double(timing.gc.seconds))))
|
wenzelm@51216
|
195 |
def unapply(markup: Markup): Option[isabelle.Timing] =
|
wenzelm@51216
|
196 |
markup match {
|
wenzelm@51216
|
197 |
case Markup(TIMING, List(
|
wenzelm@51216
|
198 |
(ELAPSED, Properties.Value.Double(elapsed)),
|
wenzelm@51216
|
199 |
(CPU, Properties.Value.Double(cpu)),
|
wenzelm@51216
|
200 |
(GC, Properties.Value.Double(gc)))) =>
|
wenzelm@51216
|
201 |
Some(new isabelle.Timing(Time.seconds(elapsed), Time.seconds(cpu), Time.seconds(gc)))
|
wenzelm@51216
|
202 |
case _ => None
|
wenzelm@51216
|
203 |
}
|
wenzelm@51216
|
204 |
}
|
wenzelm@51216
|
205 |
|
wenzelm@51216
|
206 |
|
wenzelm@51216
|
207 |
/* toplevel */
|
wenzelm@51216
|
208 |
|
wenzelm@51216
|
209 |
val SUBGOALS = "subgoals"
|
wenzelm@51216
|
210 |
val PROOF_STATE = "proof_state"
|
wenzelm@51216
|
211 |
|
wenzelm@51216
|
212 |
val STATE = "state"
|
wenzelm@51216
|
213 |
val SUBGOAL = "subgoal"
|
wenzelm@51230
|
214 |
|
wenzelm@51465
|
215 |
|
wenzelm@51216
|
216 |
/* command status */
|
wenzelm@51216
|
217 |
|
wenzelm@51216
|
218 |
val TASK = "task"
|
wenzelm@51216
|
219 |
|
wenzelm@51216
|
220 |
val ACCEPTED = "accepted"
|
wenzelm@51216
|
221 |
val FORKED = "forked"
|
wenzelm@51216
|
222 |
val JOINED = "joined"
|
wenzelm@51216
|
223 |
val RUNNING = "running"
|
wenzelm@51216
|
224 |
val FINISHED = "finished"
|
wenzelm@51216
|
225 |
val FAILED = "failed"
|
wenzelm@51216
|
226 |
|
wenzelm@51216
|
227 |
|
wenzelm@51216
|
228 |
/* interactive documents */
|
wenzelm@51216
|
229 |
|
wenzelm@51216
|
230 |
val VERSION = "version"
|
wenzelm@51216
|
231 |
val ASSIGN = "assign"
|
wenzelm@51216
|
232 |
|
wenzelm@51216
|
233 |
|
wenzelm@51216
|
234 |
/* prover process */
|
wenzelm@51216
|
235 |
|
wenzelm@51216
|
236 |
val PROVER_COMMAND = "prover_command"
|
wenzelm@51216
|
237 |
val PROVER_ARG = "prover_arg"
|
wenzelm@51216
|
238 |
|
wenzelm@51216
|
239 |
|
wenzelm@51216
|
240 |
/* messages */
|
wenzelm@51216
|
241 |
|
wenzelm@51216
|
242 |
val Serial = new Properties.Long("serial")
|
wenzelm@51216
|
243 |
|
wenzelm@51216
|
244 |
val MESSAGE = "message"
|
wenzelm@51216
|
245 |
|
wenzelm@51216
|
246 |
val INIT = "init"
|
wenzelm@51216
|
247 |
val STATUS = "status"
|
wenzelm@51216
|
248 |
val REPORT = "report"
|
wenzelm@51515
|
249 |
val RESULT = "result"
|
wenzelm@51216
|
250 |
val WRITELN = "writeln"
|
wenzelm@51216
|
251 |
val TRACING = "tracing"
|
wenzelm@51216
|
252 |
val WARNING = "warning"
|
wenzelm@51216
|
253 |
val ERROR = "error"
|
wenzelm@51216
|
254 |
val PROTOCOL = "protocol"
|
wenzelm@51216
|
255 |
val SYSTEM = "system"
|
wenzelm@51216
|
256 |
val STDOUT = "stdout"
|
wenzelm@51216
|
257 |
val STDERR = "stderr"
|
wenzelm@51216
|
258 |
val EXIT = "exit"
|
wenzelm@51216
|
259 |
|
wenzelm@51216
|
260 |
val WRITELN_MESSAGE = "writeln_message"
|
wenzelm@51216
|
261 |
val TRACING_MESSAGE = "tracing_message"
|
wenzelm@51216
|
262 |
val WARNING_MESSAGE = "warning_message"
|
wenzelm@51216
|
263 |
val ERROR_MESSAGE = "error_message"
|
wenzelm@51216
|
264 |
|
wenzelm@51216
|
265 |
val message: String => String =
|
wenzelm@51216
|
266 |
Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
|
wenzelm@51516
|
267 |
WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE).withDefault((s: String) => s)
|
wenzelm@51216
|
268 |
|
wenzelm@51216
|
269 |
val Return_Code = new Properties.Int("return_code")
|
wenzelm@51216
|
270 |
|
wenzelm@51216
|
271 |
val LEGACY = "legacy"
|
wenzelm@51216
|
272 |
|
wenzelm@51216
|
273 |
val NO_REPORT = "no_report"
|
wenzelm@51216
|
274 |
|
wenzelm@51216
|
275 |
val BAD = "bad"
|
wenzelm@51216
|
276 |
|
wenzelm@51515
|
277 |
val INTENSIFY = "intensify"
|
wenzelm@51515
|
278 |
|
wenzelm@51515
|
279 |
|
wenzelm@51515
|
280 |
/* active areas */
|
wenzelm@51515
|
281 |
|
wenzelm@51515
|
282 |
val GRAPHVIEW = "graphview"
|
wenzelm@51515
|
283 |
|
wenzelm@51515
|
284 |
val SENDBACK = "sendback"
|
wenzelm@51515
|
285 |
val PADDING = "padding"
|
wenzelm@51515
|
286 |
val PADDING_LINE = (PADDING, LINE)
|
wenzelm@51515
|
287 |
|
wenzelm@51515
|
288 |
val DIALOG = "dialog"
|
wenzelm@51518
|
289 |
val Result = new Properties.String(RESULT)
|
wenzelm@51515
|
290 |
|
wenzelm@51216
|
291 |
|
wenzelm@51216
|
292 |
/* protocol message functions */
|
wenzelm@51216
|
293 |
|
wenzelm@51216
|
294 |
val FUNCTION = "function"
|
wenzelm@51216
|
295 |
val Function = new Properties.String(FUNCTION)
|
wenzelm@51216
|
296 |
|
wenzelm@51216
|
297 |
val Assign_Execs: Properties.T = List((FUNCTION, "assign_execs"))
|
wenzelm@51216
|
298 |
val Removed_Versions: Properties.T = List((FUNCTION, "removed_versions"))
|
wenzelm@51216
|
299 |
|
wenzelm@51216
|
300 |
object Invoke_Scala
|
wenzelm@51216
|
301 |
{
|
wenzelm@51216
|
302 |
def unapply(props: Properties.T): Option[(String, String)] =
|
wenzelm@51216
|
303 |
props match {
|
wenzelm@51216
|
304 |
case List((FUNCTION, "invoke_scala"), (NAME, name), (ID, id)) => Some((name, id))
|
wenzelm@51216
|
305 |
case _ => None
|
wenzelm@51216
|
306 |
}
|
wenzelm@51216
|
307 |
}
|
wenzelm@51216
|
308 |
object Cancel_Scala
|
wenzelm@51216
|
309 |
{
|
wenzelm@51216
|
310 |
def unapply(props: Properties.T): Option[String] =
|
wenzelm@51216
|
311 |
props match {
|
wenzelm@51216
|
312 |
case List((FUNCTION, "cancel_scala"), (ID, id)) => Some(id)
|
wenzelm@51216
|
313 |
case _ => None
|
wenzelm@51216
|
314 |
}
|
wenzelm@51216
|
315 |
}
|
wenzelm@51270
|
316 |
|
wenzelm@51270
|
317 |
object ML_Statistics
|
wenzelm@51270
|
318 |
{
|
wenzelm@51270
|
319 |
def unapply(props: Properties.T): Option[Properties.T] =
|
wenzelm@51270
|
320 |
props match {
|
wenzelm@51270
|
321 |
case (FUNCTION, "ML_statistics") :: stats => Some(stats)
|
wenzelm@51270
|
322 |
case _ => None
|
wenzelm@51270
|
323 |
}
|
wenzelm@51270
|
324 |
}
|
wenzelm@27958
|
325 |
}
|
wenzelm@38486
|
326 |
|
wenzelm@46537
|
327 |
|
wenzelm@44654
|
328 |
sealed case class Markup(name: String, properties: Properties.T)
|
wenzelm@46537
|
329 |
|