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