1.1 --- a/src/Pure/General/markup.ML	Sat Jun 06 19:58:10 2009 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Sat Jun 06 19:58:10 2009 +0200
     1.3 @@ -71,6 +71,8 @@
     1.4    val ML_commentN: string val ML_comment: T
     1.5    val ML_malformedN: string val ML_malformed: T
     1.6    val ML_defN: string val ML_def: T
     1.7 +  val ML_openN: string val ML_open: T
     1.8 +  val ML_structN: string val ML_struct: T
     1.9    val ML_refN: string val ML_ref: T
    1.10    val ML_typingN: string val ML_typing: T
    1.11    val ML_sourceN: string val ML_source: T
    1.12 @@ -237,6 +239,8 @@
    1.13  val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
    1.14  
    1.15  val (ML_defN, ML_def) = markup_elem "ML_def";
    1.16 +val (ML_openN, ML_open) = markup_elem "ML_open";
    1.17 +val (ML_structN, ML_struct) = markup_elem "ML_struct";
    1.18  val (ML_refN, ML_ref) = markup_elem "ML_ref";
    1.19  val (ML_typingN, ML_typing) = markup_elem "ML_typing";
    1.20  

     2.1 --- a/src/Pure/General/markup.scala	Sat Jun 06 19:58:10 2009 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Sat Jun 06 19:58:10 2009 +0200
     2.3 @@ -92,6 +92,8 @@
     2.4    val ML_MALFORMED = "ML_malformed"
     2.5  
     2.6    val ML_DEF = "ML_def"
     2.7 +  val ML_OPEN = "ML_open"
     2.8 +  val ML_STRUCT = "ML_struct"
     2.9    val ML_REF = "ML_ref"
    2.10    val ML_TYPING = "ML_typing"
    2.11