# HG changeset patch # User wenzelm # Date 1207250616 -7200 # Node ID 6e1aef001b3b238fcb1a8dbdfbd91b3552bff14d # Parent af4c77a21c06837f8e491c1f04477632ced4563e output: canonical argument order (as opposed to write); diff -r af4c77a21c06 -r 6e1aef001b3b src/Pure/General/buffer.ML --- a/src/Pure/General/buffer.ML Thu Apr 03 18:42:42 2008 +0200 +++ b/src/Pure/General/buffer.ML Thu Apr 03 21:23:36 2008 +0200 @@ -13,7 +13,7 @@ val add_substring: substring -> T -> T val markup: Markup.T -> (T -> T) -> T -> T val content: T -> string - val output: TextIO.outstream -> T -> unit + val output: T -> TextIO.outstream -> unit val write: Path.T -> T -> unit end; @@ -55,13 +55,13 @@ | rev_buffer (String (s, buf)) acc = rev_buffer buf (String (s, acc)) | rev_buffer (Substring (s, buf)) acc = rev_buffer buf (Substring (s, acc)); -fun output stream buffer = +fun output buffer stream = let fun rev_output EmptyBuffer = () | rev_output (String (s, buf)) = (TextIO.output (stream, s); rev_output buf) | rev_output (Substring (s, buf)) = (TextIO.outputSubstr (stream, s); rev_output buf); in rev_output (rev_buffer buffer empty) end; -fun write path buf = File.open_output (fn stream => output stream buf) path; +fun write path buf = File.open_output (output buf) path; end;