--- a/src/Pure/IsaMakefile Sun May 31 14:46:44 2009 +0200
+++ b/src/Pure/IsaMakefile Sun May 31 14:51:21 2009 +0200
@@ -19,14 +19,15 @@
## Pure
-BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
+BOOTSTRAP_FILES = ML-Systems/compiler_polyml-5.0.ML \
+ ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML \
+ ML-Systems/exn.ML ML-Systems/ml_name_space.ML \
ML-Systems/ml_pretty.ML ML-Systems/mosml.ML \
ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML \
ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML \
ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML \
ML-Systems/polyml.ML ML-Systems/polyml_common.ML \
- ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML \
- ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
+ ML-Systems/polyml_pp.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML \
ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML \
ML-Systems/time_limit.ML ML-Systems/universal.ML
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML Sun May 31 14:51:21 2009 +0200
@@ -0,0 +1,32 @@
+(* Title: Pure/ML-Systems/compiler_polyml-5.0.ML
+
+Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1.
+*)
+
+fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
+ let
+ val in_buffer = ref (explode (tune_source txt));
+ val out_buffer = ref ([]: string list);
+ fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
+
+ val current_line = ref line;
+ fun get () =
+ (case ! in_buffer of
+ [] => ""
+ | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
+ fun put s = out_buffer := s :: ! out_buffer;
+
+ fun exec () =
+ (case ! in_buffer of
+ [] => ()
+ | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
+ in
+ exec () handle exn => (error (output ()); raise exn);
+ if verbose then print (output ()) else ()
+ end;
+
+fun use_file context verbose name =
+ let
+ val instream = TextIO.openIn name;
+ val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+ in use_text context (1, name) verbose txt end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML Sun May 31 14:51:21 2009 +0200
@@ -0,0 +1,51 @@
+(* Title: Pure/ML-Systems/compiler_polyml-5.2.ML
+
+Runtime compilation for Poly/ML 5.2 and 5.2.1.
+*)
+
+local
+
+fun drop_newline s =
+ if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+ else s;
+
+in
+
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+ (start_line, name) verbose txt =
+ let
+ val current_line = ref start_line;
+ val in_buffer = ref (String.explode (tune_source txt));
+ val out_buffer = ref ([]: string list);
+ fun output () = drop_newline (implode (rev (! out_buffer)));
+
+ fun get () =
+ (case ! in_buffer of
+ [] => NONE
+ | c :: cs =>
+ (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+ fun put s = out_buffer := s :: ! out_buffer;
+ fun message (msg, is_err, line) =
+ (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPErrorMessageProc (put o message),
+ PolyML.Compiler.CPNameSpace name_space];
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); raise exn);
+ in if verbose then print (output ()) else () end;
+
+fun use_file context verbose name =
+ let
+ val instream = TextIO.openIn name;
+ val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+ in use_text context (1, name) verbose txt end;
+
+end;
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML Sun May 31 14:51:21 2009 +0200
@@ -0,0 +1,55 @@
+(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
+
+Runtime compilation for Poly/ML 5.3 (SVN experimental).
+*)
+
+local
+
+fun drop_newline s =
+ if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+ else s;
+
+in
+
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+ (start_line, name) verbose txt =
+ let
+ val current_line = ref start_line;
+ val in_buffer = ref (String.explode (tune_source txt));
+ val out_buffer = ref ([]: string list);
+ fun output () = drop_newline (implode (rev (! out_buffer)));
+
+ fun get () =
+ (case ! in_buffer of
+ [] => NONE
+ | c :: cs =>
+ (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
+ fun put s = out_buffer := s :: ! out_buffer;
+ fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
+ (put (if hard then "Error: " else "Warning: ");
+ PolyML.prettyPrint (put, 76) msg1;
+ (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
+ put ("At" ^ str_of_pos line name ^ "\n"));
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPLineNo (fn () => ! current_line),
+ PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPNameSpace name_space,
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false];
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); raise exn);
+ in if verbose then print (output ()) else () end;
+
+fun use_file context verbose name =
+ let
+ val instream = TextIO.openIn name;
+ val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+ in use_text context (1, name) verbose txt end;
+
+end;
+
--- a/src/Pure/ML-Systems/polyml-5.0.ML Sun May 31 14:46:44 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-5.0.ML Sun May 31 14:51:21 2009 +0200
@@ -7,7 +7,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
-use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/compiler_polyml-5.0.ML";
use "ML-Systems/polyml_pp.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-5.1.ML Sun May 31 14:46:44 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-5.1.ML Sun May 31 14:51:21 2009 +0200
@@ -6,7 +6,7 @@
use "ML-Systems/thread_dummy.ML";
use "ML-Systems/ml_name_space.ML";
use "ML-Systems/polyml_common.ML";
-use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/compiler_polyml-5.0.ML";
use "ML-Systems/polyml_pp.ML";
val pointer_eq = PolyML.pointerEq;
--- a/src/Pure/ML-Systems/polyml-experimental.ML Sun May 31 14:46:44 2009 +0200
+++ b/src/Pure/ML-Systems/polyml-experimental.ML Sun May 31 14:51:21 2009 +0200
@@ -1,6 +1,6 @@
-(* Title: Pure/ML-Systems/polyml.ML
+(* Title: Pure/ML-Systems/polyml-experimental.ML
-Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
+Compatibility wrapper for Poly/ML 5.3 (SVN experimental).
*)
open Thread;
@@ -19,58 +19,7 @@
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-(* runtime compilation *)
-
-local
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (start_line, name) verbose txt =
- let
- val current_line = ref start_line;
- val in_buffer = ref (String.explode (tune_source txt));
- val out_buffer = ref ([]: string list);
- fun output () = drop_newline (implode (rev (! out_buffer)));
-
- fun get () =
- (case ! in_buffer of
- [] => NONE
- | c :: cs =>
- (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
- fun put s = out_buffer := s :: ! out_buffer;
- fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
- (put (if hard then "Error: " else "Warning: ");
- PolyML.prettyPrint (put, 76) msg1;
- (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
- put ("At" ^ str_of_pos line name ^ "\n"));
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPErrorMessageProc put_message,
- PolyML.Compiler.CPNameSpace name_space,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false];
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
- in if verbose then print (output ()) else () end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
-
-end;
+use "ML-Systems/compiler_polyml-5.3.ML";
(* toplevel pretty printing *)
--- a/src/Pure/ML-Systems/polyml.ML Sun May 31 14:46:44 2009 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Sun May 31 14:51:21 2009 +0200
@@ -1,6 +1,6 @@
(* Title: Pure/ML-Systems/polyml.ML
-Compatibility wrapper for Poly/ML 5.2 or later.
+Compatibility wrapper for Poly/ML 5.2 and 5.2.1.
*)
open Thread;
@@ -22,54 +22,6 @@
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-(* runtime compilation *)
-
-local
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (start_line, name) verbose txt =
- let
- val current_line = ref start_line;
- val in_buffer = ref (String.explode (tune_source txt));
- val out_buffer = ref ([]: string list);
- fun output () = drop_newline (implode (rev (! out_buffer)));
-
- fun get () =
- (case ! in_buffer of
- [] => NONE
- | c :: cs =>
- (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
- fun put s = out_buffer := s :: ! out_buffer;
- fun message (msg, is_err, line) =
- (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPErrorMessageProc (put o message),
- PolyML.Compiler.CPNameSpace name_space];
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); raise exn);
- in if verbose then print (output ()) else () end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
-
-end;
-
+use "ML-Systems/compiler_polyml-5.2.ML";
use "ML-Systems/polyml_pp.ML";
--- a/src/Pure/ML-Systems/polyml_old_compiler5.ML Sun May 31 14:46:44 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,32 +0,0 @@
-(* Title: Pure/ML-Systems/polyml_old_compiler5.ML
-
-Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
-*)
-
-fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
- let
- val in_buffer = ref (explode (tune_source txt));
- val out_buffer = ref ([]: string list);
- fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
-
- val current_line = ref line;
- fun get () =
- (case ! in_buffer of
- [] => ""
- | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
- fun put s = out_buffer := s :: ! out_buffer;
-
- fun exec () =
- (case ! in_buffer of
- [] => ()
- | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
- in
- exec () handle exn => (error (output ()); raise exn);
- if verbose then print (output ()) else ()
- end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;