src/Pure/ML/ml_compiler_polyml-5.3.ML

--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 29 11:48:32 2009 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 29 11:49:22 2009 +0200
@@ -91,8 +91,8 @@
       if null toks then Position.none
       else ML_Lex.end_pos_of (List.last toks);
 
-    val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]);
-    val line = ref (the_default 1 (Position.line_of pos));
+    val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
+    val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
 
     fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
     fun get () =
@@ -106,9 +106,9 @@
 
     (* output *)
 
-    val output_buffer = ref Buffer.empty;
+    val output_buffer = Unsynchronized.ref Buffer.empty;
     fun output () = Buffer.content (! output_buffer);
-    fun put s = change output_buffer (Buffer.add s);
+    fun put s = Unsynchronized.change output_buffer (Buffer.add s);
 
     fun put_message {message, hard, location, context = _} =
      (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");