diff -r 080beab27264 -r 7cacedbddba7 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Sun Oct 06 13:02:33 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Sun Oct 06 18:34:35 2024 +0200
@@ -9,6 +9,8 @@
   datatype context = datatype PolyML.context
   val context_markup: PolyML.context list -> string * string
   val markup_context: string * string -> PolyML.context list
+  val context_open_block: PolyML.context list -> bool
+  val open_block_context: bool -> PolyML.context list
   datatype pretty = datatype PolyML.pretty
   val block: pretty list -> pretty
   val str: string -> pretty
@@ -29,7 +31,9 @@
 structure ML_Pretty: ML_PRETTY =
 struct
 
-(* context and markup *)
+(** context **)
+
+(* properties *)
 
 datatype context = datatype PolyML.context;
 
@@ -38,6 +42,9 @@
     SOME (ContextProperty (_, b)) => b
   | _ => "");
 
+
+(* markup *)
+
 val markup_bg = "markup_bg";
 val markup_en = "markup_en";
 
@@ -52,6 +59,19 @@
   (if en = "" then [] else [ContextProperty (markup_en, en)]);
 
 
+(* open_block flag *)
+
+val open_block = ContextProperty ("open_block", "true");
+
+val context_open_block = List.exists (fn c => c = open_block);
+
+fun open_block_context false = []
+  | open_block_context true = [open_block];
+
+
+
+(** pretty printing **)
+
 (* datatype pretty with derived operations *)
 
 datatype pretty = datatype PolyML.pretty;