--- a/src/Pure/General/pretty.ML Sat Sep 04 18:21:58 2021 +0200
+++ b/src/Pure/General/pretty.ML Sat Sep 04 20:01:43 2021 +0200
@@ -321,7 +321,7 @@
(* special output *)
(*symbolic markup -- no formatting*)
-fun symbolic prt =
+val symbolic =
let
fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
| out (Block ((bg, en), consistent, indent, prts, _)) =
@@ -332,15 +332,15 @@
Buffer.markup (Markup.break wd ind) (Buffer.add (output_spaces wd))
| out (Break (true, _, _)) = Buffer.add (Output.output "\n")
| out (Str (s, _)) = Buffer.add s;
- in out prt Buffer.empty end;
+ in Buffer.build o out end;
(*unformatted output*)
-fun unformatted prt =
+val unformatted =
let
fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
| out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
| out (Str (s, _)) = Buffer.add s;
- in out prt Buffer.empty end;
+ in Buffer.build o out end;
(* output interfaces *)