| changeset 31472 | d7929d74acb4 |
| parent 31384 | ce169bd37fc0 |
| child 32450 | 375db037f4d2 |
--- a/src/Pure/General/markup.scala Sat Jun 06 19:58:10 2009 +0200 +++ b/src/Pure/General/markup.scala Sat Jun 06 19:58:10 2009 +0200 @@ -92,6 +92,8 @@ val ML_MALFORMED = "ML_malformed" val ML_DEF = "ML_def" + val ML_OPEN = "ML_open" + val ML_STRUCT = "ML_struct" val ML_REF = "ML_ref" val ML_TYPING = "ML_typing"