src/Pure/General/markup.scala
changeset 31472 d7929d74acb4
parent 31384 ce169bd37fc0
child 32450 375db037f4d2
equal deleted inserted replaced
31471:e3987b32e401 31472:d7929d74acb4
    90   val ML_STRING = "ML_string"
    90   val ML_STRING = "ML_string"
    91   val ML_COMMENT = "ML_comment"
    91   val ML_COMMENT = "ML_comment"
    92   val ML_MALFORMED = "ML_malformed"
    92   val ML_MALFORMED = "ML_malformed"
    93 
    93 
    94   val ML_DEF = "ML_def"
    94   val ML_DEF = "ML_def"
       
    95   val ML_OPEN = "ML_open"
       
    96   val ML_STRUCT = "ML_struct"
    95   val ML_REF = "ML_ref"
    97   val ML_REF = "ML_ref"
    96   val ML_TYPING = "ML_typing"
    98   val ML_TYPING = "ML_typing"
    97 
    99 
    98 
   100 
    99   /* outer syntax */
   101   /* outer syntax */