# HG changeset patch
# User wenzelm
# Date 1218737620 -7200
# Node ID 1b46d9ec3788eee484ff7da8bc12eddfc1826abb
# Parent  f0364f1c0ecfa01e235725cc4f34faf2e0fa17ae
added ML_source, doc_source;

diff -r f0364f1c0ecf -r 1b46d9ec3788 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Thu Aug 14 19:52:40 2008 +0200
+++ b/src/Pure/General/markup.ML	Thu Aug 14 20:13:40 2008 +0200
@@ -60,6 +60,8 @@
   val propN: string val prop: T
   val attributeN: string val attribute: string -> T
   val methodN: string val method: string -> T
+  val ML_sourceN: string val ML_source: T
+  val doc_sourceN: string val doc_source: T
   val keyword_declN: string val keyword_decl: string -> T
   val command_declN: string val command_decl: string -> string -> T
   val keywordN: string val keyword: string -> T
@@ -195,6 +197,12 @@
 val (methodN, method) = markup_string "method" nameN;
 
 
+(* embedded source text *)
+
+val (ML_sourceN, ML_source) = markup_elem "ML_source";
+val (doc_sourceN, doc_source) = markup_elem "doc_source";
+
+
 (* outer syntax *)
 
 val (keyword_declN, keyword_decl) = markup_string "keyword_decl" nameN;