src/Pure/ML-Systems/polyml_old_compiler4.ML
changeset 26385 ae7564661e76
parent 26382 16628f5c7e28
child 26504 6e87c0a60104
equal deleted inserted replaced
26384:0aed2ba71388 26385:ae7564661e76
     1 (*  Title:      Pure/ML-Systems/polyml_old_compiler4.ML
     1 (*  Title:      Pure/ML-Systems/polyml_old_compiler4.ML
     2     ID:         $Id$
     2     ID:         $Id$
     3 
     3 
     4 Runtime compilation -- for old version of PolyML.compiler (version 4.x).
     4 Runtime compilation -- for old PolyML.compiler (version 4.x).
     5 *)
     5 *)
     6 
     6 
     7 fun use_text (tune: string -> string) name (print, err) verbose txt =
     7 fun use_text (tune: string -> string) (line: int, name) (print, err) verbose txt =
     8   let
     8   let
     9     val in_buffer = ref (explode (tune txt));
     9     val in_buffer = ref (explode (tune txt));
    10     val out_buffer = ref ([]: string list);
    10     val out_buffer = ref ([]: string list);
    11     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    11     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    12 
    12 
    28 
    28 
    29 fun use_file tune output verbose name =
    29 fun use_file tune output verbose name =
    30   let
    30   let
    31     val instream = TextIO.openIn name;
    31     val instream = TextIO.openIn name;
    32     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    32     val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    33   in use_text tune name output verbose txt end;
    33   in use_text tune (1, name) output verbose txt end;
    34 
    34