added ML_antiq, doc_antiq;
authorwenzelm
Fri, 15 Aug 2008 17:03:52 +0200
changeset 27894 a06f78f917e0
parent 27893 7c97cf70d663
child 27895 e4f8763b971b
added ML_antiq, doc_antiq;
src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Fri Aug 15 16:08:08 2008 +0200
+++ b/src/Pure/General/markup.ML	Fri Aug 15 17:03:52 2008 +0200
@@ -65,6 +65,8 @@
   val ML_sourceN: string val ML_source: T
   val doc_sourceN: string val doc_source: T
   val antiqN: string val antiq: T
+  val ML_antiqN: string val ML_antiq: string -> T
+  val doc_antiqN: string val doc_antiq: string -> 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
@@ -209,6 +211,8 @@
 val (doc_sourceN, doc_source) = markup_elem "doc_source";
 
 val (antiqN, antiq) = markup_elem "antiq";
+val (ML_antiqN, ML_antiq) = markup_string "ML_antiq" nameN;
+val (doc_antiqN, doc_antiq) = markup_string "doc_antiq" nameN;
 
 
 (* outer syntax *)