src/Pure/ML-Systems/compiler_polyml-5.0.ML
changeset 31312 1c00e4ff3c99
child 31329 c8821a6297f9
equal deleted inserted replaced
31311:b82e55f51dcc 31312:1c00e4ff3c99
       
     1 (*  Title:      Pure/ML-Systems/compiler_polyml-5.0.ML
       
     2 
       
     3 Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1.
       
     4 *)
       
     5 
       
     6 fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
       
     7   let
       
     8     val in_buffer = ref (explode (tune_source txt));
       
     9     val out_buffer = ref ([]: string list);
       
    10     fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
       
    11 
       
    12     val current_line = ref line;
       
    13     fun get () =
       
    14       (case ! in_buffer of
       
    15         [] => ""
       
    16       | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
       
    17     fun put s = out_buffer := s :: ! out_buffer;
       
    18 
       
    19     fun exec () =
       
    20       (case ! in_buffer of
       
    21         [] => ()
       
    22       | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
       
    23   in
       
    24     exec () handle exn => (error (output ()); raise exn);
       
    25     if verbose then print (output ()) else ()
       
    26   end;
       
    27 
       
    28 fun use_file context verbose name =
       
    29   let
       
    30     val instream = TextIO.openIn name;
       
    31     val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
       
    32   in use_text context (1, name) verbose txt end;