src/Pure/ML-Systems/compiler_polyml-5.0.ML
changeset 32738 15bb09ca0378
parent 31480 05937d6aafb5
     1.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -5,11 +5,11 @@
     1.4  
     1.5  fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
     1.6    let
     1.7 -    val in_buffer = ref (explode (tune_source txt));
     1.8 -    val out_buffer = ref ([]: string list);
     1.9 +    val in_buffer = Unsynchronized.ref (explode (tune_source txt));
    1.10 +    val out_buffer = Unsynchronized.ref ([]: string list);
    1.11      fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.12  
    1.13 -    val current_line = ref line;
    1.14 +    val current_line = Unsynchronized.ref line;
    1.15      fun get () =
    1.16        (case ! in_buffer of
    1.17          [] => ""