author | wenzelm |
Fri, 16 Jan 2009 22:56:12 +0100 | |
changeset 29522 | 793766d4c1b5 |
parent 29488 | 8fc3aeece219 |
child 30615 | f1275196df16 |
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 |
||
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 |
||
29205 | 28 |
val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID) |
29 |
||
29184 | 30 |
val POSITION = "position" |
31 |
val LOCATION = "location" |
|
32 |
||
33 |
||
34 |
/* logical entities */ |
|
35 |
||
36 |
val TCLASS = "tclass" |
|
37 |
val TYCON = "tycon" |
|
38 |
val FIXED_DECL = "fixed_decl" |
|
39 |
val FIXED = "fixed" |
|
40 |
val CONST_DECL = "const_decl" |
|
41 |
val CONST = "const" |
|
42 |
val FACT_DECL = "fact_decl" |
|
43 |
val FACT = "fact" |
|
44 |
val DYNAMIC_FACT = "dynamic_fact" |
|
45 |
val LOCAL_FACT_DECL = "local_fact_decl" |
|
46 |
val LOCAL_FACT = "local_fact" |
|
47 |
||
48 |
||
49 |
/* inner syntax */ |
|
50 |
||
51 |
val TFREE = "tfree" |
|
52 |
val TVAR = "tvar" |
|
53 |
val FREE = "free" |
|
54 |
val SKOLEM = "skolem" |
|
55 |
val BOUND = "bound" |
|
56 |
val VAR = "var" |
|
57 |
val NUM = "num" |
|
58 |
val FLOAT = "float" |
|
59 |
val XNUM = "xnum" |
|
60 |
val XSTR = "xstr" |
|
61 |
val LITERAL = "literal" |
|
62 |
val INNER_COMMENT = "inner_comment" |
|
63 |
||
64 |
val SORT = "sort" |
|
65 |
val TYP = "typ" |
|
66 |
val TERM = "term" |
|
67 |
val PROP = "prop" |
|
68 |
||
69 |
val ATTRIBUTE = "attribute" |
|
70 |
val METHOD = "method" |
|
71 |
||
72 |
||
73 |
/* embedded source text */ |
|
74 |
||
75 |
val ML_SOURCE = "ML_source" |
|
76 |
val DOC_SOURCE = "doc_source" |
|
77 |
||
78 |
val ANTIQ = "antiq" |
|
79 |
val ML_ANTIQ = "ML_antiq" |
|
80 |
val DOC_ANTIQ = "doc_antiq" |
|
81 |
||
82 |
||
83 |
/* outer syntax */ |
|
84 |
||
85 |
val KEYWORD_DECL = "keyword_decl" |
|
86 |
val COMMAND_DECL = "command_decl" |
|
87 |
||
88 |
val KEYWORD = "keyword" |
|
89 |
val COMMAND = "command" |
|
90 |
val IDENT = "ident" |
|
91 |
val STRING = "string" |
|
92 |
val ALTSTRING = "altstring" |
|
93 |
val VERBATIM = "verbatim" |
|
94 |
val COMMENT = "comment" |
|
95 |
val CONTROL = "control" |
|
96 |
val MALFORMED = "malformed" |
|
97 |
||
29185 | 98 |
val COMMAND_SPAN = "command_span" |
99 |
val IGNORED_SPAN = "ignored_span" |
|
100 |
val MALFORMED_SPAN = "malformed_span" |
|
101 |
||
29184 | 102 |
|
103 |
/* toplevel */ |
|
104 |
||
105 |
val STATE = "state" |
|
106 |
val SUBGOAL = "subgoal" |
|
107 |
val SENDBACK = "sendback" |
|
108 |
val HILITE = "hilite" |
|
109 |
||
110 |
||
111 |
/* command status */ |
|
112 |
||
29417 | 113 |
val TASK = "task" |
114 |
||
29184 | 115 |
val UNPROCESSED = "unprocessed" |
116 |
val RUNNING = "running" |
|
117 |
val FAILED = "failed" |
|
118 |
val FINISHED = "finished" |
|
119 |
val DISPOSED = "disposed" |
|
29488 | 120 |
|
121 |
||
122 |
/* interactive documents */ |
|
123 |
||
124 |
val EDITS = "edits" |
|
125 |
val EDIT = "edit" |
|
29184 | 126 |
|
27970 | 127 |
|
128 |
/* messages */ |
|
129 |
||
130 |
val PID = "pid" |
|
131 |
val SESSION = "session" |
|
132 |
||
29195 | 133 |
val MESSAGE = "message" |
29522
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
134 |
val CLASS = "class" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
135 |
|
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
136 |
val INIT = "init" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
137 |
val STATUS = "status" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
138 |
val WRITELN = "writeln" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
139 |
val PRIORITY = "priority" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
140 |
val TRACING = "tracing" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
141 |
val WARNING = "warning" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
142 |
val ERROR = "error" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
143 |
val DEBUG = "debug" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
144 |
val SYSTEM = "system" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
145 |
val STDIN = "stdin" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
146 |
val STDOUT = "stdout" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
147 |
val SIGNAL = "signal" |
793766d4c1b5
moved message markup into Scala layer -- reduced redundancy;
wenzelm
parents:
29488
diff
changeset
|
148 |
val EXIT = "exit" |
29195 | 149 |
|
27970 | 150 |
|
151 |
/* content */ |
|
152 |
||
27958 | 153 |
val ROOT = "root" |
154 |
val RAW = "raw" |
|
27970 | 155 |
val BAD = "bad" |
27958 | 156 |
} |