# HG changeset patch
# User wenzelm
# Date 1735476747 -3600
# Node ID 8473f4f57368468eddbc2e101d06f195e78d64f0
# Parent  13bd6223691da2da6eaf6c1de64d3524ece9e493
clarified data representation: less redundancy;

diff -r 13bd6223691d -r 8473f4f57368 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Sun Dec 29 13:16:26 2024 +0100
+++ b/src/Pure/ML/ml_pretty.ML	Sun Dec 29 13:52:27 2024 +0100
@@ -61,12 +61,13 @@
 
 (* open_block flag *)
 
-val open_block = ContextProperty ("open_block", "true");
+val open_block = ContextProperty ("open_block", "");
 
-val open_block_detect = List.exists (fn c => c = open_block);
+val open_block_detect =
+  List.exists (fn ContextProperty ("open_block", _) => true | _ => false);
 
-fun open_block_context false = []
-  | open_block_context true = [open_block];
+fun open_block_context true = [open_block]
+  | open_block_context false = [];