# HG changeset patch
# User wenzelm
# Date 1725873708 -7200
# Node ID 4f54a509bc8967c888731286823d1d22057c201c
# Parent  eb383d50564b1a3f364c23603edeeaa21267da85
clarified modules (see also ea7c2ee8a47a);

diff -r eb383d50564b -r 4f54a509bc89 src/Pure/General/buffer.ML
--- a/src/Pure/General/buffer.ML	Mon Sep 09 11:12:13 2024 +0200
+++ b/src/Pure/General/buffer.ML	Mon Sep 09 11:21:48 2024 +0200
@@ -15,7 +15,6 @@
   val content: T -> string
   val build: (T -> T) -> T
   val build_content: (T -> T) -> string
-  val markup: Markup.T -> (T -> T) -> T -> T
 end;
 
 structure Buffer: BUFFER =
@@ -41,8 +40,4 @@
 
 end;
 
-fun markup m body =
-  let val (bg, en) = Markup.output m
-  in add bg #> body #> add en end;
-
 end;
diff -r eb383d50564b -r 4f54a509bc89 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Sep 09 11:12:13 2024 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 09 11:21:48 2024 +0200
@@ -368,15 +368,19 @@
 
 (* special output *)
 
+fun buffer_markup m body =
+  let val (bg, en) = Markup.output m
+  in Buffer.add bg #> body #> Buffer.add en end;
+
 (*symbolic markup -- no formatting*)
 val symbolic =
   let
     fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
       | out (Block ((bg, en), consistent, indent, prts, _)) =
           Buffer.add bg #>
-          Buffer.markup (Markup.block consistent indent) (fold out prts) #>
+          buffer_markup (Markup.block consistent indent) (fold out prts) #>
           Buffer.add en
-      | out (Break (false, wd, ind)) = Buffer.markup (Markup.break wd ind) (buffer_output_spaces wd)
+      | out (Break (false, wd, ind)) = buffer_markup (Markup.break wd ind) (buffer_output_spaces wd)
       | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
       | out (Str (s, _)) = Buffer.add s;
   in Buffer.build o out o output_tree false end;