Runtime compilation -- for old version of PolyML.compilerEx (version 5.0, 5.1).
authorwenzelm
Mon Mar 24 18:35:49 2008 +0100 (2008-03-24 ago)
changeset 2638308da16c3f124
parent 26382 16628f5c7e28
child 26384 0aed2ba71388
Runtime compilation -- for old version of PolyML.compilerEx (version 5.0, 5.1).
src/Pure/ML-Systems/polyml_old_compiler5.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML-Systems/polyml_old_compiler5.ML	Mon Mar 24 18:35:49 2008 +0100
     1.3 @@ -0,0 +1,35 @@
     1.4 +(*  Title:      Pure/ML-Systems/polyml_old_compiler5.ML
     1.5 +    ID:         $Id$
     1.6 +
     1.7 +Runtime compilation -- for old version of PolyML.compilerEx (version 5.0, 5.1).
     1.8 +*)
     1.9 +
    1.10 +fun use_text (tune: string -> string) name (print, err) verbose txt =
    1.11 +  let
    1.12 +    val in_buffer = ref (explode (tune txt));
    1.13 +    val out_buffer = ref ([]: string list);
    1.14 +    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    1.15 +
    1.16 +    val line_no = ref 1;
    1.17 +    fun line () = ! line_no;
    1.18 +    fun get () =
    1.19 +      (case ! in_buffer of
    1.20 +        [] => ""
    1.21 +      | c :: cs => (in_buffer := cs; if c = "\n" then line_no := ! line_no + 1 else (); c));
    1.22 +    fun put s = out_buffer := s :: ! out_buffer;
    1.23 +
    1.24 +    fun exec () =
    1.25 +      (case ! in_buffer of
    1.26 +        [] => ()
    1.27 +      | _ => (PolyML.compilerEx (get, put, line, name) (); exec ()));
    1.28 +  in
    1.29 +    exec () handle exn => (err (output ()); raise exn);
    1.30 +    if verbose then print (output ()) else ()
    1.31 +  end;
    1.32 +
    1.33 +fun use_file tune output verbose name =
    1.34 +  let
    1.35 +    val instream = TextIO.openIn name;
    1.36 +    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
    1.37 +  in use_text tune name output verbose txt end;
    1.38 +