1.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Thu May 24 14:46:14 2012 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,53 +0,0 @@
     1.4 -(*  Title:      Pure/ML-Systems/compiler_polyml-5.2.ML
     1.5 -
     1.6 -Runtime compilation for Poly/ML 5.2.x.
     1.7 -*)
     1.8 -
     1.9 -local
    1.10 -
    1.11 -fun drop_newline s =
    1.12 -  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    1.13 -  else s;
    1.14 -
    1.15 -in
    1.16 -
    1.17 -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    1.18 -    (start_line, name) verbose txt =
    1.19 -  let
    1.20 -    val current_line = Unsynchronized.ref start_line;
    1.21 -    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
    1.22 -    val out_buffer = Unsynchronized.ref ([]: string list);
    1.23 -    fun output () = drop_newline (implode (rev (! out_buffer)));
    1.24 -
    1.25 -    fun get () =
    1.26 -      (case ! in_buffer of
    1.27 -        [] => NONE
    1.28 -      | c :: cs =>
    1.29 -          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    1.30 -    fun put s = out_buffer := s :: ! out_buffer;
    1.31 -    fun message (msg, is_err, line) =
    1.32 -      (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
    1.33 -
    1.34 -    val parameters =
    1.35 -     [PolyML.Compiler.CPOutStream put,
    1.36 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    1.37 -      PolyML.Compiler.CPErrorMessageProc (put o message),
    1.38 -      PolyML.Compiler.CPNameSpace name_space];
    1.39 -    val _ =
    1.40 -      (while not (List.null (! in_buffer)) do
    1.41 -        PolyML.compiler (get, parameters) ())
    1.42 -      handle exn =>
    1.43 -        if Exn.is_interrupt exn then reraise exn
    1.44 -        else
    1.45 -         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    1.46 -          error (output ()); reraise exn);
    1.47 -  in if verbose then print (output ()) else () end;
    1.48 -
    1.49 -fun use_file context verbose name =
    1.50 -  let
    1.51 -    val instream = TextIO.openIn name;
    1.52 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    1.53 -  in use_text context (1, name) verbose txt end;
    1.54 -
    1.55 -end;
    1.56 -