changeset 80857 | aff85c86737b |
parent 80856 | 300c75231e2b |
child 81121 | 7cacedbddba7 |
--- 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