27958
|
1 |
/* Title: Pure/General/markup.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Common markup elements.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
object Markup {
|
27970
|
10 |
|
29184
|
11 |
/* name */
|
|
12 |
|
|
13 |
val NAME = "name"
|
|
14 |
val KIND = "kind"
|
|
15 |
|
|
16 |
|
27970
|
17 |
/* position */
|
|
18 |
|
|
19 |
val LINE = "line"
|
|
20 |
val COLUMN = "column"
|
|
21 |
val OFFSET = "offset"
|
|
22 |
val END_LINE = "end_line"
|
|
23 |
val END_COLUMN = "end_column"
|
|
24 |
val END_OFFSET = "end_offset"
|
|
25 |
val FILE = "file"
|
|
26 |
val ID = "id"
|
|
27 |
|
29184
|
28 |
val POSITION = "position"
|
|
29 |
val LOCATION = "location"
|
|
30 |
|
|
31 |
|
|
32 |
/* logical entities */
|
|
33 |
|
|
34 |
val TCLASS = "tclass"
|
|
35 |
val TYCON = "tycon"
|
|
36 |
val FIXED_DECL = "fixed_decl"
|
|
37 |
val FIXED = "fixed"
|
|
38 |
val CONST_DECL = "const_decl"
|
|
39 |
val CONST = "const"
|
|
40 |
val FACT_DECL = "fact_decl"
|
|
41 |
val FACT = "fact"
|
|
42 |
val DYNAMIC_FACT = "dynamic_fact"
|
|
43 |
val LOCAL_FACT_DECL = "local_fact_decl"
|
|
44 |
val LOCAL_FACT = "local_fact"
|
|
45 |
|
|
46 |
|
|
47 |
/* inner syntax */
|
|
48 |
|
|
49 |
val TFREE = "tfree"
|
|
50 |
val TVAR = "tvar"
|
|
51 |
val FREE = "free"
|
|
52 |
val SKOLEM = "skolem"
|
|
53 |
val BOUND = "bound"
|
|
54 |
val VAR = "var"
|
|
55 |
val NUM = "num"
|
|
56 |
val FLOAT = "float"
|
|
57 |
val XNUM = "xnum"
|
|
58 |
val XSTR = "xstr"
|
|
59 |
val LITERAL = "literal"
|
|
60 |
val INNER_COMMENT = "inner_comment"
|
|
61 |
|
|
62 |
val SORT = "sort"
|
|
63 |
val TYP = "typ"
|
|
64 |
val TERM = "term"
|
|
65 |
val PROP = "prop"
|
|
66 |
|
|
67 |
val ATTRIBUTE = "attribute"
|
|
68 |
val METHOD = "method"
|
|
69 |
|
|
70 |
|
|
71 |
/* embedded source text */
|
|
72 |
|
|
73 |
val ML_SOURCE = "ML_source"
|
|
74 |
val DOC_SOURCE = "doc_source"
|
|
75 |
|
|
76 |
val ANTIQ = "antiq"
|
|
77 |
val ML_ANTIQ = "ML_antiq"
|
|
78 |
val DOC_ANTIQ = "doc_antiq"
|
|
79 |
|
|
80 |
|
|
81 |
/* outer syntax */
|
|
82 |
|
|
83 |
val KEYWORD_DECL = "keyword_decl"
|
|
84 |
val COMMAND_DECL = "command_decl"
|
|
85 |
|
|
86 |
val KEYWORD = "keyword"
|
|
87 |
val COMMAND = "command"
|
|
88 |
val IDENT = "ident"
|
|
89 |
val STRING = "string"
|
|
90 |
val ALTSTRING = "altstring"
|
|
91 |
val VERBATIM = "verbatim"
|
|
92 |
val COMMENT = "comment"
|
|
93 |
val CONTROL = "control"
|
|
94 |
val MALFORMED = "malformed"
|
|
95 |
|
|
96 |
|
|
97 |
/* toplevel */
|
|
98 |
|
|
99 |
val STATE = "state"
|
|
100 |
val SUBGOAL = "subgoal"
|
|
101 |
val SENDBACK = "sendback"
|
|
102 |
val HILITE = "hilite"
|
|
103 |
|
|
104 |
|
|
105 |
/* command status */
|
|
106 |
|
|
107 |
val UNPROCESSED = "unprocessed"
|
|
108 |
val RUNNING = "running"
|
|
109 |
val FAILED = "failed"
|
|
110 |
val FINISHED = "finished"
|
|
111 |
val DISPOSED = "disposed"
|
|
112 |
|
27970
|
113 |
|
|
114 |
/* messages */
|
|
115 |
|
|
116 |
val PID = "pid"
|
|
117 |
val SESSION = "session"
|
|
118 |
|
|
119 |
|
|
120 |
/* content */
|
|
121 |
|
27958
|
122 |
val ROOT = "root"
|
|
123 |
val RAW = "raw"
|
27970
|
124 |
val BAD = "bad"
|
27958
|
125 |
}
|