# HG changeset patch
# User wenzelm
# Date 1237905793 -3600
# Node ID 274626e2b2dd56c2ad8a4846fc82134e09678887
# Parent  9ae91c0d3d1b966a246acac65fda0d4ea81087d8
more markup elements for ML programs;

diff -r 9ae91c0d3d1b -r 274626e2b2dd src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Tue Mar 24 13:20:40 2009 +0100
+++ b/src/Pure/General/markup.ML	Tue Mar 24 15:43:13 2009 +0100
@@ -70,6 +70,9 @@
   val ML_stringN: string val ML_string: T
   val ML_commentN: string val ML_comment: T
   val ML_malformedN: string val ML_malformed: T
+  val ML_defN: string val ML_def: T
+  val ML_refN: string val ML_ref: T
+  val ML_typingN: string val ML_typing: T
   val ML_sourceN: string val ML_source: T
   val doc_sourceN: string val doc_source: T
   val antiqN: string val antiq: T
@@ -232,6 +235,10 @@
 val (ML_commentN, ML_comment) = markup_elem "ML_comment";
 val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
 
+val (ML_defN, ML_def) = markup_elem "ML_def";
+val (ML_refN, ML_ref) = markup_elem "ML_ref";
+val (ML_typingN, ML_typing) = markup_elem "ML_typing";
+
 
 (* embedded source text *)
 
diff -r 9ae91c0d3d1b -r 274626e2b2dd src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Tue Mar 24 13:20:40 2009 +0100
+++ b/src/Pure/General/markup.scala	Tue Mar 24 15:43:13 2009 +0100
@@ -91,6 +91,10 @@
   val ML_COMMENT = "ML_comment"
   val ML_MALFORMED = "ML_malformed"
 
+  val ML_DEF = "ML_def"
+  val ML_REF = "ML_ref"
+  val ML_TYPING = "ML_typing"
+
 
   /* outer syntax */