1.1 --- a/src/Pure/General/markup.ML	Fri Mar 20 20:21:38 2009 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Fri Mar 20 20:22:13 2009 +0100
     1.3 @@ -62,6 +62,14 @@
     1.4    val propN: string val prop: T
     1.5    val attributeN: string val attribute: string -> T
     1.6    val methodN: string val method: string -> T
     1.7 +  val ML_keywordN: string val ML_keyword: T
     1.8 +  val ML_identN: string val ML_ident: T
     1.9 +  val ML_tvarN: string val ML_tvar: T
    1.10 +  val ML_numeralN: string val ML_numeral: T
    1.11 +  val ML_charN: string val ML_char: T
    1.12 +  val ML_stringN: string val ML_string: T
    1.13 +  val ML_commentN: string val ML_comment: T
    1.14 +  val ML_malformedN: string val ML_malformed: T
    1.15    val ML_sourceN: string val ML_source: T
    1.16    val doc_sourceN: string val doc_source: T
    1.17    val antiqN: string val antiq: T
    1.18 @@ -213,6 +221,18 @@
    1.19  val (methodN, method) = markup_string "method" nameN;
    1.20  
    1.21  
    1.22 +(* ML syntax *)
    1.23 +
    1.24 +val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
    1.25 +val (ML_identN, ML_ident) = markup_elem "ML_ident";
    1.26 +val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
    1.27 +val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";
    1.28 +val (ML_charN, ML_char) = markup_elem "ML_char";
    1.29 +val (ML_stringN, ML_string) = markup_elem "ML_string";
    1.30 +val (ML_commentN, ML_comment) = markup_elem "ML_comment";
    1.31 +val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
    1.32 +
    1.33 +
    1.34  (* embedded source text *)
    1.35  
    1.36  val (ML_sourceN, ML_source) = markup_elem "ML_source";