src/Pure/ML-Systems/compiler_polyml-5.2.ML
changeset 32738 15bb09ca0378
parent 31480 05937d6aafb5
child 39242 28d3809ff91f
     1.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -14,9 +14,9 @@
     1.4  fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
     1.5      (start_line, name) verbose txt =
     1.6    let
     1.7 -    val current_line = ref start_line;
     1.8 -    val in_buffer = ref (String.explode (tune_source txt));
     1.9 -    val out_buffer = ref ([]: string list);
    1.10 +    val current_line = Unsynchronized.ref start_line;
    1.11 +    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
    1.12 +    val out_buffer = Unsynchronized.ref ([]: string list);
    1.13      fun output () = drop_newline (implode (rev (! out_buffer)));
    1.14  
    1.15      fun get () =