# HG changeset patch
# User wenzelm
# Date 1206380148 -3600
# Node ID 16628f5c7e28d4e5d9cff4c37c953c97ad2cd10d
# Parent  509a1ca9d35cb5c898c061f039b0da806c950d72
Runtime compilation -- for old version of PolyML.compiler (version 4.x).

diff -r 509a1ca9d35c -r 16628f5c7e28 src/Pure/ML-Systems/polyml_old_compiler4.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml_old_compiler4.ML	Mon Mar 24 18:35:48 2008 +0100
@@ -0,0 +1,34 @@
+(*  Title:      Pure/ML-Systems/polyml_old_compiler4.ML
+    ID:         $Id$
+
+Runtime compilation -- for old version of PolyML.compiler (version 4.x).
+*)
+
+fun use_text (tune: string -> string) name (print, err) verbose txt =
+  let
+    val in_buffer = ref (explode (tune txt));
+    val out_buffer = ref ([]: string list);
+    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
+
+    fun get () =
+      (case ! in_buffer of
+        [] => ""
+      | c :: cs => (in_buffer := cs; c));
+    fun put s = out_buffer := s :: ! out_buffer;
+
+    fun exec () =
+      (case ! in_buffer of
+        [] => ()
+      | _ => (PolyML.compiler (get, put) (); exec ()));
+  in
+    exec () handle exn =>
+      (err ((if name = "" then "" else "Error in " ^ name ^ "\n") ^ output ()); raise exn);
+    if verbose then print (output ()) else ()
+  end;
+
+fun use_file tune output verbose name =
+  let
+    val instream = TextIO.openIn name;
+    val txt = TextIO.inputAll instream before TextIO.closeIn instream;
+  in use_text tune name output verbose txt end;
+