simplified Poly/ML setup -- 5.3.0 is now the common base-line;
authorwenzelm
Thu May 24 15:33:45 2012 +0200 (2012-05-24)
changeset 47980c81801f881b3
parent 47979 59ec72d3d0b9
child 47986 ca7104aebb74
simplified Poly/ML setup -- 5.3.0 is now the common base-line;
src/Pure/General/linear_set.ML
src/Pure/General/table.ML
src/Pure/IsaMakefile
src/Pure/ML-Systems/compiler_polyml-5.3.ML
src/Pure/ML-Systems/compiler_polyml.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML/install_pp_polyml-5.3.ML
src/Pure/ML/install_pp_polyml.ML
src/Pure/ML/ml_compiler_polyml-5.3.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/ROOT.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/General/linear_set.ML	Thu May 24 15:01:17 2012 +0200
     1.2 +++ b/src/Pure/General/linear_set.ML	Thu May 24 15:33:45 2012 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4            in (start, entries') end)));
     1.5  
     1.6  
     1.7 -(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
     1.8 +(* ML pretty-printing *)
     1.9  
    1.10  val _ =
    1.11    PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
     2.1 --- a/src/Pure/General/table.ML	Thu May 24 15:01:17 2012 +0200
     2.2 +++ b/src/Pure/General/table.ML	Thu May 24 15:33:45 2012 +0200
     2.3 @@ -394,7 +394,7 @@
     2.4  fun merge_list eq = join (fn _ => Library.merge eq);
     2.5  
     2.6  
     2.7 -(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
     2.8 +(* ML pretty-printing *)
     2.9  
    2.10  val _ =
    2.11    PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
     3.1 --- a/src/Pure/IsaMakefile	Thu May 24 15:01:17 2012 +0200
     3.2 +++ b/src/Pure/IsaMakefile	Thu May 24 15:33:45 2012 +0200
     3.3 @@ -23,7 +23,7 @@
     3.4  
     3.5  BOOTSTRAP_FILES = 					\
     3.6    General/exn.ML					\
     3.7 -  ML-Systems/compiler_polyml-5.3.ML			\
     3.8 +  ML-Systems/compiler_polyml.ML			\
     3.9    ML-Systems/ml_name_space.ML				\
    3.10    ML-Systems/ml_pretty.ML				\
    3.11    ML-Systems/ml_system.ML				\
    3.12 @@ -31,7 +31,6 @@
    3.13    ML-Systems/multithreading_polyml.ML			\
    3.14    ML-Systems/overloading_smlnj.ML			\
    3.15    ML-Systems/polyml.ML					\
    3.16 -  ML-Systems/polyml_common.ML				\
    3.17    ML-Systems/pp_dummy.ML				\
    3.18    ML-Systems/proper_int.ML				\
    3.19    ML-Systems/single_assignment.ML			\
    3.20 @@ -141,10 +140,10 @@
    3.21    Isar/token.ML						\
    3.22    Isar/toplevel.ML					\
    3.23    Isar/typedecl.ML					\
    3.24 -  ML/install_pp_polyml-5.3.ML				\
    3.25 +  ML/install_pp_polyml.ML				\
    3.26    ML/ml_antiquote.ML					\
    3.27    ML/ml_compiler.ML					\
    3.28 -  ML/ml_compiler_polyml-5.3.ML				\
    3.29 +  ML/ml_compiler_polyml.ML				\
    3.30    ML/ml_context.ML					\
    3.31    ML/ml_env.ML						\
    3.32    ML/ml_lex.ML						\
     4.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu May 24 15:01:17 2012 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,57 +0,0 @@
     4.4 -(*  Title:      Pure/ML-Systems/compiler_polyml-5.3.ML
     4.5 -
     4.6 -Runtime compilation for Poly/ML 5.3.0 and 5.4.0.
     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 line = Unsynchronized.ref start_line;
    4.21 -    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
    4.22 -    val out_buffer = Unsynchronized.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 => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
    4.29 -    fun put s = out_buffer := s :: ! out_buffer;
    4.30 -    fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
    4.31 -     (put (if hard then "Error: " else "Warning: ");
    4.32 -      PolyML.prettyPrint (put, 76) msg1;
    4.33 -      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    4.34 -      put ("At" ^ str_of_pos line name ^ "\n"));
    4.35 -
    4.36 -    val parameters =
    4.37 -     [PolyML.Compiler.CPOutStream put,
    4.38 -      PolyML.Compiler.CPNameSpace name_space,
    4.39 -      PolyML.Compiler.CPErrorMessageProc put_message,
    4.40 -      PolyML.Compiler.CPLineNo (fn () => ! line),
    4.41 -      PolyML.Compiler.CPFileName name,
    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 -        if Exn.is_interrupt exn then reraise exn
    4.48 -        else
    4.49 -         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    4.50 -          error (output ()); reraise exn);
    4.51 -  in if verbose then print (output ()) else () end;
    4.52 -
    4.53 -fun use_file context verbose name =
    4.54 -  let
    4.55 -    val instream = TextIO.openIn name;
    4.56 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    4.57 -  in use_text context (1, name) verbose txt end;
    4.58 -
    4.59 -end;
    4.60 -
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/ML-Systems/compiler_polyml.ML	Thu May 24 15:33:45 2012 +0200
     5.3 @@ -0,0 +1,59 @@
     5.4 +(*  Title:      Pure/ML-Systems/compiler_polyml.ML
     5.5 +
     5.6 +Runtime compilation for Poly/ML 5.3.0 or later.
     5.7 +
     5.8 +See also Pure/ML/ml_compiler_polyml.ML for advanced version.
     5.9 +*)
    5.10 +
    5.11 +local
    5.12 +
    5.13 +fun drop_newline s =
    5.14 +  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    5.15 +  else s;
    5.16 +
    5.17 +in
    5.18 +
    5.19 +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    5.20 +    (start_line, name) verbose txt =
    5.21 +  let
    5.22 +    val line = Unsynchronized.ref start_line;
    5.23 +    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
    5.24 +    val out_buffer = Unsynchronized.ref ([]: string list);
    5.25 +    fun output () = drop_newline (implode (rev (! out_buffer)));
    5.26 +
    5.27 +    fun get () =
    5.28 +      (case ! in_buffer of
    5.29 +        [] => NONE
    5.30 +      | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
    5.31 +    fun put s = out_buffer := s :: ! out_buffer;
    5.32 +    fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
    5.33 +     (put (if hard then "Error: " else "Warning: ");
    5.34 +      PolyML.prettyPrint (put, 76) msg1;
    5.35 +      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
    5.36 +      put ("At" ^ str_of_pos line name ^ "\n"));
    5.37 +
    5.38 +    val parameters =
    5.39 +     [PolyML.Compiler.CPOutStream put,
    5.40 +      PolyML.Compiler.CPNameSpace name_space,
    5.41 +      PolyML.Compiler.CPErrorMessageProc put_message,
    5.42 +      PolyML.Compiler.CPLineNo (fn () => ! line),
    5.43 +      PolyML.Compiler.CPFileName name,
    5.44 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
    5.45 +    val _ =
    5.46 +      (while not (List.null (! in_buffer)) do
    5.47 +        PolyML.compiler (get, parameters) ())
    5.48 +      handle exn =>
    5.49 +        if Exn.is_interrupt exn then reraise exn
    5.50 +        else
    5.51 +         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    5.52 +          error (output ()); reraise exn);
    5.53 +  in if verbose then print (output ()) else () end;
    5.54 +
    5.55 +fun use_file context verbose name =
    5.56 +  let
    5.57 +    val instream = TextIO.openIn name;
    5.58 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    5.59 +  in use_text context (1, name) verbose txt end;
    5.60 +
    5.61 +end;
    5.62 +
     6.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu May 24 15:01:17 2012 +0200
     6.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu May 24 15:33:45 2012 +0200
     6.3 @@ -1,16 +1,10 @@
     6.4  (*  Title:      Pure/ML-Systems/polyml.ML
     6.5 +    Author:     Makarius
     6.6  
     6.7 -Compatibility wrapper for Poly/ML 5.3 and 5.4.
     6.8 +Compatibility wrapper for Poly/ML 5.3.0 or later.
     6.9  *)
    6.10  
    6.11 -open Thread;
    6.12 -
    6.13 -structure ML_Name_Space =
    6.14 -struct
    6.15 -  open PolyML.NameSpace;
    6.16 -  type T = PolyML.NameSpace.nameSpace;
    6.17 -  val global = PolyML.globalNameSpace;
    6.18 -end;
    6.19 +(* exceptions *)
    6.20  
    6.21  fun reraise exn =
    6.22    (case PolyML.exceptionLocation exn of
    6.23 @@ -33,22 +27,104 @@
    6.24      NONE => NONE
    6.25    | SOME i => if i >= 0 then NONE else SOME (~ i));
    6.26  
    6.27 -use "ML-Systems/polyml_common.ML";
    6.28 +exception Interrupt = SML90.Interrupt;
    6.29 +
    6.30 +use "General/exn.ML";
    6.31 +
    6.32 +
    6.33 +(* multithreading *)
    6.34 +
    6.35 +val seconds = Time.fromReal;
    6.36 +
    6.37 +if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
    6.38 +then ()
    6.39 +else use "ML-Systems/single_assignment_polyml.ML";
    6.40 +
    6.41 +open Thread;
    6.42 +use "ML-Systems/multithreading.ML";
    6.43  use "ML-Systems/multithreading_polyml.ML";
    6.44 +
    6.45  use "ML-Systems/unsynchronized.ML";
    6.46 -
    6.47  val _ = PolyML.Compiler.forgetValue "ref";
    6.48  val _ = PolyML.Compiler.forgetType "ref";
    6.49  
    6.50 +
    6.51 +(* pervasive environment *)
    6.52 +
    6.53 +fun op before (a, _: unit) = a;
    6.54 +
    6.55 +val _ = PolyML.Compiler.forgetValue "isSome";
    6.56 +val _ = PolyML.Compiler.forgetValue "getOpt";
    6.57 +val _ = PolyML.Compiler.forgetValue "valOf";
    6.58 +val _ = PolyML.Compiler.forgetValue "foldl";
    6.59 +val _ = PolyML.Compiler.forgetValue "foldr";
    6.60 +val _ = PolyML.Compiler.forgetValue "print";
    6.61 +val _ = PolyML.Compiler.forgetValue "explode";
    6.62 +val _ = PolyML.Compiler.forgetValue "concat";
    6.63 +
    6.64 +val ord = SML90.ord;
    6.65 +val chr = SML90.chr;
    6.66 +val raw_explode = SML90.explode;
    6.67 +val implode = SML90.implode;
    6.68 +
    6.69 +fun quit () = exit 0;
    6.70 +
    6.71 +
    6.72 +(* ML system identification *)
    6.73 +
    6.74 +use "ML-Systems/ml_system.ML";
    6.75 +
    6.76 +
    6.77 +(* ML runtime system *)
    6.78 +
    6.79 +val exception_trace = PolyML.exception_trace;
    6.80 +val timing = PolyML.timing;
    6.81 +val profiling = PolyML.profiling;
    6.82 +
    6.83 +fun profile 0 f x = f x
    6.84 +  | profile n f x =
    6.85 +      let
    6.86 +        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
    6.87 +        val res = Exn.capture f x;
    6.88 +        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
    6.89 +      in Exn.release res end;
    6.90 +
    6.91  val pointer_eq = PolyML.pointerEq;
    6.92  
    6.93  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
    6.94  
    6.95 -use "ML-Systems/compiler_polyml-5.3.ML";
    6.96 +
    6.97 +(* ML compiler *)
    6.98 +
    6.99 +structure ML_Name_Space =
   6.100 +struct
   6.101 +  open PolyML.NameSpace;
   6.102 +  type T = PolyML.NameSpace.nameSpace;
   6.103 +  val global = PolyML.globalNameSpace;
   6.104 +end;
   6.105 +
   6.106 +use "ML-Systems/use_context.ML";
   6.107 +use "ML-Systems/compiler_polyml.ML";
   6.108 +
   6.109  PolyML.Compiler.reportUnreferencedIds := true;
   6.110 +PolyML.Compiler.printInAlphabeticalOrder := false;
   6.111 +PolyML.Compiler.maxInlineSize := 80;
   6.112 +
   6.113 +fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
   6.114  
   6.115  
   6.116 -(* toplevel pretty printing *)
   6.117 +(* ML toplevel pretty printing *)
   6.118 +
   6.119 +use "ML-Systems/ml_pretty.ML";
   6.120 +
   6.121 +local
   6.122 +  val depth = Unsynchronized.ref 10;
   6.123 +in
   6.124 +  fun get_print_depth () = ! depth;
   6.125 +  fun print_depth n = (depth := n; PolyML.print_depth n);
   6.126 +end;
   6.127 +
   6.128 +val error_depth = PolyML.error_depth;
   6.129  
   6.130  val pretty_ml =
   6.131    let
   6.132 @@ -87,5 +163,3 @@
   6.133  val ml_make_string =
   6.134    "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
   6.135  
   6.136 -use "ML-Systems/ml_system.ML";
   6.137 -
     7.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Thu May 24 15:01:17 2012 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,88 +0,0 @@
     7.4 -(*  Title:      Pure/ML-Systems/polyml_common.ML
     7.5 -
     7.6 -Compatibility file for Poly/ML -- common part for 5.x.
     7.7 -*)
     7.8 -
     7.9 -fun op before (a, _: unit) = a;
    7.10 -
    7.11 -exception Interrupt = SML90.Interrupt;
    7.12 -
    7.13 -use "General/exn.ML";
    7.14 -
    7.15 -if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
    7.16 -then ()
    7.17 -else use "ML-Systems/single_assignment_polyml.ML";
    7.18 -
    7.19 -use "ML-Systems/multithreading.ML";
    7.20 -use "ML-Systems/ml_pretty.ML";
    7.21 -use "ML-Systems/use_context.ML";
    7.22 -
    7.23 -val seconds = Time.fromReal;
    7.24 -
    7.25 -
    7.26 -
    7.27 -(** ML system and platform related **)
    7.28 -
    7.29 -val _ = PolyML.Compiler.forgetValue "isSome";
    7.30 -val _ = PolyML.Compiler.forgetValue "getOpt";
    7.31 -val _ = PolyML.Compiler.forgetValue "valOf";
    7.32 -val _ = PolyML.Compiler.forgetValue "foldl";
    7.33 -val _ = PolyML.Compiler.forgetValue "foldr";
    7.34 -val _ = PolyML.Compiler.forgetValue "print";
    7.35 -val _ = PolyML.Compiler.forgetValue "explode";
    7.36 -val _ = PolyML.Compiler.forgetValue "concat";
    7.37 -
    7.38 -
    7.39 -(* Compiler options *)
    7.40 -
    7.41 -PolyML.Compiler.printInAlphabeticalOrder := false;
    7.42 -PolyML.Compiler.maxInlineSize := 80;
    7.43 -
    7.44 -
    7.45 -(* old Poly/ML emulation *)
    7.46 -
    7.47 -fun quit () = exit 0;
    7.48 -
    7.49 -
    7.50 -(* restore old-style character / string functions *)
    7.51 -
    7.52 -val ord = SML90.ord;
    7.53 -val chr = SML90.chr;
    7.54 -val raw_explode = SML90.explode;
    7.55 -val implode = SML90.implode;
    7.56 -
    7.57 -
    7.58 -(* prompts *)
    7.59 -
    7.60 -fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
    7.61 -
    7.62 -
    7.63 -(* toplevel printing *)
    7.64 -
    7.65 -local
    7.66 -  val depth = ref 10;
    7.67 -in
    7.68 -  fun get_print_depth () = ! depth;
    7.69 -  fun print_depth n = (depth := n; PolyML.print_depth n);
    7.70 -end;
    7.71 -
    7.72 -val error_depth = PolyML.error_depth;
    7.73 -
    7.74 -val ml_make_string = "PolyML.makestring";
    7.75 -
    7.76 -
    7.77 -
    7.78 -(** Runtime system **)
    7.79 -
    7.80 -val exception_trace = PolyML.exception_trace;
    7.81 -val timing = PolyML.timing;
    7.82 -val profiling = PolyML.profiling;
    7.83 -
    7.84 -fun profile 0 f x = f x
    7.85 -  | profile n f x =
    7.86 -      let
    7.87 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
    7.88 -        val res = Exn.capture f x;
    7.89 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
    7.90 -      in Exn.release res end;
    7.91 -
     8.1 --- a/src/Pure/ML/install_pp_polyml-5.3.ML	Thu May 24 15:01:17 2012 +0200
     8.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.3 @@ -1,53 +0,0 @@
     8.4 -(*  Title:      Pure/ML/install_pp_polyml-5.3.ML
     8.5 -    Author:     Makarius
     8.6 -
     8.7 -Extra toplevel pretty-printing for Poly/ML 5.3.0.
     8.8 -*)
     8.9 -
    8.10 -PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
    8.11 -  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
    8.12 -
    8.13 -PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
    8.14 -  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
    8.15 -
    8.16 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
    8.17 -  pretty (Synchronized.value var, depth));
    8.18 -
    8.19 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    8.20 -  (case Future.peek x of
    8.21 -    NONE => PolyML.PrettyString "<future>"
    8.22 -  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    8.23 -  | SOME (Exn.Res y) => pretty (y, depth)));
    8.24 -
    8.25 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    8.26 -  (case Lazy.peek x of
    8.27 -    NONE => PolyML.PrettyString "<lazy>"
    8.28 -  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    8.29 -  | SOME (Exn.Res y) => pretty (y, depth)));
    8.30 -
    8.31 -PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
    8.32 -  let
    8.33 -    open PolyML;
    8.34 -    val from_ML = Pretty.from_ML o pretty_ml;
    8.35 -    fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
    8.36 -    fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
    8.37 -    fun prt_term parens dp (t as _ $ _) =
    8.38 -          op :: (strip_comb t)
    8.39 -          |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
    8.40 -          |> Pretty.separate " $"
    8.41 -          |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
    8.42 -      | prt_term _ dp (Abs (x, T, body)) =
    8.43 -          prt_apps "Abs"
    8.44 -           [from_ML (prettyRepresentation (x, dp - 1)),
    8.45 -            from_ML (prettyRepresentation (T, dp - 2)),
    8.46 -            prt_term false (dp - 3) body]
    8.47 -      | prt_term _ dp (Const const) =
    8.48 -          prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
    8.49 -      | prt_term _ dp (Free free) =
    8.50 -          prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
    8.51 -      | prt_term _ dp (Var var) =
    8.52 -          prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
    8.53 -      | prt_term _ dp (Bound i) =
    8.54 -          prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
    8.55 -  in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
    8.56 -
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/src/Pure/ML/install_pp_polyml.ML	Thu May 24 15:33:45 2012 +0200
     9.3 @@ -0,0 +1,53 @@
     9.4 +(*  Title:      Pure/ML/install_pp_polyml.ML
     9.5 +    Author:     Makarius
     9.6 +
     9.7 +Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
     9.8 +*)
     9.9 +
    9.10 +PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
    9.11 +  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
    9.12 +
    9.13 +PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
    9.14 +  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
    9.15 +
    9.16 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
    9.17 +  pretty (Synchronized.value var, depth));
    9.18 +
    9.19 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    9.20 +  (case Future.peek x of
    9.21 +    NONE => PolyML.PrettyString "<future>"
    9.22 +  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    9.23 +  | SOME (Exn.Res y) => pretty (y, depth)));
    9.24 +
    9.25 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    9.26 +  (case Lazy.peek x of
    9.27 +    NONE => PolyML.PrettyString "<lazy>"
    9.28 +  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    9.29 +  | SOME (Exn.Res y) => pretty (y, depth)));
    9.30 +
    9.31 +PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
    9.32 +  let
    9.33 +    open PolyML;
    9.34 +    val from_ML = Pretty.from_ML o pretty_ml;
    9.35 +    fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
    9.36 +    fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
    9.37 +    fun prt_term parens dp (t as _ $ _) =
    9.38 +          op :: (strip_comb t)
    9.39 +          |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
    9.40 +          |> Pretty.separate " $"
    9.41 +          |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
    9.42 +      | prt_term _ dp (Abs (x, T, body)) =
    9.43 +          prt_apps "Abs"
    9.44 +           [from_ML (prettyRepresentation (x, dp - 1)),
    9.45 +            from_ML (prettyRepresentation (T, dp - 2)),
    9.46 +            prt_term false (dp - 3) body]
    9.47 +      | prt_term _ dp (Const const) =
    9.48 +          prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
    9.49 +      | prt_term _ dp (Free free) =
    9.50 +          prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
    9.51 +      | prt_term _ dp (Var var) =
    9.52 +          prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
    9.53 +      | prt_term _ dp (Bound i) =
    9.54 +          prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
    9.55 +  in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
    9.56 +
    10.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu May 24 15:01:17 2012 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,202 +0,0 @@
    10.4 -(*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML
    10.5 -    Author:     Makarius
    10.6 -
    10.7 -Advanced runtime compilation for Poly/ML 5.3.0 or later.
    10.8 -*)
    10.9 -
   10.10 -structure ML_Compiler: ML_COMPILER =
   10.11 -struct
   10.12 -
   10.13 -(* source locations *)
   10.14 -
   10.15 -fun position_of (loc: PolyML.location) =
   10.16 -  let
   10.17 -    val {file = text, startLine = line, startPosition = offset,
   10.18 -      endLine = _, endPosition = end_offset} = loc;
   10.19 -    val props =
   10.20 -      (case YXML.parse text of
   10.21 -        XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
   10.22 -      | XML.Text s => Position.file_name s);
   10.23 -  in
   10.24 -    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   10.25 -  end;
   10.26 -
   10.27 -fun exn_position exn =
   10.28 -  (case PolyML.exceptionLocation exn of
   10.29 -    NONE => Position.none
   10.30 -  | SOME loc => position_of loc);
   10.31 -
   10.32 -val exn_messages = Runtime.exn_messages exn_position;
   10.33 -val exn_message = Runtime.exn_message exn_position;
   10.34 -
   10.35 -
   10.36 -(* parse trees *)
   10.37 -
   10.38 -fun report_parse_tree depth space =
   10.39 -  let
   10.40 -    val reported_text =
   10.41 -      (case Context.thread_data () of
   10.42 -        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
   10.43 -      | _ => Position.reported_text);
   10.44 -
   10.45 -    fun reported_entity kind loc decl =
   10.46 -      reported_text (position_of loc)
   10.47 -        (Isabelle_Markup.entityN,
   10.48 -          (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   10.49 -
   10.50 -    fun reported loc (PolyML.PTtype types) =
   10.51 -          cons
   10.52 -            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
   10.53 -              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   10.54 -              |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
   10.55 -      | reported loc (PolyML.PTdeclaredAt decl) =
   10.56 -          cons (reported_entity Isabelle_Markup.ML_defN loc decl)
   10.57 -      | reported loc (PolyML.PTopenedAt decl) =
   10.58 -          cons (reported_entity Isabelle_Markup.ML_openN loc decl)
   10.59 -      | reported loc (PolyML.PTstructureAt decl) =
   10.60 -          cons (reported_entity Isabelle_Markup.ML_structN loc decl)
   10.61 -      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
   10.62 -      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
   10.63 -      | reported _ _ = I
   10.64 -    and reported_tree (loc, props) = fold (reported loc) props;
   10.65 -  in fn tree => Output.report (implode (reported_tree tree [])) end;
   10.66 -
   10.67 -
   10.68 -(* eval ML source tokens *)
   10.69 -
   10.70 -fun eval verbose pos toks =
   10.71 -  let
   10.72 -    val _ = Secure.secure_mltext ();
   10.73 -    val space = ML_Env.name_space;
   10.74 -
   10.75 -
   10.76 -    (* input *)
   10.77 -
   10.78 -    val location_props =
   10.79 -      op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
   10.80 -            (filter (member (op =)
   10.81 -              [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
   10.82 -
   10.83 -    val input_buffer =
   10.84 -      Unsynchronized.ref (toks |> map
   10.85 -        (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
   10.86 -
   10.87 -    fun get () =
   10.88 -      (case ! input_buffer of
   10.89 -        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
   10.90 -      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
   10.91 -      | [] => NONE);
   10.92 -
   10.93 -    fun get_pos () =
   10.94 -      (case ! input_buffer of
   10.95 -        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
   10.96 -      | ([], tok) :: _ => ML_Lex.end_pos_of tok
   10.97 -      | [] => Position.none);
   10.98 -
   10.99 -
  10.100 -    (* output channels *)
  10.101 -
  10.102 -    val writeln_buffer = Unsynchronized.ref Buffer.empty;
  10.103 -    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
  10.104 -    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
  10.105 -
  10.106 -    val warnings = Unsynchronized.ref ([]: string list);
  10.107 -    fun warn msg = Unsynchronized.change warnings (cons msg);
  10.108 -    fun output_warnings () = List.app warning (rev (! warnings));
  10.109 -
  10.110 -    val error_buffer = Unsynchronized.ref Buffer.empty;
  10.111 -    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
  10.112 -    fun flush_error () = writeln (Buffer.content (! error_buffer));
  10.113 -    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
  10.114 -
  10.115 -    fun message {message = msg, hard, location = loc, context = _} =
  10.116 -      let
  10.117 -        val pos = position_of loc;
  10.118 -        val txt =
  10.119 -          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
  10.120 -            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
  10.121 -          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
  10.122 -          Position.reported_text pos Isabelle_Markup.report "";
  10.123 -      in if hard then err txt else warn txt end;
  10.124 -
  10.125 -
  10.126 -    (* results *)
  10.127 -
  10.128 -    val depth = get_print_depth ();
  10.129 -
  10.130 -    fun apply_result {fixes, types, signatures, structures, functors, values} =
  10.131 -      let
  10.132 -        fun display disp x =
  10.133 -          if depth > 0 then
  10.134 -            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
  10.135 -          else ();
  10.136 -
  10.137 -        fun apply_fix (a, b) =
  10.138 -          (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
  10.139 -        fun apply_type (a, b) =
  10.140 -          (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
  10.141 -        fun apply_sig (a, b) =
  10.142 -          (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
  10.143 -        fun apply_struct (a, b) =
  10.144 -          (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
  10.145 -        fun apply_funct (a, b) =
  10.146 -          (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
  10.147 -        fun apply_val (a, b) =
  10.148 -          (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
  10.149 -      in
  10.150 -        List.app apply_fix fixes;
  10.151 -        List.app apply_type types;
  10.152 -        List.app apply_sig signatures;
  10.153 -        List.app apply_struct structures;
  10.154 -        List.app apply_funct functors;
  10.155 -        List.app apply_val values
  10.156 -      end;
  10.157 -
  10.158 -    exception STATIC_ERRORS of unit;
  10.159 -
  10.160 -    fun result_fun (phase1, phase2) () =
  10.161 -     ((case phase1 of
  10.162 -        NONE => ()
  10.163 -      | SOME parse_tree => report_parse_tree depth space parse_tree);
  10.164 -      (case phase2 of
  10.165 -        NONE => raise STATIC_ERRORS ()
  10.166 -      | SOME code =>
  10.167 -          apply_result
  10.168 -            ((code
  10.169 -              |> Runtime.debugging
  10.170 -              |> Runtime.toplevel_error (err o exn_message)) ())));
  10.171 -
  10.172 -
  10.173 -    (* compiler invocation *)
  10.174 -
  10.175 -    val parameters =
  10.176 -     [PolyML.Compiler.CPOutStream write,
  10.177 -      PolyML.Compiler.CPNameSpace space,
  10.178 -      PolyML.Compiler.CPErrorMessageProc message,
  10.179 -      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
  10.180 -      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
  10.181 -      PolyML.Compiler.CPFileName location_props,
  10.182 -      PolyML.Compiler.CPCompilerResultFun result_fun,
  10.183 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
  10.184 -    val _ =
  10.185 -      (while not (List.null (! input_buffer)) do
  10.186 -        PolyML.compiler (get, parameters) ())
  10.187 -      handle exn =>
  10.188 -        if Exn.is_interrupt exn then reraise exn
  10.189 -        else
  10.190 -          let
  10.191 -            val exn_msg =
  10.192 -              (case exn of
  10.193 -                STATIC_ERRORS () => ""
  10.194 -              | Runtime.TOPLEVEL_ERROR => ""
  10.195 -              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
  10.196 -            val _ = output_warnings ();
  10.197 -            val _ = output_writeln ();
  10.198 -          in raise_error exn_msg end;
  10.199 -  in
  10.200 -    if verbose then (output_warnings (); flush_error (); output_writeln ())
  10.201 -    else ()
  10.202 -  end;
  10.203 -
  10.204 -end;
  10.205 -
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu May 24 15:33:45 2012 +0200
    11.3 @@ -0,0 +1,202 @@
    11.4 +(*  Title:      Pure/ML/ml_compiler_polyml.ML
    11.5 +    Author:     Makarius
    11.6 +
    11.7 +Advanced runtime compilation for Poly/ML 5.3.0 or later.
    11.8 +*)
    11.9 +
   11.10 +structure ML_Compiler: ML_COMPILER =
   11.11 +struct
   11.12 +
   11.13 +(* source locations *)
   11.14 +
   11.15 +fun position_of (loc: PolyML.location) =
   11.16 +  let
   11.17 +    val {file = text, startLine = line, startPosition = offset,
   11.18 +      endLine = _, endPosition = end_offset} = loc;
   11.19 +    val props =
   11.20 +      (case YXML.parse text of
   11.21 +        XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
   11.22 +      | XML.Text s => Position.file_name s);
   11.23 +  in
   11.24 +    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   11.25 +  end;
   11.26 +
   11.27 +fun exn_position exn =
   11.28 +  (case PolyML.exceptionLocation exn of
   11.29 +    NONE => Position.none
   11.30 +  | SOME loc => position_of loc);
   11.31 +
   11.32 +val exn_messages = Runtime.exn_messages exn_position;
   11.33 +val exn_message = Runtime.exn_message exn_position;
   11.34 +
   11.35 +
   11.36 +(* parse trees *)
   11.37 +
   11.38 +fun report_parse_tree depth space =
   11.39 +  let
   11.40 +    val reported_text =
   11.41 +      (case Context.thread_data () of
   11.42 +        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
   11.43 +      | _ => Position.reported_text);
   11.44 +
   11.45 +    fun reported_entity kind loc decl =
   11.46 +      reported_text (position_of loc)
   11.47 +        (Isabelle_Markup.entityN,
   11.48 +          (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   11.49 +
   11.50 +    fun reported loc (PolyML.PTtype types) =
   11.51 +          cons
   11.52 +            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
   11.53 +              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   11.54 +              |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
   11.55 +      | reported loc (PolyML.PTdeclaredAt decl) =
   11.56 +          cons (reported_entity Isabelle_Markup.ML_defN loc decl)
   11.57 +      | reported loc (PolyML.PTopenedAt decl) =
   11.58 +          cons (reported_entity Isabelle_Markup.ML_openN loc decl)
   11.59 +      | reported loc (PolyML.PTstructureAt decl) =
   11.60 +          cons (reported_entity Isabelle_Markup.ML_structN loc decl)
   11.61 +      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
   11.62 +      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
   11.63 +      | reported _ _ = I
   11.64 +    and reported_tree (loc, props) = fold (reported loc) props;
   11.65 +  in fn tree => Output.report (implode (reported_tree tree [])) end;
   11.66 +
   11.67 +
   11.68 +(* eval ML source tokens *)
   11.69 +
   11.70 +fun eval verbose pos toks =
   11.71 +  let
   11.72 +    val _ = Secure.secure_mltext ();
   11.73 +    val space = ML_Env.name_space;
   11.74 +
   11.75 +
   11.76 +    (* input *)
   11.77 +
   11.78 +    val location_props =
   11.79 +      op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
   11.80 +            (filter (member (op =)
   11.81 +              [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
   11.82 +
   11.83 +    val input_buffer =
   11.84 +      Unsynchronized.ref (toks |> map
   11.85 +        (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
   11.86 +
   11.87 +    fun get () =
   11.88 +      (case ! input_buffer of
   11.89 +        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
   11.90 +      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
   11.91 +      | [] => NONE);
   11.92 +
   11.93 +    fun get_pos () =
   11.94 +      (case ! input_buffer of
   11.95 +        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
   11.96 +      | ([], tok) :: _ => ML_Lex.end_pos_of tok
   11.97 +      | [] => Position.none);
   11.98 +
   11.99 +
  11.100 +    (* output channels *)
  11.101 +
  11.102 +    val writeln_buffer = Unsynchronized.ref Buffer.empty;
  11.103 +    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
  11.104 +    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
  11.105 +
  11.106 +    val warnings = Unsynchronized.ref ([]: string list);
  11.107 +    fun warn msg = Unsynchronized.change warnings (cons msg);
  11.108 +    fun output_warnings () = List.app warning (rev (! warnings));
  11.109 +
  11.110 +    val error_buffer = Unsynchronized.ref Buffer.empty;
  11.111 +    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
  11.112 +    fun flush_error () = writeln (Buffer.content (! error_buffer));
  11.113 +    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
  11.114 +
  11.115 +    fun message {message = msg, hard, location = loc, context = _} =
  11.116 +      let
  11.117 +        val pos = position_of loc;
  11.118 +        val txt =
  11.119 +          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
  11.120 +            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
  11.121 +          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
  11.122 +          Position.reported_text pos Isabelle_Markup.report "";
  11.123 +      in if hard then err txt else warn txt end;
  11.124 +
  11.125 +
  11.126 +    (* results *)
  11.127 +
  11.128 +    val depth = get_print_depth ();
  11.129 +
  11.130 +    fun apply_result {fixes, types, signatures, structures, functors, values} =
  11.131 +      let
  11.132 +        fun display disp x =
  11.133 +          if depth > 0 then
  11.134 +            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
  11.135 +          else ();
  11.136 +
  11.137 +        fun apply_fix (a, b) =
  11.138 +          (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
  11.139 +        fun apply_type (a, b) =
  11.140 +          (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
  11.141 +        fun apply_sig (a, b) =
  11.142 +          (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
  11.143 +        fun apply_struct (a, b) =
  11.144 +          (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
  11.145 +        fun apply_funct (a, b) =
  11.146 +          (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
  11.147 +        fun apply_val (a, b) =
  11.148 +          (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
  11.149 +      in
  11.150 +        List.app apply_fix fixes;
  11.151 +        List.app apply_type types;
  11.152 +        List.app apply_sig signatures;
  11.153 +        List.app apply_struct structures;
  11.154 +        List.app apply_funct functors;
  11.155 +        List.app apply_val values
  11.156 +      end;
  11.157 +
  11.158 +    exception STATIC_ERRORS of unit;
  11.159 +
  11.160 +    fun result_fun (phase1, phase2) () =
  11.161 +     ((case phase1 of
  11.162 +        NONE => ()
  11.163 +      | SOME parse_tree => report_parse_tree depth space parse_tree);
  11.164 +      (case phase2 of
  11.165 +        NONE => raise STATIC_ERRORS ()
  11.166 +      | SOME code =>
  11.167 +          apply_result
  11.168 +            ((code
  11.169 +              |> Runtime.debugging
  11.170 +              |> Runtime.toplevel_error (err o exn_message)) ())));
  11.171 +
  11.172 +
  11.173 +    (* compiler invocation *)
  11.174 +
  11.175 +    val parameters =
  11.176 +     [PolyML.Compiler.CPOutStream write,
  11.177 +      PolyML.Compiler.CPNameSpace space,
  11.178 +      PolyML.Compiler.CPErrorMessageProc message,
  11.179 +      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
  11.180 +      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
  11.181 +      PolyML.Compiler.CPFileName location_props,
  11.182 +      PolyML.Compiler.CPCompilerResultFun result_fun,
  11.183 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
  11.184 +    val _ =
  11.185 +      (while not (List.null (! input_buffer)) do
  11.186 +        PolyML.compiler (get, parameters) ())
  11.187 +      handle exn =>
  11.188 +        if Exn.is_interrupt exn then reraise exn
  11.189 +        else
  11.190 +          let
  11.191 +            val exn_msg =
  11.192 +              (case exn of
  11.193 +                STATIC_ERRORS () => ""
  11.194 +              | Runtime.TOPLEVEL_ERROR => ""
  11.195 +              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
  11.196 +            val _ = output_warnings ();
  11.197 +            val _ = output_writeln ();
  11.198 +          in raise_error exn_msg end;
  11.199 +  in
  11.200 +    if verbose then (output_warnings (); flush_error (); output_writeln ())
  11.201 +    else ()
  11.202 +  end;
  11.203 +
  11.204 +end;
  11.205 +
    12.1 --- a/src/Pure/ROOT.ML	Thu May 24 15:01:17 2012 +0200
    12.2 +++ b/src/Pure/ROOT.ML	Thu May 24 15:33:45 2012 +0200
    12.3 @@ -74,7 +74,7 @@
    12.4  if Multithreading.available then ()
    12.5  else use "Concurrent/single_assignment_sequential.ML";
    12.6  
    12.7 -if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML";
    12.8 +if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
    12.9  
   12.10  if Multithreading.available
   12.11  then use "Concurrent/bash.ML"
   12.12 @@ -191,8 +191,7 @@
   12.13  use "ML/ml_env.ML";
   12.14  use "Isar/runtime.ML";
   12.15  use "ML/ml_compiler.ML";
   12.16 -if ML_System.is_smlnj then ()
   12.17 -else use "ML/ml_compiler_polyml-5.3.ML";
   12.18 +if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
   12.19  use "ML/ml_context.ML";
   12.20  
   12.21  (*theory sources*)
    13.1 --- a/src/Pure/pure_setup.ML	Thu May 24 15:01:17 2012 +0200
    13.2 +++ b/src/Pure/pure_setup.ML	Thu May 24 15:33:45 2012 +0200
    13.3 @@ -36,9 +36,7 @@
    13.4  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
    13.5  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
    13.6  
    13.7 -if ML_System.is_polyml
    13.8 -then use "ML/install_pp_polyml-5.3.ML"
    13.9 -else ();
   13.10 +if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
   13.11  
   13.12  
   13.13  (* ML toplevel use commands *)