| changeset 75615 | 4494cd69f97f |
| parent 75577 | c51e1cef1eae |
| child 76183 | 8089593a364a |
--- a/src/Pure/PIDE/byte_message.ML Fri Jun 24 23:11:59 2022 +0200 +++ b/src/Pure/PIDE/byte_message.ML Fri Jun 24 23:31:28 2022 +0200 @@ -29,7 +29,8 @@ val write = List.app o Bytes.write_stream; -fun write_yxml stream tree = YXML.traverse (fn s => fn () => File.output stream s) tree (); +fun write_yxml stream tree = + YXML.traverse (fn s => fn () => File_Stream.output stream s) tree (); fun flush stream = ignore (try BinIO.flushOut stream);