# 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;