| changeset 74231 | b3c65c984210 |
| parent 73557 | 225486d9c960 |
| child 75615 | 4494cd69f97f |
--- a/src/Pure/PIDE/yxml.ML Sat Sep 04 18:21:58 2021 +0200 +++ b/src/Pure/PIDE/yxml.ML Sat Sep 04 20:01:43 2021 +0200 @@ -85,7 +85,7 @@ (* output *) -fun string_of_body body = Buffer.empty |> fold (traverse Buffer.add) body |> Buffer.content; +val string_of_body = Buffer.build_content o fold (traverse Buffer.add); val string_of = string_of_body o single; fun write_body path body =