# HG changeset patch
# User wenzelm
# Date 1244311090 -7200
# Node ID d7929d74acb42c4bd3cb8000ed22432a48285f5b
# Parent  e3987b32e401075280c618b93c6b62da30cf1f9d
added markup ML_open, ML_struct;

diff -r e3987b32e401 -r d7929d74acb4 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sat Jun 06 19:58:10 2009 +0200
+++ b/src/Pure/General/markup.ML	Sat Jun 06 19:58:10 2009 +0200
@@ -71,6 +71,8 @@
   val ML_commentN: string val ML_comment: T
   val ML_malformedN: string val ML_malformed: T
   val ML_defN: string val ML_def: T
+  val ML_openN: string val ML_open: T
+  val ML_structN: string val ML_struct: T
   val ML_refN: string val ML_ref: T
   val ML_typingN: string val ML_typing: T
   val ML_sourceN: string val ML_source: T
@@ -237,6 +239,8 @@
 val (ML_malformedN, ML_malformed) = markup_elem "ML_malformed";
 
 val (ML_defN, ML_def) = markup_elem "ML_def";
+val (ML_openN, ML_open) = markup_elem "ML_open";
+val (ML_structN, ML_struct) = markup_elem "ML_struct";
 val (ML_refN, ML_ref) = markup_elem "ML_ref";
 val (ML_typingN, ML_typing) = markup_elem "ML_typing";
 
diff -r e3987b32e401 -r d7929d74acb4 src/Pure/General/markup.scala
--- 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"