--- a/src/Pure/PIDE/markup.scala Sun Mar 02 18:41:41 2014 +0100
+++ b/src/Pure/PIDE/markup.scala Sun Mar 02 19:00:45 2014 +0100
@@ -204,7 +204,7 @@
val ML_DEF = "ML_def"
val ML_OPEN = "ML_open"
- val ML_STRUCT = "ML_struct"
+ val ML_STRUCTURE = "ML_structure"
val ML_TYPING = "ML_typing"