clarified data representation: less redundancy;
authorwenzelm
Sun, 29 Dec 2024 13:52:27 +0100
changeset 81686 8473f4f57368
parent 81685 13bd6223691d
child 81687 d92a3649bfd1
clarified data representation: less redundancy;
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 = [];