# HG changeset patch # User wenzelm # Date 1243774281 -7200 # Node ID 1c00e4ff3c99b387b4e2560ec471fe54a8d553be # Parent b82e55f51dccd8551117ad0d84ac23e5007d14c4 more modular setup of runtime compilation; diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/IsaMakefile --- 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 diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/ML-Systems/compiler_polyml-5.0.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; diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/ML-Systems/compiler_polyml-5.2.ML --- /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; + diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/ML-Systems/compiler_polyml-5.3.ML --- /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; + diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/ML-Systems/polyml-5.0.ML --- 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; diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/ML-Systems/polyml-5.1.ML --- 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; diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/ML-Systems/polyml-experimental.ML --- 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 *) diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/ML-Systems/polyml.ML --- 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"; diff -r b82e55f51dcc -r 1c00e4ff3c99 src/Pure/ML-Systems/polyml_old_compiler5.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;