# HG changeset patch
# User wenzelm
# Date 1230478767 -3600
# Node ID 85889d58b5da55af6c6e70c16968ff030687eb58
# Parent  f1648e009dc111245ba28ff656f1e5e84a593924
more markup elements;

diff -r f1648e009dc1 -r 85889d58b5da src/Pure/General/markup.scala
--- 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 */