src/Pure/ML-Systems/polyml-5.1.ML
changeset 23943 1b5f77bc146a
child 23947 5e396bcf749e
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Mon Jul 23 20:47:55 2007 +0200
     1.3 @@ -0,0 +1,41 @@
     1.4 +(*  Title:      Pure/ML-Systems/polyml-5.0.ML
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +Compatibility wrapper for Poly/ML 5.1.
     1.8 +*)
     1.9 +
    1.10 +use "ML-Systems/polyml.ML";
    1.11 +
    1.12 +val pointer_eq = PolyML.pointerEq;
    1.13 +
    1.14 +
    1.15 +(* improved versions of use_text/file *)
    1.16 +
    1.17 +fun use_text name (print, err) verbose txt =
    1.18 +  let
    1.19 +    val in_buffer = ref (explode txt);
    1.20 +    val out_buffer = ref ([]: string list);
    1.21 +    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.22 +
    1.23 +    val line_no = ref 1;
    1.24 +    fun line () = ! line_no;
    1.25 +    fun get () =
    1.26 +      (case ! in_buffer of
    1.27 +        [] => ""
    1.28 +      | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
    1.29 +    fun put s = out_buffer := s :: ! out_buffer;
    1.30 +
    1.31 +    fun exec () =
    1.32 +      (case ! in_buffer of
    1.33 +        [] => ()
    1.34 +      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
    1.35 +  in
    1.36 +    exec () handle exn => (err (output ()); raise exn);
    1.37 +    if verbose then print (output ()) else ()
    1.38 +  end;
    1.39 +
    1.40 +fun use_file output verbose name =
    1.41 +  let
    1.42 +    val instream = TextIO.openIn name;
    1.43 +    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.44 +  in use_text name output verbose txt end;