# HG changeset patch
# User wenzelm
# Date 1726077215 -7200
# Node ID 300c75231e2bbffafefa07a834ecb8ae69867bf5
# Parent  301612847ea3f4cc3724def679240143ca407340
clarified signature and modules;

diff -r 301612847ea3 -r 300c75231e2b src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Sep 11 19:35:21 2024 +0200
+++ b/src/Pure/General/pretty.ML	Wed Sep 11 19:53:35 2024 +0200
@@ -143,11 +143,9 @@
 
 (* primitives *)
 
-fun make_block {markup = (bg, en), consistent, indent} body =
+fun make_block {markup, consistent, indent} body =
   let
-    val context =
-      (if bg = "" then [] else [ML_Pretty.ContextProperty ("begin", bg)]) @
-      (if en = "" then [] else [ML_Pretty.ContextProperty ("end", en)]);
+    val context = ML_Pretty.markup_context markup;
     val ind = short_nat indent;
   in from_ML (ML_Pretty.PrettyBlock (ind, consistent, context, map to_ML body)) end;
 
@@ -278,12 +276,6 @@
 
 local
 
-fun context_property context name =
-  let
-    fun get (ML_Pretty.ContextProperty (a, b)) = if name = a then SOME b else NONE
-      | get _ = NONE;
-  in the_default "" (get_first get context) end;
-
 fun block_length indent =
   let
     fun block_len len prts =
@@ -306,13 +298,11 @@
   let
     fun out (ML_Pretty.PrettyBlock (ind, consistent, context, body)) =
           let
-            val bg = context_property context "begin";
-            val en = context_property context "end";
-            val m = #markup ops (bg, en);
+            val markup = #markup ops (ML_Pretty.context_markup context);
             val indent = long_nat ind;
             val body' = map out body;
             val len = if make_length then block_length indent body' else ~1;
-          in Block (m, consistent, indent, body', len) end
+          in Block (markup, consistent, indent, body', len) end
       | out (ML_Pretty.PrettyBreak (wd, ind)) = Break (false, long_nat wd, long_nat ind)
       | out ML_Pretty.PrettyLineBreak = fbreak
       | out (ML_Pretty.PrettyString s) = Str (#output ops s ||> force_nat)
diff -r 301612847ea3 -r 300c75231e2b src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Wed Sep 11 19:35:21 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Wed Sep 11 19:53:35 2024 +0200
@@ -7,6 +7,8 @@
 signature ML_PRETTY =
 sig
   datatype context = datatype PolyML.context
+  val context_markup: PolyML.context list -> string * string
+  val markup_context: string * string -> PolyML.context list
   datatype pretty = datatype PolyML.pretty
   val block: pretty list -> pretty
   val str: string -> pretty
@@ -27,9 +29,31 @@
 structure ML_Pretty: ML_PRETTY =
 struct
 
+(* context and markup *)
+
+datatype context = datatype PolyML.context;
+
+fun context_property context name =
+  (case List.find (fn ContextProperty (a, _) => name = a | _ => false) context of
+    SOME (ContextProperty (_, b)) => b
+  | _ => "");
+
+val markup_bg = "begin";
+val markup_en = "end";
+
+fun context_markup context =
+  let
+    val bg = context_property context markup_bg;
+    val en = context_property context markup_en;
+  in (bg, en) end;
+
+fun markup_context (bg, en) =
+  (if bg = "" then [] else [ContextProperty (markup_bg, bg)]) @
+  (if en = "" then [] else [ContextProperty (markup_en, en)]);
+
+
 (* datatype pretty with derived operations *)
 
-datatype context = datatype PolyML.context;
 datatype pretty = datatype PolyML.pretty;
 
 fun block prts = PrettyBlock (2, false, [], prts);