more modular setup of runtime compilation;
authorwenzelm
Sun May 31 14:51:21 2009 +0200 (2009-05-31)
changeset 313121c00e4ff3c99
parent 31311 b82e55f51dcc
child 31313 97800f7e80b4
more modular setup of runtime compilation;
src/Pure/IsaMakefile
src/Pure/ML-Systems/compiler_polyml-5.0.ML
src/Pure/ML-Systems/compiler_polyml-5.2.ML
src/Pure/ML-Systems/compiler_polyml-5.3.ML
src/Pure/ML-Systems/polyml-5.0.ML
src/Pure/ML-Systems/polyml-5.1.ML
src/Pure/ML-Systems/polyml-experimental.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/polyml_old_compiler5.ML
     1.1 --- a/src/Pure/IsaMakefile	Sun May 31 14:46:44 2009 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Sun May 31 14:51:21 2009 +0200
     1.3 @@ -19,14 +19,15 @@
     1.4  
     1.5  ## Pure
     1.6  
     1.7 -BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML		\
     1.8 +BOOTSTRAP_FILES = ML-Systems/compiler_polyml-5.0.ML			\
     1.9 +  ML-Systems/compiler_polyml-5.2.ML ML-Systems/compiler_polyml-5.3.ML	\
    1.10 +  ML-Systems/exn.ML ML-Systems/ml_name_space.ML				\
    1.11    ML-Systems/ml_pretty.ML ML-Systems/mosml.ML				\
    1.12    ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML	\
    1.13    ML-Systems/overloading_smlnj.ML ML-Systems/polyml-5.0.ML		\
    1.14    ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML		\
    1.15    ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
    1.16 -  ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML		\
    1.17 -  ML-Systems/proper_int.ML ML-Systems/smlnj.ML				\
    1.18 +  ML-Systems/polyml_pp.ML ML-Systems/proper_int.ML ML-Systems/smlnj.ML	\
    1.19    ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
    1.20    ML-Systems/time_limit.ML ML-Systems/universal.ML
    1.21  
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Sun May 31 14:51:21 2009 +0200
     2.3 @@ -0,0 +1,32 @@
     2.4 +(*  Title:      Pure/ML-Systems/compiler_polyml-5.0.ML
     2.5 +
     2.6 +Runtime compilation -- for PolyML.compilerEx in version 5.0 and 5.1.
     2.7 +*)
     2.8 +
     2.9 +fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
    2.10 +  let
    2.11 +    val in_buffer = ref (explode (tune_source txt));
    2.12 +    val out_buffer = ref ([]: string list);
    2.13 +    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    2.14 +
    2.15 +    val current_line = ref line;
    2.16 +    fun get () =
    2.17 +      (case ! in_buffer of
    2.18 +        [] => ""
    2.19 +      | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
    2.20 +    fun put s = out_buffer := s :: ! out_buffer;
    2.21 +
    2.22 +    fun exec () =
    2.23 +      (case ! in_buffer of
    2.24 +        [] => ()
    2.25 +      | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
    2.26 +  in
    2.27 +    exec () handle exn => (error (output ()); raise exn);
    2.28 +    if verbose then print (output ()) else ()
    2.29 +  end;
    2.30 +
    2.31 +fun use_file context verbose name =
    2.32 +  let
    2.33 +    val instream = TextIO.openIn name;
    2.34 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    2.35 +  in use_text context (1, name) verbose txt end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Sun May 31 14:51:21 2009 +0200
     3.3 @@ -0,0 +1,51 @@
     3.4 +(*  Title:      Pure/ML-Systems/compiler_polyml-5.2.ML
     3.5 +
     3.6 +Runtime compilation for Poly/ML 5.2 and 5.2.1.
     3.7 +*)
     3.8 +
     3.9 +local
    3.10 +
    3.11 +fun drop_newline s =
    3.12 +  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    3.13 +  else s;
    3.14 +
    3.15 +in
    3.16 +
    3.17 +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    3.18 +    (start_line, name) verbose txt =
    3.19 +  let
    3.20 +    val current_line = ref start_line;
    3.21 +    val in_buffer = ref (String.explode (tune_source txt));
    3.22 +    val out_buffer = ref ([]: string list);
    3.23 +    fun output () = drop_newline (implode (rev (! out_buffer)));
    3.24 +
    3.25 +    fun get () =
    3.26 +      (case ! in_buffer of
    3.27 +        [] => NONE
    3.28 +      | c :: cs =>
    3.29 +          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    3.30 +    fun put s = out_buffer := s :: ! out_buffer;
    3.31 +    fun message (msg, is_err, line) =
    3.32 +      (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
    3.33 +
    3.34 +    val parameters =
    3.35 +     [PolyML.Compiler.CPOutStream put,
    3.36 +      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    3.37 +      PolyML.Compiler.CPErrorMessageProc (put o message),
    3.38 +      PolyML.Compiler.CPNameSpace name_space];
    3.39 +    val _ =
    3.40 +      (while not (List.null (! in_buffer)) do
    3.41 +        PolyML.compiler (get, parameters) ())
    3.42 +      handle exn =>
    3.43 +       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    3.44 +        error (output ()); raise exn);
    3.45 +  in if verbose then print (output ()) else () end;
    3.46 +
    3.47 +fun use_file context verbose name =
    3.48 +  let
    3.49 +    val instream = TextIO.openIn name;
    3.50 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    3.51 +  in use_text context (1, name) verbose txt end;
    3.52 +
    3.53 +end;
    3.54 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Sun May 31 14:51:21 2009 +0200
     4.3 @@ -0,0 +1,55 @@
     4.4 +(*  Title:      Pure/ML-Systems/compiler_polyml-5.3.ML
     4.5 +
     4.6 +Runtime compilation for Poly/ML 5.3 (SVN experimental).
     4.7 +*)
     4.8 +
     4.9 +local
    4.10 +
    4.11 +fun drop_newline s =
    4.12 +  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    4.13 +  else s;
    4.14 +
    4.15 +in
    4.16 +
    4.17 +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    4.18 +    (start_line, name) verbose txt =
    4.19 +  let
    4.20 +    val current_line = ref start_line;
    4.21 +    val in_buffer = ref (String.explode (tune_source txt));
    4.22 +    val out_buffer = ref ([]: string list);
    4.23 +    fun output () = drop_newline (implode (rev (! out_buffer)));
    4.24 +
    4.25 +    fun get () =
    4.26 +      (case ! in_buffer of
    4.27 +        [] => NONE
    4.28 +      | c :: cs =>
    4.29 +          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    4.30 +    fun put s = out_buffer := s :: ! out_buffer;
    4.31 +    fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
    4.32 +     (put (if hard then "Error: " else "Warning: ");
    4.33 +      PolyML.prettyPrint (put, 76) msg1;
    4.34 +      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    4.35 +      put ("At" ^ str_of_pos line name ^ "\n"));
    4.36 +
    4.37 +    val parameters =
    4.38 +     [PolyML.Compiler.CPOutStream put,
    4.39 +      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    4.40 +      PolyML.Compiler.CPErrorMessageProc put_message,
    4.41 +      PolyML.Compiler.CPNameSpace name_space,
    4.42 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
    4.43 +    val _ =
    4.44 +      (while not (List.null (! in_buffer)) do
    4.45 +        PolyML.compiler (get, parameters) ())
    4.46 +      handle exn =>
    4.47 +       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    4.48 +        error (output ()); raise exn);
    4.49 +  in if verbose then print (output ()) else () end;
    4.50 +
    4.51 +fun use_file context verbose name =
    4.52 +  let
    4.53 +    val instream = TextIO.openIn name;
    4.54 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    4.55 +  in use_text context (1, name) verbose txt end;
    4.56 +
    4.57 +end;
    4.58 +
     5.1 --- a/src/Pure/ML-Systems/polyml-5.0.ML	Sun May 31 14:46:44 2009 +0200
     5.2 +++ b/src/Pure/ML-Systems/polyml-5.0.ML	Sun May 31 14:51:21 2009 +0200
     5.3 @@ -7,7 +7,7 @@
     5.4  use "ML-Systems/thread_dummy.ML";
     5.5  use "ML-Systems/ml_name_space.ML";
     5.6  use "ML-Systems/polyml_common.ML";
     5.7 -use "ML-Systems/polyml_old_compiler5.ML";
     5.8 +use "ML-Systems/compiler_polyml-5.0.ML";
     5.9  use "ML-Systems/polyml_pp.ML";
    5.10  
    5.11  val pointer_eq = PolyML.pointerEq;
     6.1 --- a/src/Pure/ML-Systems/polyml-5.1.ML	Sun May 31 14:46:44 2009 +0200
     6.2 +++ b/src/Pure/ML-Systems/polyml-5.1.ML	Sun May 31 14:51:21 2009 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4  use "ML-Systems/thread_dummy.ML";
     6.5  use "ML-Systems/ml_name_space.ML";
     6.6  use "ML-Systems/polyml_common.ML";
     6.7 -use "ML-Systems/polyml_old_compiler5.ML";
     6.8 +use "ML-Systems/compiler_polyml-5.0.ML";
     6.9  use "ML-Systems/polyml_pp.ML";
    6.10  
    6.11  val pointer_eq = PolyML.pointerEq;
     7.1 --- a/src/Pure/ML-Systems/polyml-experimental.ML	Sun May 31 14:46:44 2009 +0200
     7.2 +++ b/src/Pure/ML-Systems/polyml-experimental.ML	Sun May 31 14:51:21 2009 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4 -(*  Title:      Pure/ML-Systems/polyml.ML
     7.5 +(*  Title:      Pure/ML-Systems/polyml-experimental.ML
     7.6  
     7.7 -Compatibility wrapper for experimental versions of Poly/ML after 5.2.1.
     7.8 +Compatibility wrapper for Poly/ML 5.3 (SVN experimental).
     7.9  *)
    7.10  
    7.11  open Thread;
    7.12 @@ -19,58 +19,7 @@
    7.13  
    7.14  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    7.15  
    7.16 -
    7.17 -(* runtime compilation *)
    7.18 -
    7.19 -local
    7.20 -
    7.21 -fun drop_newline s =
    7.22 -  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    7.23 -  else s;
    7.24 -
    7.25 -in
    7.26 -
    7.27 -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    7.28 -    (start_line, name) verbose txt =
    7.29 -  let
    7.30 -    val current_line = ref start_line;
    7.31 -    val in_buffer = ref (String.explode (tune_source txt));
    7.32 -    val out_buffer = ref ([]: string list);
    7.33 -    fun output () = drop_newline (implode (rev (! out_buffer)));
    7.34 -
    7.35 -    fun get () =
    7.36 -      (case ! in_buffer of
    7.37 -        [] => NONE
    7.38 -      | c :: cs =>
    7.39 -          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    7.40 -    fun put s = out_buffer := s :: ! out_buffer;
    7.41 -    fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
    7.42 -     (put (if hard then "Error: " else "Warning: ");
    7.43 -      PolyML.prettyPrint (put, 76) msg1;
    7.44 -      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    7.45 -      put ("At" ^ str_of_pos line name ^ "\n"));
    7.46 -
    7.47 -    val parameters =
    7.48 -     [PolyML.Compiler.CPOutStream put,
    7.49 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    7.50 -      PolyML.Compiler.CPErrorMessageProc put_message,
    7.51 -      PolyML.Compiler.CPNameSpace name_space,
    7.52 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
    7.53 -    val _ =
    7.54 -      (while not (List.null (! in_buffer)) do
    7.55 -        PolyML.compiler (get, parameters) ())
    7.56 -      handle exn =>
    7.57 -       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    7.58 -        error (output ()); raise exn);
    7.59 -  in if verbose then print (output ()) else () end;
    7.60 -
    7.61 -fun use_file context verbose name =
    7.62 -  let
    7.63 -    val instream = TextIO.openIn name;
    7.64 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    7.65 -  in use_text context (1, name) verbose txt end;
    7.66 -
    7.67 -end;
    7.68 +use "ML-Systems/compiler_polyml-5.3.ML";
    7.69  
    7.70  
    7.71  (* toplevel pretty printing *)
     8.1 --- a/src/Pure/ML-Systems/polyml.ML	Sun May 31 14:46:44 2009 +0200
     8.2 +++ b/src/Pure/ML-Systems/polyml.ML	Sun May 31 14:51:21 2009 +0200
     8.3 @@ -1,6 +1,6 @@
     8.4  (*  Title:      Pure/ML-Systems/polyml.ML
     8.5  
     8.6 -Compatibility wrapper for Poly/ML 5.2 or later.
     8.7 +Compatibility wrapper for Poly/ML 5.2 and 5.2.1.
     8.8  *)
     8.9  
    8.10  open Thread;
    8.11 @@ -22,54 +22,6 @@
    8.12  
    8.13  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    8.14  
    8.15 -
    8.16 -(* runtime compilation *)
    8.17 -
    8.18 -local
    8.19 -
    8.20 -fun drop_newline s =
    8.21 -  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    8.22 -  else s;
    8.23 -
    8.24 -in
    8.25 -
    8.26 -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    8.27 -    (start_line, name) verbose txt =
    8.28 -  let
    8.29 -    val current_line = ref start_line;
    8.30 -    val in_buffer = ref (String.explode (tune_source txt));
    8.31 -    val out_buffer = ref ([]: string list);
    8.32 -    fun output () = drop_newline (implode (rev (! out_buffer)));
    8.33 -
    8.34 -    fun get () =
    8.35 -      (case ! in_buffer of
    8.36 -        [] => NONE
    8.37 -      | c :: cs =>
    8.38 -          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    8.39 -    fun put s = out_buffer := s :: ! out_buffer;
    8.40 -    fun message (msg, is_err, line) =
    8.41 -      (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
    8.42 -
    8.43 -    val parameters =
    8.44 -     [PolyML.Compiler.CPOutStream put,
    8.45 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    8.46 -      PolyML.Compiler.CPErrorMessageProc (put o message),
    8.47 -      PolyML.Compiler.CPNameSpace name_space];
    8.48 -    val _ =
    8.49 -      (while not (List.null (! in_buffer)) do
    8.50 -        PolyML.compiler (get, parameters) ())
    8.51 -      handle exn =>
    8.52 -       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    8.53 -        error (output ()); raise exn);
    8.54 -  in if verbose then print (output ()) else () end;
    8.55 -
    8.56 -fun use_file context verbose name =
    8.57 -  let
    8.58 -    val instream = TextIO.openIn name;
    8.59 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    8.60 -  in use_text context (1, name) verbose txt end;
    8.61 -
    8.62 -end;
    8.63 -
    8.64 +use "ML-Systems/compiler_polyml-5.2.ML";
    8.65  use "ML-Systems/polyml_pp.ML";
    8.66  
     9.1 --- a/src/Pure/ML-Systems/polyml_old_compiler5.ML	Sun May 31 14:46:44 2009 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,32 +0,0 @@
     9.4 -(*  Title:      Pure/ML-Systems/polyml_old_compiler5.ML
     9.5 -
     9.6 -Runtime compilation -- for old PolyML.compilerEx (version 5.0, 5.1).
     9.7 -*)
     9.8 -
     9.9 -fun use_text ({tune_source, print, error, ...}: use_context) (line, name) verbose txt =
    9.10 -  let
    9.11 -    val in_buffer = ref (explode (tune_source txt));
    9.12 -    val out_buffer = ref ([]: string list);
    9.13 -    fun output () = implode (rev (case ! out_buffer of "\n" :: cs => cs | cs => cs));
    9.14 -
    9.15 -    val current_line = ref line;
    9.16 -    fun get () =
    9.17 -      (case ! in_buffer of
    9.18 -        [] => ""
    9.19 -      | c :: cs => (in_buffer := cs; if c = "\n" then current_line := ! current_line + 1 else (); c));
    9.20 -    fun put s = out_buffer := s :: ! out_buffer;
    9.21 -
    9.22 -    fun exec () =
    9.23 -      (case ! in_buffer of
    9.24 -        [] => ()
    9.25 -      | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
    9.26 -  in
    9.27 -    exec () handle exn => (error (output ()); raise exn);
    9.28 -    if verbose then print (output ()) else ()
    9.29 -  end;
    9.30 -
    9.31 -fun use_file context verbose name =
    9.32 -  let
    9.33 -    val instream = TextIO.openIn name;
    9.34 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    9.35 -  in use_text context (1, name) verbose txt end;