--- a/src/Pure/General/markup.scala Sat Dec 27 17:49:15 2008 +0100
+++ b/src/Pure/General/markup.scala Sun Dec 28 16:39:27 2008 +0100
@@ -8,6 +8,12 @@
object Markup {
+ /* name */
+
+ val NAME = "name"
+ val KIND = "kind"
+
+
/* position */
val LINE = "line"
@@ -19,6 +25,91 @@
val FILE = "file"
val ID = "id"
+ val POSITION = "position"
+ val LOCATION = "location"
+
+
+ /* logical entities */
+
+ val TCLASS = "tclass"
+ val TYCON = "tycon"
+ val FIXED_DECL = "fixed_decl"
+ val FIXED = "fixed"
+ val CONST_DECL = "const_decl"
+ val CONST = "const"
+ val FACT_DECL = "fact_decl"
+ val FACT = "fact"
+ val DYNAMIC_FACT = "dynamic_fact"
+ val LOCAL_FACT_DECL = "local_fact_decl"
+ val LOCAL_FACT = "local_fact"
+
+
+ /* inner syntax */
+
+ val TFREE = "tfree"
+ val TVAR = "tvar"
+ val FREE = "free"
+ val SKOLEM = "skolem"
+ val BOUND = "bound"
+ val VAR = "var"
+ val NUM = "num"
+ val FLOAT = "float"
+ val XNUM = "xnum"
+ val XSTR = "xstr"
+ val LITERAL = "literal"
+ val INNER_COMMENT = "inner_comment"
+
+ val SORT = "sort"
+ val TYP = "typ"
+ val TERM = "term"
+ val PROP = "prop"
+
+ val ATTRIBUTE = "attribute"
+ val METHOD = "method"
+
+
+ /* embedded source text */
+
+ val ML_SOURCE = "ML_source"
+ val DOC_SOURCE = "doc_source"
+
+ val ANTIQ = "antiq"
+ val ML_ANTIQ = "ML_antiq"
+ val DOC_ANTIQ = "doc_antiq"
+
+
+ /* outer syntax */
+
+ val KEYWORD_DECL = "keyword_decl"
+ val COMMAND_DECL = "command_decl"
+
+ val KEYWORD = "keyword"
+ val COMMAND = "command"
+ val IDENT = "ident"
+ val STRING = "string"
+ val ALTSTRING = "altstring"
+ val VERBATIM = "verbatim"
+ val COMMENT = "comment"
+ val CONTROL = "control"
+ val MALFORMED = "malformed"
+
+
+ /* toplevel */
+
+ val STATE = "state"
+ val SUBGOAL = "subgoal"
+ val SENDBACK = "sendback"
+ val HILITE = "hilite"
+
+
+ /* command status */
+
+ val UNPROCESSED = "unprocessed"
+ val RUNNING = "running"
+ val FAILED = "failed"
+ val FINISHED = "finished"
+ val DISPOSED = "disposed"
+
/* messages */