# HG changeset patch
# User wenzelm
# Date 1726077550 -7200
# Node ID aff85c86737b09ac2e276d43560c47d9305fe27f
# Parent  300c75231e2bbffafefa07a834ecb8ae69867bf5
clarified properties;

diff -r 300c75231e2b -r aff85c86737b src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Wed Sep 11 19:53:35 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Wed Sep 11 19:59:10 2024 +0200
@@ -38,8 +38,8 @@
     SOME (ContextProperty (_, b)) => b
   | _ => "");
 
-val markup_bg = "begin";
-val markup_en = "end";
+val markup_bg = "markup_bg";
+val markup_en = "markup_en";
 
 fun context_markup context =
   let