author | wenzelm |
Sat, 06 Jun 2009 19:58:10 +0200 | |
changeset 31472 | d7929d74acb4 |
parent 31384 | ce169bd37fc0 |
child 32450 | 375db037f4d2 |
permissions | -rw-r--r-- |
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@27958 | 9 |
object Markup { |
wenzelm@27970 | 10 |
|
wenzelm@29184 | 11 |
/* name */ |
wenzelm@29184 | 12 |
|
wenzelm@29184 | 13 |
val NAME = "name" |
wenzelm@29184 | 14 |
val KIND = "kind" |
wenzelm@29184 | 15 |
|
wenzelm@29184 | 16 |
|
wenzelm@27970 | 17 |
/* position */ |
wenzelm@27970 | 18 |
|
wenzelm@27970 | 19 |
val LINE = "line" |
wenzelm@27970 | 20 |
val COLUMN = "column" |
wenzelm@27970 | 21 |
val OFFSET = "offset" |
wenzelm@27970 | 22 |
val END_LINE = "end_line" |
wenzelm@27970 | 23 |
val END_COLUMN = "end_column" |
wenzelm@27970 | 24 |
val END_OFFSET = "end_offset" |
wenzelm@27970 | 25 |
val FILE = "file" |
wenzelm@27970 | 26 |
val ID = "id" |
wenzelm@27970 | 27 |
|
wenzelm@29205 | 28 |
val POSITION_PROPERTIES = Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID) |
wenzelm@29205 | 29 |
|
wenzelm@29184 | 30 |
val POSITION = "position" |
wenzelm@29184 | 31 |
val LOCATION = "location" |
wenzelm@29184 | 32 |
|
wenzelm@29184 | 33 |
|
wenzelm@29184 | 34 |
/* logical entities */ |
wenzelm@29184 | 35 |
|
wenzelm@29184 | 36 |
val TCLASS = "tclass" |
wenzelm@29184 | 37 |
val TYCON = "tycon" |
wenzelm@29184 | 38 |
val FIXED_DECL = "fixed_decl" |
wenzelm@29184 | 39 |
val FIXED = "fixed" |
wenzelm@29184 | 40 |
val CONST_DECL = "const_decl" |
wenzelm@29184 | 41 |
val CONST = "const" |
wenzelm@29184 | 42 |
val FACT_DECL = "fact_decl" |
wenzelm@29184 | 43 |
val FACT = "fact" |
wenzelm@29184 | 44 |
val DYNAMIC_FACT = "dynamic_fact" |
wenzelm@29184 | 45 |
val LOCAL_FACT_DECL = "local_fact_decl" |
wenzelm@29184 | 46 |
val LOCAL_FACT = "local_fact" |
wenzelm@29184 | 47 |
|
wenzelm@29184 | 48 |
|
wenzelm@29184 | 49 |
/* inner syntax */ |
wenzelm@29184 | 50 |
|
wenzelm@29184 | 51 |
val TFREE = "tfree" |
wenzelm@29184 | 52 |
val TVAR = "tvar" |
wenzelm@29184 | 53 |
val FREE = "free" |
wenzelm@29184 | 54 |
val SKOLEM = "skolem" |
wenzelm@29184 | 55 |
val BOUND = "bound" |
wenzelm@29184 | 56 |
val VAR = "var" |
wenzelm@29184 | 57 |
val NUM = "num" |
wenzelm@29184 | 58 |
val FLOAT = "float" |
wenzelm@29184 | 59 |
val XNUM = "xnum" |
wenzelm@29184 | 60 |
val XSTR = "xstr" |
wenzelm@29184 | 61 |
val LITERAL = "literal" |
wenzelm@29184 | 62 |
val INNER_COMMENT = "inner_comment" |
wenzelm@29184 | 63 |
|
wenzelm@29184 | 64 |
val SORT = "sort" |
wenzelm@29184 | 65 |
val TYP = "typ" |
wenzelm@29184 | 66 |
val TERM = "term" |
wenzelm@29184 | 67 |
val PROP = "prop" |
wenzelm@29184 | 68 |
|
wenzelm@29184 | 69 |
val ATTRIBUTE = "attribute" |
wenzelm@29184 | 70 |
val METHOD = "method" |
wenzelm@29184 | 71 |
|
wenzelm@29184 | 72 |
|
wenzelm@29184 | 73 |
/* embedded source text */ |
wenzelm@29184 | 74 |
|
wenzelm@29184 | 75 |
val ML_SOURCE = "ML_source" |
wenzelm@29184 | 76 |
val DOC_SOURCE = "doc_source" |
wenzelm@29184 | 77 |
|
wenzelm@29184 | 78 |
val ANTIQ = "antiq" |
wenzelm@29184 | 79 |
val ML_ANTIQ = "ML_antiq" |
wenzelm@29184 | 80 |
val DOC_ANTIQ = "doc_antiq" |
wenzelm@29184 | 81 |
|
wenzelm@29184 | 82 |
|
wenzelm@30615 | 83 |
/* ML syntax */ |
wenzelm@30615 | 84 |
|
wenzelm@30615 | 85 |
val ML_KEYWORD = "ML_keyword" |
wenzelm@30615 | 86 |
val ML_IDENT = "ML_ident" |
wenzelm@30615 | 87 |
val ML_TVAR = "ML_tvar" |
wenzelm@30615 | 88 |
val ML_NUMERAL = "ML_numeral" |
wenzelm@30615 | 89 |
val ML_CHAR = "ML_char" |
wenzelm@30615 | 90 |
val ML_STRING = "ML_string" |
wenzelm@30615 | 91 |
val ML_COMMENT = "ML_comment" |
wenzelm@30615 | 92 |
val ML_MALFORMED = "ML_malformed" |
wenzelm@30615 | 93 |
|
wenzelm@30704 | 94 |
val ML_DEF = "ML_def" |
wenzelm@31472 | 95 |
val ML_OPEN = "ML_open" |
wenzelm@31472 | 96 |
val ML_STRUCT = "ML_struct" |
wenzelm@30704 | 97 |
val ML_REF = "ML_ref" |
wenzelm@30704 | 98 |
val ML_TYPING = "ML_typing" |
wenzelm@30704 | 99 |
|
wenzelm@30615 | 100 |
|
wenzelm@29184 | 101 |
/* outer syntax */ |
wenzelm@29184 | 102 |
|
wenzelm@29184 | 103 |
val KEYWORD_DECL = "keyword_decl" |
wenzelm@29184 | 104 |
val COMMAND_DECL = "command_decl" |
wenzelm@29184 | 105 |
|
wenzelm@29184 | 106 |
val KEYWORD = "keyword" |
wenzelm@29184 | 107 |
val COMMAND = "command" |
wenzelm@29184 | 108 |
val IDENT = "ident" |
wenzelm@29184 | 109 |
val STRING = "string" |
wenzelm@29184 | 110 |
val ALTSTRING = "altstring" |
wenzelm@29184 | 111 |
val VERBATIM = "verbatim" |
wenzelm@29184 | 112 |
val COMMENT = "comment" |
wenzelm@29184 | 113 |
val CONTROL = "control" |
wenzelm@29184 | 114 |
val MALFORMED = "malformed" |
wenzelm@29184 | 115 |
|
wenzelm@29185 | 116 |
val COMMAND_SPAN = "command_span" |
wenzelm@29185 | 117 |
val IGNORED_SPAN = "ignored_span" |
wenzelm@29185 | 118 |
val MALFORMED_SPAN = "malformed_span" |
wenzelm@29185 | 119 |
|
wenzelm@29184 | 120 |
|
wenzelm@29184 | 121 |
/* toplevel */ |
wenzelm@29184 | 122 |
|
wenzelm@29184 | 123 |
val STATE = "state" |
wenzelm@29184 | 124 |
val SUBGOAL = "subgoal" |
wenzelm@29184 | 125 |
val SENDBACK = "sendback" |
wenzelm@29184 | 126 |
val HILITE = "hilite" |
wenzelm@29184 | 127 |
|
wenzelm@29184 | 128 |
|
wenzelm@29184 | 129 |
/* command status */ |
wenzelm@29184 | 130 |
|
wenzelm@29418 | 131 |
val TASK = "task" |
wenzelm@29418 | 132 |
|
wenzelm@29184 | 133 |
val UNPROCESSED = "unprocessed" |
wenzelm@29184 | 134 |
val RUNNING = "running" |
wenzelm@29184 | 135 |
val FAILED = "failed" |
wenzelm@29184 | 136 |
val FINISHED = "finished" |
wenzelm@29184 | 137 |
val DISPOSED = "disposed" |
wenzelm@29488 | 138 |
|
wenzelm@29488 | 139 |
|
wenzelm@29488 | 140 |
/* interactive documents */ |
wenzelm@29488 | 141 |
|
wenzelm@29488 | 142 |
val EDITS = "edits" |
wenzelm@29488 | 143 |
val EDIT = "edit" |
wenzelm@29184 | 144 |
|
wenzelm@27970 | 145 |
|
wenzelm@27970 | 146 |
/* messages */ |
wenzelm@27970 | 147 |
|
wenzelm@27970 | 148 |
val PID = "pid" |
wenzelm@27970 | 149 |
val SESSION = "session" |
wenzelm@27970 | 150 |
|
wenzelm@29195 | 151 |
val MESSAGE = "message" |
wenzelm@29522 | 152 |
val CLASS = "class" |
wenzelm@29522 | 153 |
|
wenzelm@29522 | 154 |
val INIT = "init" |
wenzelm@29522 | 155 |
val STATUS = "status" |
wenzelm@29522 | 156 |
val WRITELN = "writeln" |
wenzelm@29522 | 157 |
val PRIORITY = "priority" |
wenzelm@29522 | 158 |
val TRACING = "tracing" |
wenzelm@29522 | 159 |
val WARNING = "warning" |
wenzelm@29522 | 160 |
val ERROR = "error" |
wenzelm@29522 | 161 |
val DEBUG = "debug" |
wenzelm@29522 | 162 |
val SYSTEM = "system" |
wenzelm@29522 | 163 |
val STDIN = "stdin" |
wenzelm@29522 | 164 |
val STDOUT = "stdout" |
wenzelm@29522 | 165 |
val SIGNAL = "signal" |
wenzelm@29522 | 166 |
val EXIT = "exit" |
wenzelm@29195 | 167 |
|
wenzelm@31384 | 168 |
val READY = "ready" |
wenzelm@31384 | 169 |
|
wenzelm@27970 | 170 |
|
wenzelm@27970 | 171 |
/* content */ |
wenzelm@27970 | 172 |
|
wenzelm@27958 | 173 |
val ROOT = "root" |
wenzelm@27958 | 174 |
val RAW = "raw" |
wenzelm@27970 | 175 |
val BAD = "bad" |
wenzelm@27958 | 176 |
} |