src/Pure/ML/ml_compiler_polyml-5.3.ML
changeset 32738 15bb09ca0378
parent 32493 457ea5ddbb9b
child 33538 edf497b5b5d2
     1.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -91,8 +91,8 @@
     1.4        if null toks then Position.none
     1.5        else ML_Lex.end_pos_of (List.last toks);
     1.6  
     1.7 -    val input_buffer = ref (input @ [(offset_of end_pos, #"\n")]);
     1.8 -    val line = ref (the_default 1 (Position.line_of pos));
     1.9 +    val input_buffer = Unsynchronized.ref (input @ [(offset_of end_pos, #"\n")]);
    1.10 +    val line = Unsynchronized.ref (the_default 1 (Position.line_of pos));
    1.11  
    1.12      fun get_offset () = (case ! input_buffer of [] => 0 | (i, _) :: _ => i);
    1.13      fun get () =
    1.14 @@ -106,9 +106,9 @@
    1.15  
    1.16      (* output *)
    1.17  
    1.18 -    val output_buffer = ref Buffer.empty;
    1.19 +    val output_buffer = Unsynchronized.ref Buffer.empty;
    1.20      fun output () = Buffer.content (! output_buffer);
    1.21 -    fun put s = change output_buffer (Buffer.add s);
    1.22 +    fun put s = Unsynchronized.change output_buffer (Buffer.add s);
    1.23  
    1.24      fun put_message {message, hard, location, context = _} =
    1.25       (put ((if hard then "Error" else "Warning") ^ Position.str_of (position_of location) ^ ":\n");