merged
authorwenzelm
Thu May 24 15:54:38 2012 +0200 (2012-05-24)
changeset 47986ca7104aebb74
parent 47985 22846a7cf66e
parent 47980 c81801f881b3
child 47987 4e9df6ffcc6e
merged
src/Pure/ML-Systems/compiler_polyml-5.2.ML
src/Pure/ML-Systems/compiler_polyml-5.3.ML
src/Pure/ML-Systems/polyml-5.2.1.ML
src/Pure/ML-Systems/polyml_common.ML
src/Pure/ML-Systems/pp_polyml.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
     1.1 --- a/Admin/CHECKLIST	Thu May 24 15:11:53 2012 +0200
     1.2 +++ b/Admin/CHECKLIST	Thu May 24 15:54:38 2012 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  Checklist for official releases
     1.5  ===============================
     1.6  
     1.7 -- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
     1.8 +- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
     1.9  
    1.10  - test Proof General 4.1, 3.7.1.1;
    1.11  
     2.1 --- a/Admin/isatest/settings/at-poly	Thu May 24 15:11:53 2012 +0200
     2.2 +++ b/Admin/isatest/settings/at-poly	Thu May 24 15:54:38 2012 +0200
     2.3 @@ -1,7 +1,7 @@
     2.4  # -*- shell-script -*- :mode=shellscript:
     2.5  
     2.6 -  POLYML_HOME="/home/polyml/polyml-5.2.1"
     2.7 -  ML_SYSTEM="polyml-5.2.1"
     2.8 +  POLYML_HOME="/home/polyml/polyml-5.3.0"
     2.9 +  ML_SYSTEM="polyml-5.3.0"
    2.10    ML_PLATFORM="x86-linux"
    2.11    ML_HOME="$POLYML_HOME/$ML_PLATFORM"
    2.12    ML_OPTIONS="-H 500"
     3.1 --- a/NEWS	Thu May 24 15:11:53 2012 +0200
     3.2 +++ b/NEWS	Thu May 24 15:54:38 2012 +0200
     3.3 @@ -10,6 +10,13 @@
     3.4  is called fastforce / fast_force_tac already since Isabelle2011-1.
     3.5  
     3.6  
     3.7 +*** System ***
     3.8 +
     3.9 +* Discontinued support for Poly/ML 5.2.1, which was the last version
    3.10 +without exception positions and advanced ML compiler/toplevel
    3.11 +configuration.
    3.12 +
    3.13 +
    3.14  
    3.15  New in Isabelle2012 (May 2012)
    3.16  ------------------------------
     4.1 --- a/doc-src/System/Thy/Presentation.thy	Thu May 24 15:11:53 2012 +0200
     4.2 +++ b/doc-src/System/Thy/Presentation.thy	Thu May 24 15:54:38 2012 +0200
     4.3 @@ -465,12 +465,12 @@
     4.4    Build object-logic or run examples. Also creates browsing
     4.5    information (HTML etc.) according to settings.
     4.6  
     4.7 -  ISABELLE_USEDIR_OPTIONS=
     4.8 +  ISABELLE_USEDIR_OPTIONS=...
     4.9  
    4.10 -  ML_PLATFORM=x86-linux
    4.11 -  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
    4.12 -  ML_SYSTEM=polyml-5.2.1
    4.13 -  ML_OPTIONS=-H 500
    4.14 +  ML_PLATFORM=...
    4.15 +  ML_HOME=...
    4.16 +  ML_SYSTEM=...
    4.17 +  ML_OPTIONS=...
    4.18  \end{ttbox}
    4.19  
    4.20    Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
     5.1 --- a/doc-src/System/Thy/document/Presentation.tex	Thu May 24 15:11:53 2012 +0200
     5.2 +++ b/doc-src/System/Thy/document/Presentation.tex	Thu May 24 15:54:38 2012 +0200
     5.3 @@ -491,12 +491,12 @@
     5.4    Build object-logic or run examples. Also creates browsing
     5.5    information (HTML etc.) according to settings.
     5.6  
     5.7 -  ISABELLE_USEDIR_OPTIONS=
     5.8 +  ISABELLE_USEDIR_OPTIONS=...
     5.9  
    5.10 -  ML_PLATFORM=x86-linux
    5.11 -  ML_HOME=/usr/local/polyml-5.2.1/x86-linux
    5.12 -  ML_SYSTEM=polyml-5.2.1
    5.13 -  ML_OPTIONS=-H 500
    5.14 +  ML_PLATFORM=...
    5.15 +  ML_HOME=...
    5.16 +  ML_SYSTEM=...
    5.17 +  ML_OPTIONS=...
    5.18  \end{ttbox}
    5.19  
    5.20    Note that the value of the \indexref{}{setting}{ISABELLE\_USEDIR\_OPTIONS}\hyperlink{setting.ISABELLE-USEDIR-OPTIONS}{\mbox{\isa{\isatt{ISABELLE{\isaliteral{5F}{\isacharunderscore}}USEDIR{\isaliteral{5F}{\isacharunderscore}}OPTIONS}}}}
     6.1 --- a/src/Pure/General/linear_set.ML	Thu May 24 15:11:53 2012 +0200
     6.2 +++ b/src/Pure/General/linear_set.ML	Thu May 24 15:54:38 2012 +0200
     6.3 @@ -133,7 +133,7 @@
     6.4            in (start, entries') end)));
     6.5  
     6.6  
     6.7 -(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
     6.8 +(* ML pretty-printing *)
     6.9  
    6.10  val _ =
    6.11    PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
     7.1 --- a/src/Pure/General/table.ML	Thu May 24 15:11:53 2012 +0200
     7.2 +++ b/src/Pure/General/table.ML	Thu May 24 15:54:38 2012 +0200
     7.3 @@ -394,7 +394,7 @@
     7.4  fun merge_list eq = join (fn _ => Library.merge eq);
     7.5  
     7.6  
     7.7 -(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
     7.8 +(* ML pretty-printing *)
     7.9  
    7.10  val _ =
    7.11    PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
     8.1 --- a/src/Pure/IsaMakefile	Thu May 24 15:11:53 2012 +0200
     8.2 +++ b/src/Pure/IsaMakefile	Thu May 24 15:54:38 2012 +0200
     8.3 @@ -23,19 +23,15 @@
     8.4  
     8.5  BOOTSTRAP_FILES = 					\
     8.6    General/exn.ML					\
     8.7 -  ML-Systems/compiler_polyml-5.2.ML			\
     8.8 -  ML-Systems/compiler_polyml-5.3.ML			\
     8.9 +  ML-Systems/compiler_polyml.ML			\
    8.10    ML-Systems/ml_name_space.ML				\
    8.11    ML-Systems/ml_pretty.ML				\
    8.12    ML-Systems/ml_system.ML				\
    8.13    ML-Systems/multithreading.ML				\
    8.14    ML-Systems/multithreading_polyml.ML			\
    8.15    ML-Systems/overloading_smlnj.ML			\
    8.16 -  ML-Systems/polyml-5.2.1.ML				\
    8.17    ML-Systems/polyml.ML					\
    8.18 -  ML-Systems/polyml_common.ML				\
    8.19    ML-Systems/pp_dummy.ML				\
    8.20 -  ML-Systems/pp_polyml.ML				\
    8.21    ML-Systems/proper_int.ML				\
    8.22    ML-Systems/single_assignment.ML			\
    8.23    ML-Systems/single_assignment_polyml.ML		\
    8.24 @@ -144,11 +140,10 @@
    8.25    Isar/token.ML						\
    8.26    Isar/toplevel.ML					\
    8.27    Isar/typedecl.ML					\
    8.28 -  ML/install_pp_polyml-5.3.ML				\
    8.29    ML/install_pp_polyml.ML				\
    8.30    ML/ml_antiquote.ML					\
    8.31    ML/ml_compiler.ML					\
    8.32 -  ML/ml_compiler_polyml-5.3.ML				\
    8.33 +  ML/ml_compiler_polyml.ML				\
    8.34    ML/ml_context.ML					\
    8.35    ML/ml_env.ML						\
    8.36    ML/ml_lex.ML						\
     9.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Thu May 24 15:11:53 2012 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,53 +0,0 @@
     9.4 -(*  Title:      Pure/ML-Systems/compiler_polyml-5.2.ML
     9.5 -
     9.6 -Runtime compilation for Poly/ML 5.2.x.
     9.7 -*)
     9.8 -
     9.9 -local
    9.10 -
    9.11 -fun drop_newline s =
    9.12 -  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
    9.13 -  else s;
    9.14 -
    9.15 -in
    9.16 -
    9.17 -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
    9.18 -    (start_line, name) verbose txt =
    9.19 -  let
    9.20 -    val current_line = Unsynchronized.ref start_line;
    9.21 -    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
    9.22 -    val out_buffer = Unsynchronized.ref ([]: string list);
    9.23 -    fun output () = drop_newline (implode (rev (! out_buffer)));
    9.24 -
    9.25 -    fun get () =
    9.26 -      (case ! in_buffer of
    9.27 -        [] => NONE
    9.28 -      | c :: cs =>
    9.29 -          (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
    9.30 -    fun put s = out_buffer := s :: ! out_buffer;
    9.31 -    fun message (msg, is_err, line) =
    9.32 -      (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
    9.33 -
    9.34 -    val parameters =
    9.35 -     [PolyML.Compiler.CPOutStream put,
    9.36 -      PolyML.Compiler.CPLineNo (fn () => ! current_line),
    9.37 -      PolyML.Compiler.CPErrorMessageProc (put o message),
    9.38 -      PolyML.Compiler.CPNameSpace name_space];
    9.39 -    val _ =
    9.40 -      (while not (List.null (! in_buffer)) do
    9.41 -        PolyML.compiler (get, parameters) ())
    9.42 -      handle exn =>
    9.43 -        if Exn.is_interrupt exn then reraise exn
    9.44 -        else
    9.45 -         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
    9.46 -          error (output ()); reraise exn);
    9.47 -  in if verbose then print (output ()) else () end;
    9.48 -
    9.49 -fun use_file context verbose name =
    9.50 -  let
    9.51 -    val instream = TextIO.openIn name;
    9.52 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
    9.53 -  in use_text context (1, name) verbose txt end;
    9.54 -
    9.55 -end;
    9.56 -
    10.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Thu May 24 15:11:53 2012 +0200
    10.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.3 @@ -1,57 +0,0 @@
    10.4 -(*  Title:      Pure/ML-Systems/compiler_polyml-5.3.ML
    10.5 -
    10.6 -Runtime compilation for Poly/ML 5.3.0 and 5.4.0.
    10.7 -*)
    10.8 -
    10.9 -local
   10.10 -
   10.11 -fun drop_newline s =
   10.12 -  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
   10.13 -  else s;
   10.14 -
   10.15 -in
   10.16 -
   10.17 -fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
   10.18 -    (start_line, name) verbose txt =
   10.19 -  let
   10.20 -    val line = Unsynchronized.ref start_line;
   10.21 -    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
   10.22 -    val out_buffer = Unsynchronized.ref ([]: string list);
   10.23 -    fun output () = drop_newline (implode (rev (! out_buffer)));
   10.24 -
   10.25 -    fun get () =
   10.26 -      (case ! in_buffer of
   10.27 -        [] => NONE
   10.28 -      | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
   10.29 -    fun put s = out_buffer := s :: ! out_buffer;
   10.30 -    fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
   10.31 -     (put (if hard then "Error: " else "Warning: ");
   10.32 -      PolyML.prettyPrint (put, 76) msg1;
   10.33 -      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
   10.34 -      put ("At" ^ str_of_pos line name ^ "\n"));
   10.35 -
   10.36 -    val parameters =
   10.37 -     [PolyML.Compiler.CPOutStream put,
   10.38 -      PolyML.Compiler.CPNameSpace name_space,
   10.39 -      PolyML.Compiler.CPErrorMessageProc put_message,
   10.40 -      PolyML.Compiler.CPLineNo (fn () => ! line),
   10.41 -      PolyML.Compiler.CPFileName name,
   10.42 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
   10.43 -    val _ =
   10.44 -      (while not (List.null (! in_buffer)) do
   10.45 -        PolyML.compiler (get, parameters) ())
   10.46 -      handle exn =>
   10.47 -        if Exn.is_interrupt exn then reraise exn
   10.48 -        else
   10.49 -         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   10.50 -          error (output ()); reraise exn);
   10.51 -  in if verbose then print (output ()) else () end;
   10.52 -
   10.53 -fun use_file context verbose name =
   10.54 -  let
   10.55 -    val instream = TextIO.openIn name;
   10.56 -    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   10.57 -  in use_text context (1, name) verbose txt end;
   10.58 -
   10.59 -end;
   10.60 -
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/src/Pure/ML-Systems/compiler_polyml.ML	Thu May 24 15:54:38 2012 +0200
    11.3 @@ -0,0 +1,59 @@
    11.4 +(*  Title:      Pure/ML-Systems/compiler_polyml.ML
    11.5 +
    11.6 +Runtime compilation for Poly/ML 5.3.0 or later.
    11.7 +
    11.8 +See also Pure/ML/ml_compiler_polyml.ML for advanced version.
    11.9 +*)
   11.10 +
   11.11 +local
   11.12 +
   11.13 +fun drop_newline s =
   11.14 +  if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
   11.15 +  else s;
   11.16 +
   11.17 +in
   11.18 +
   11.19 +fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
   11.20 +    (start_line, name) verbose txt =
   11.21 +  let
   11.22 +    val line = Unsynchronized.ref start_line;
   11.23 +    val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
   11.24 +    val out_buffer = Unsynchronized.ref ([]: string list);
   11.25 +    fun output () = drop_newline (implode (rev (! out_buffer)));
   11.26 +
   11.27 +    fun get () =
   11.28 +      (case ! in_buffer of
   11.29 +        [] => NONE
   11.30 +      | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
   11.31 +    fun put s = out_buffer := s :: ! out_buffer;
   11.32 +    fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
   11.33 +     (put (if hard then "Error: " else "Warning: ");
   11.34 +      PolyML.prettyPrint (put, 76) msg1;
   11.35 +      (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
   11.36 +      put ("At" ^ str_of_pos line name ^ "\n"));
   11.37 +
   11.38 +    val parameters =
   11.39 +     [PolyML.Compiler.CPOutStream put,
   11.40 +      PolyML.Compiler.CPNameSpace name_space,
   11.41 +      PolyML.Compiler.CPErrorMessageProc put_message,
   11.42 +      PolyML.Compiler.CPLineNo (fn () => ! line),
   11.43 +      PolyML.Compiler.CPFileName name,
   11.44 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
   11.45 +    val _ =
   11.46 +      (while not (List.null (! in_buffer)) do
   11.47 +        PolyML.compiler (get, parameters) ())
   11.48 +      handle exn =>
   11.49 +        if Exn.is_interrupt exn then reraise exn
   11.50 +        else
   11.51 +         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
   11.52 +          error (output ()); reraise exn);
   11.53 +  in if verbose then print (output ()) else () end;
   11.54 +
   11.55 +fun use_file context verbose name =
   11.56 +  let
   11.57 +    val instream = TextIO.openIn name;
   11.58 +    val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
   11.59 +  in use_text context (1, name) verbose txt end;
   11.60 +
   11.61 +end;
   11.62 +
    12.1 --- a/src/Pure/ML-Systems/multithreading_polyml.ML	Thu May 24 15:11:53 2012 +0200
    12.2 +++ b/src/Pure/ML-Systems/multithreading_polyml.ML	Thu May 24 15:54:38 2012 +0200
    12.3 @@ -1,7 +1,7 @@
    12.4  (*  Title:      Pure/ML-Systems/multithreading_polyml.ML
    12.5      Author:     Makarius
    12.6  
    12.7 -Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml).
    12.8 +Multithreading in Poly/ML 5.3.0 or later (cf. polyml/basis/Thread.sml).
    12.9  *)
   12.10  
   12.11  signature MULTITHREADING_POLYML =
    13.1 --- a/src/Pure/ML-Systems/polyml-5.2.1.ML	Thu May 24 15:11:53 2012 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,35 +0,0 @@
    13.4 -(*  Title:      Pure/ML-Systems/polyml-5.2.1.ML
    13.5 -
    13.6 -Compatibility wrapper for Poly/ML 5.2.1.
    13.7 -*)
    13.8 -
    13.9 -open Thread;
   13.10 -
   13.11 -structure ML_Name_Space =
   13.12 -struct
   13.13 -  open PolyML.NameSpace;
   13.14 -  type T = PolyML.NameSpace.nameSpace;
   13.15 -  val global = PolyML.globalNameSpace;
   13.16 -end;
   13.17 -
   13.18 -fun reraise exn = raise exn;
   13.19 -fun set_exn_serial (_: int) (exn: exn) = exn;
   13.20 -fun get_exn_serial (exn: exn) : int option = NONE;
   13.21 -
   13.22 -use "ML-Systems/polyml_common.ML";
   13.23 -use "ML-Systems/multithreading_polyml.ML";
   13.24 -use "ML-Systems/unsynchronized.ML";
   13.25 -
   13.26 -val _ = PolyML.Compiler.forgetValue "ref";
   13.27 -val _ = PolyML.Compiler.forgetType "ref";
   13.28 -
   13.29 -val pointer_eq = PolyML.pointerEq;
   13.30 -
   13.31 -fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
   13.32 -
   13.33 -use "ML-Systems/compiler_polyml-5.2.ML";
   13.34 -use "ML-Systems/pp_polyml.ML";
   13.35 -use "ML-Systems/pp_dummy.ML";
   13.36 -
   13.37 -use "ML-Systems/ml_system.ML";
   13.38 -
    14.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu May 24 15:11:53 2012 +0200
    14.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu May 24 15:54:38 2012 +0200
    14.3 @@ -1,16 +1,10 @@
    14.4  (*  Title:      Pure/ML-Systems/polyml.ML
    14.5 +    Author:     Makarius
    14.6  
    14.7 -Compatibility wrapper for Poly/ML 5.3 and 5.4.
    14.8 +Compatibility wrapper for Poly/ML 5.3.0 or later.
    14.9  *)
   14.10  
   14.11 -open Thread;
   14.12 -
   14.13 -structure ML_Name_Space =
   14.14 -struct
   14.15 -  open PolyML.NameSpace;
   14.16 -  type T = PolyML.NameSpace.nameSpace;
   14.17 -  val global = PolyML.globalNameSpace;
   14.18 -end;
   14.19 +(* exceptions *)
   14.20  
   14.21  fun reraise exn =
   14.22    (case PolyML.exceptionLocation exn of
   14.23 @@ -33,22 +27,104 @@
   14.24      NONE => NONE
   14.25    | SOME i => if i >= 0 then NONE else SOME (~ i));
   14.26  
   14.27 -use "ML-Systems/polyml_common.ML";
   14.28 +exception Interrupt = SML90.Interrupt;
   14.29 +
   14.30 +use "General/exn.ML";
   14.31 +
   14.32 +
   14.33 +(* multithreading *)
   14.34 +
   14.35 +val seconds = Time.fromReal;
   14.36 +
   14.37 +if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
   14.38 +then ()
   14.39 +else use "ML-Systems/single_assignment_polyml.ML";
   14.40 +
   14.41 +open Thread;
   14.42 +use "ML-Systems/multithreading.ML";
   14.43  use "ML-Systems/multithreading_polyml.ML";
   14.44 +
   14.45  use "ML-Systems/unsynchronized.ML";
   14.46 -
   14.47  val _ = PolyML.Compiler.forgetValue "ref";
   14.48  val _ = PolyML.Compiler.forgetType "ref";
   14.49  
   14.50 +
   14.51 +(* pervasive environment *)
   14.52 +
   14.53 +fun op before (a, _: unit) = a;
   14.54 +
   14.55 +val _ = PolyML.Compiler.forgetValue "isSome";
   14.56 +val _ = PolyML.Compiler.forgetValue "getOpt";
   14.57 +val _ = PolyML.Compiler.forgetValue "valOf";
   14.58 +val _ = PolyML.Compiler.forgetValue "foldl";
   14.59 +val _ = PolyML.Compiler.forgetValue "foldr";
   14.60 +val _ = PolyML.Compiler.forgetValue "print";
   14.61 +val _ = PolyML.Compiler.forgetValue "explode";
   14.62 +val _ = PolyML.Compiler.forgetValue "concat";
   14.63 +
   14.64 +val ord = SML90.ord;
   14.65 +val chr = SML90.chr;
   14.66 +val raw_explode = SML90.explode;
   14.67 +val implode = SML90.implode;
   14.68 +
   14.69 +fun quit () = exit 0;
   14.70 +
   14.71 +
   14.72 +(* ML system identification *)
   14.73 +
   14.74 +use "ML-Systems/ml_system.ML";
   14.75 +
   14.76 +
   14.77 +(* ML runtime system *)
   14.78 +
   14.79 +val exception_trace = PolyML.exception_trace;
   14.80 +val timing = PolyML.timing;
   14.81 +val profiling = PolyML.profiling;
   14.82 +
   14.83 +fun profile 0 f x = f x
   14.84 +  | profile n f x =
   14.85 +      let
   14.86 +        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   14.87 +        val res = Exn.capture f x;
   14.88 +        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   14.89 +      in Exn.release res end;
   14.90 +
   14.91  val pointer_eq = PolyML.pointerEq;
   14.92  
   14.93  fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
   14.94  
   14.95 -use "ML-Systems/compiler_polyml-5.3.ML";
   14.96 +
   14.97 +(* ML compiler *)
   14.98 +
   14.99 +structure ML_Name_Space =
  14.100 +struct
  14.101 +  open PolyML.NameSpace;
  14.102 +  type T = PolyML.NameSpace.nameSpace;
  14.103 +  val global = PolyML.globalNameSpace;
  14.104 +end;
  14.105 +
  14.106 +use "ML-Systems/use_context.ML";
  14.107 +use "ML-Systems/compiler_polyml.ML";
  14.108 +
  14.109  PolyML.Compiler.reportUnreferencedIds := true;
  14.110 +PolyML.Compiler.printInAlphabeticalOrder := false;
  14.111 +PolyML.Compiler.maxInlineSize := 80;
  14.112 +
  14.113 +fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
  14.114  
  14.115  
  14.116 -(* toplevel pretty printing *)
  14.117 +(* ML toplevel pretty printing *)
  14.118 +
  14.119 +use "ML-Systems/ml_pretty.ML";
  14.120 +
  14.121 +local
  14.122 +  val depth = Unsynchronized.ref 10;
  14.123 +in
  14.124 +  fun get_print_depth () = ! depth;
  14.125 +  fun print_depth n = (depth := n; PolyML.print_depth n);
  14.126 +end;
  14.127 +
  14.128 +val error_depth = PolyML.error_depth;
  14.129  
  14.130  val pretty_ml =
  14.131    let
  14.132 @@ -87,5 +163,3 @@
  14.133  val ml_make_string =
  14.134    "(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
  14.135  
  14.136 -use "ML-Systems/ml_system.ML";
  14.137 -
    15.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Thu May 24 15:11:53 2012 +0200
    15.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.3 @@ -1,88 +0,0 @@
    15.4 -(*  Title:      Pure/ML-Systems/polyml_common.ML
    15.5 -
    15.6 -Compatibility file for Poly/ML -- common part for 5.x.
    15.7 -*)
    15.8 -
    15.9 -fun op before (a, _: unit) = a;
   15.10 -
   15.11 -exception Interrupt = SML90.Interrupt;
   15.12 -
   15.13 -use "General/exn.ML";
   15.14 -
   15.15 -if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
   15.16 -then ()
   15.17 -else use "ML-Systems/single_assignment_polyml.ML";
   15.18 -
   15.19 -use "ML-Systems/multithreading.ML";
   15.20 -use "ML-Systems/ml_pretty.ML";
   15.21 -use "ML-Systems/use_context.ML";
   15.22 -
   15.23 -val seconds = Time.fromReal;
   15.24 -
   15.25 -
   15.26 -
   15.27 -(** ML system and platform related **)
   15.28 -
   15.29 -val _ = PolyML.Compiler.forgetValue "isSome";
   15.30 -val _ = PolyML.Compiler.forgetValue "getOpt";
   15.31 -val _ = PolyML.Compiler.forgetValue "valOf";
   15.32 -val _ = PolyML.Compiler.forgetValue "foldl";
   15.33 -val _ = PolyML.Compiler.forgetValue "foldr";
   15.34 -val _ = PolyML.Compiler.forgetValue "print";
   15.35 -val _ = PolyML.Compiler.forgetValue "explode";
   15.36 -val _ = PolyML.Compiler.forgetValue "concat";
   15.37 -
   15.38 -
   15.39 -(* Compiler options *)
   15.40 -
   15.41 -PolyML.Compiler.printInAlphabeticalOrder := false;
   15.42 -PolyML.Compiler.maxInlineSize := 80;
   15.43 -
   15.44 -
   15.45 -(* old Poly/ML emulation *)
   15.46 -
   15.47 -fun quit () = exit 0;
   15.48 -
   15.49 -
   15.50 -(* restore old-style character / string functions *)
   15.51 -
   15.52 -val ord = SML90.ord;
   15.53 -val chr = SML90.chr;
   15.54 -val raw_explode = SML90.explode;
   15.55 -val implode = SML90.implode;
   15.56 -
   15.57 -
   15.58 -(* prompts *)
   15.59 -
   15.60 -fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
   15.61 -
   15.62 -
   15.63 -(* toplevel printing *)
   15.64 -
   15.65 -local
   15.66 -  val depth = ref 10;
   15.67 -in
   15.68 -  fun get_print_depth () = ! depth;
   15.69 -  fun print_depth n = (depth := n; PolyML.print_depth n);
   15.70 -end;
   15.71 -
   15.72 -val error_depth = PolyML.error_depth;
   15.73 -
   15.74 -val ml_make_string = "PolyML.makestring";
   15.75 -
   15.76 -
   15.77 -
   15.78 -(** Runtime system **)
   15.79 -
   15.80 -val exception_trace = PolyML.exception_trace;
   15.81 -val timing = PolyML.timing;
   15.82 -val profiling = PolyML.profiling;
   15.83 -
   15.84 -fun profile 0 f x = f x
   15.85 -  | profile n f x =
   15.86 -      let
   15.87 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
   15.88 -        val res = Exn.capture f x;
   15.89 -        val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
   15.90 -      in Exn.release res end;
   15.91 -
    16.1 --- a/src/Pure/ML-Systems/pp_polyml.ML	Thu May 24 15:11:53 2012 +0200
    16.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.3 @@ -1,20 +0,0 @@
    16.4 -(*  Title:      Pure/ML-Systems/pp_polyml.ML
    16.5 -
    16.6 -Toplevel pretty printing for Poly/ML before 5.3.
    16.7 -*)
    16.8 -
    16.9 -fun ml_pprint (print, begin_blk, brk, end_blk) =
   16.10 -  let
   16.11 -    fun str "" = ()
   16.12 -      | str s = print s;
   16.13 -    fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
   16.14 -          (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
   16.15 -      | pprint (ML_Pretty.String (s, _)) = str s
   16.16 -      | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
   16.17 -      | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
   16.18 -  in pprint end;
   16.19 -
   16.20 -fun toplevel_pp context (_: string list) pp =
   16.21 -  use_text context (1, "pp") false
   16.22 -    ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
   16.23 -
    17.1 --- a/src/Pure/ML/install_pp_polyml-5.3.ML	Thu May 24 15:11:53 2012 +0200
    17.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.3 @@ -1,53 +0,0 @@
    17.4 -(*  Title:      Pure/ML/install_pp_polyml-5.3.ML
    17.5 -    Author:     Makarius
    17.6 -
    17.7 -Extra toplevel pretty-printing for Poly/ML 5.3.0.
    17.8 -*)
    17.9 -
   17.10 -PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
   17.11 -  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
   17.12 -
   17.13 -PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
   17.14 -  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
   17.15 -
   17.16 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
   17.17 -  pretty (Synchronized.value var, depth));
   17.18 -
   17.19 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   17.20 -  (case Future.peek x of
   17.21 -    NONE => PolyML.PrettyString "<future>"
   17.22 -  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   17.23 -  | SOME (Exn.Res y) => pretty (y, depth)));
   17.24 -
   17.25 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   17.26 -  (case Lazy.peek x of
   17.27 -    NONE => PolyML.PrettyString "<lazy>"
   17.28 -  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   17.29 -  | SOME (Exn.Res y) => pretty (y, depth)));
   17.30 -
   17.31 -PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
   17.32 -  let
   17.33 -    open PolyML;
   17.34 -    val from_ML = Pretty.from_ML o pretty_ml;
   17.35 -    fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
   17.36 -    fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
   17.37 -    fun prt_term parens dp (t as _ $ _) =
   17.38 -          op :: (strip_comb t)
   17.39 -          |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
   17.40 -          |> Pretty.separate " $"
   17.41 -          |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
   17.42 -      | prt_term _ dp (Abs (x, T, body)) =
   17.43 -          prt_apps "Abs"
   17.44 -           [from_ML (prettyRepresentation (x, dp - 1)),
   17.45 -            from_ML (prettyRepresentation (T, dp - 2)),
   17.46 -            prt_term false (dp - 3) body]
   17.47 -      | prt_term _ dp (Const const) =
   17.48 -          prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
   17.49 -      | prt_term _ dp (Free free) =
   17.50 -          prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
   17.51 -      | prt_term _ dp (Var var) =
   17.52 -          prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
   17.53 -      | prt_term _ dp (Bound i) =
   17.54 -          prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
   17.55 -  in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
   17.56 -
    18.1 --- a/src/Pure/ML/install_pp_polyml.ML	Thu May 24 15:11:53 2012 +0200
    18.2 +++ b/src/Pure/ML/install_pp_polyml.ML	Thu May 24 15:54:38 2012 +0200
    18.3 @@ -1,20 +1,53 @@
    18.4  (*  Title:      Pure/ML/install_pp_polyml.ML
    18.5      Author:     Makarius
    18.6  
    18.7 -Extra toplevel pretty-printing for Poly/ML.
    18.8 +Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
    18.9  *)
   18.10  
   18.11 -PolyML.install_pp
   18.12 -  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
   18.13 -    (case Future.peek x of
   18.14 -      NONE => str "<future>"
   18.15 -    | SOME (Exn.Exn _) => str "<failed>"
   18.16 -    | SOME (Exn.Res y) => print (y, depth)));
   18.17 +PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
   18.18 +  ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
   18.19 +
   18.20 +PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
   18.21 +  ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
   18.22 +
   18.23 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
   18.24 +  pretty (Synchronized.value var, depth));
   18.25 +
   18.26 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   18.27 +  (case Future.peek x of
   18.28 +    NONE => PolyML.PrettyString "<future>"
   18.29 +  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   18.30 +  | SOME (Exn.Res y) => pretty (y, depth)));
   18.31 +
   18.32 +PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
   18.33 +  (case Lazy.peek x of
   18.34 +    NONE => PolyML.PrettyString "<lazy>"
   18.35 +  | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
   18.36 +  | SOME (Exn.Res y) => pretty (y, depth)));
   18.37  
   18.38 -PolyML.install_pp
   18.39 -  (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
   18.40 -    (case Lazy.peek x of
   18.41 -      NONE => str "<lazy>"
   18.42 -    | SOME (Exn.Exn _) => str "<failed>"
   18.43 -    | SOME (Exn.Res y) => print (y, depth)));
   18.44 +PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
   18.45 +  let
   18.46 +    open PolyML;
   18.47 +    val from_ML = Pretty.from_ML o pretty_ml;
   18.48 +    fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
   18.49 +    fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
   18.50 +    fun prt_term parens dp (t as _ $ _) =
   18.51 +          op :: (strip_comb t)
   18.52 +          |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
   18.53 +          |> Pretty.separate " $"
   18.54 +          |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
   18.55 +      | prt_term _ dp (Abs (x, T, body)) =
   18.56 +          prt_apps "Abs"
   18.57 +           [from_ML (prettyRepresentation (x, dp - 1)),
   18.58 +            from_ML (prettyRepresentation (T, dp - 2)),
   18.59 +            prt_term false (dp - 3) body]
   18.60 +      | prt_term _ dp (Const const) =
   18.61 +          prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
   18.62 +      | prt_term _ dp (Free free) =
   18.63 +          prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
   18.64 +      | prt_term _ dp (Var var) =
   18.65 +          prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
   18.66 +      | prt_term _ dp (Bound i) =
   18.67 +          prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
   18.68 +  in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
   18.69  
    19.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu May 24 15:11:53 2012 +0200
    19.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.3 @@ -1,202 +0,0 @@
    19.4 -(*  Title:      Pure/ML/ml_compiler_polyml-5.3.ML
    19.5 -    Author:     Makarius
    19.6 -
    19.7 -Advanced runtime compilation for Poly/ML 5.3.0 or later.
    19.8 -*)
    19.9 -
   19.10 -structure ML_Compiler: ML_COMPILER =
   19.11 -struct
   19.12 -
   19.13 -(* source locations *)
   19.14 -
   19.15 -fun position_of (loc: PolyML.location) =
   19.16 -  let
   19.17 -    val {file = text, startLine = line, startPosition = offset,
   19.18 -      endLine = _, endPosition = end_offset} = loc;
   19.19 -    val props =
   19.20 -      (case YXML.parse text of
   19.21 -        XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
   19.22 -      | XML.Text s => Position.file_name s);
   19.23 -  in
   19.24 -    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   19.25 -  end;
   19.26 -
   19.27 -fun exn_position exn =
   19.28 -  (case PolyML.exceptionLocation exn of
   19.29 -    NONE => Position.none
   19.30 -  | SOME loc => position_of loc);
   19.31 -
   19.32 -val exn_messages = Runtime.exn_messages exn_position;
   19.33 -val exn_message = Runtime.exn_message exn_position;
   19.34 -
   19.35 -
   19.36 -(* parse trees *)
   19.37 -
   19.38 -fun report_parse_tree depth space =
   19.39 -  let
   19.40 -    val reported_text =
   19.41 -      (case Context.thread_data () of
   19.42 -        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
   19.43 -      | _ => Position.reported_text);
   19.44 -
   19.45 -    fun reported_entity kind loc decl =
   19.46 -      reported_text (position_of loc)
   19.47 -        (Isabelle_Markup.entityN,
   19.48 -          (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   19.49 -
   19.50 -    fun reported loc (PolyML.PTtype types) =
   19.51 -          cons
   19.52 -            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
   19.53 -              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   19.54 -              |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
   19.55 -      | reported loc (PolyML.PTdeclaredAt decl) =
   19.56 -          cons (reported_entity Isabelle_Markup.ML_defN loc decl)
   19.57 -      | reported loc (PolyML.PTopenedAt decl) =
   19.58 -          cons (reported_entity Isabelle_Markup.ML_openN loc decl)
   19.59 -      | reported loc (PolyML.PTstructureAt decl) =
   19.60 -          cons (reported_entity Isabelle_Markup.ML_structN loc decl)
   19.61 -      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
   19.62 -      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
   19.63 -      | reported _ _ = I
   19.64 -    and reported_tree (loc, props) = fold (reported loc) props;
   19.65 -  in fn tree => Output.report (implode (reported_tree tree [])) end;
   19.66 -
   19.67 -
   19.68 -(* eval ML source tokens *)
   19.69 -
   19.70 -fun eval verbose pos toks =
   19.71 -  let
   19.72 -    val _ = Secure.secure_mltext ();
   19.73 -    val space = ML_Env.name_space;
   19.74 -
   19.75 -
   19.76 -    (* input *)
   19.77 -
   19.78 -    val location_props =
   19.79 -      op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
   19.80 -            (filter (member (op =)
   19.81 -              [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
   19.82 -
   19.83 -    val input_buffer =
   19.84 -      Unsynchronized.ref (toks |> map
   19.85 -        (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
   19.86 -
   19.87 -    fun get () =
   19.88 -      (case ! input_buffer of
   19.89 -        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
   19.90 -      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
   19.91 -      | [] => NONE);
   19.92 -
   19.93 -    fun get_pos () =
   19.94 -      (case ! input_buffer of
   19.95 -        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
   19.96 -      | ([], tok) :: _ => ML_Lex.end_pos_of tok
   19.97 -      | [] => Position.none);
   19.98 -
   19.99 -
  19.100 -    (* output channels *)
  19.101 -
  19.102 -    val writeln_buffer = Unsynchronized.ref Buffer.empty;
  19.103 -    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
  19.104 -    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
  19.105 -
  19.106 -    val warnings = Unsynchronized.ref ([]: string list);
  19.107 -    fun warn msg = Unsynchronized.change warnings (cons msg);
  19.108 -    fun output_warnings () = List.app warning (rev (! warnings));
  19.109 -
  19.110 -    val error_buffer = Unsynchronized.ref Buffer.empty;
  19.111 -    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
  19.112 -    fun flush_error () = writeln (Buffer.content (! error_buffer));
  19.113 -    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
  19.114 -
  19.115 -    fun message {message = msg, hard, location = loc, context = _} =
  19.116 -      let
  19.117 -        val pos = position_of loc;
  19.118 -        val txt =
  19.119 -          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
  19.120 -            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
  19.121 -          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
  19.122 -          Position.reported_text pos Isabelle_Markup.report "";
  19.123 -      in if hard then err txt else warn txt end;
  19.124 -
  19.125 -
  19.126 -    (* results *)
  19.127 -
  19.128 -    val depth = get_print_depth ();
  19.129 -
  19.130 -    fun apply_result {fixes, types, signatures, structures, functors, values} =
  19.131 -      let
  19.132 -        fun display disp x =
  19.133 -          if depth > 0 then
  19.134 -            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
  19.135 -          else ();
  19.136 -
  19.137 -        fun apply_fix (a, b) =
  19.138 -          (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
  19.139 -        fun apply_type (a, b) =
  19.140 -          (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
  19.141 -        fun apply_sig (a, b) =
  19.142 -          (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
  19.143 -        fun apply_struct (a, b) =
  19.144 -          (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
  19.145 -        fun apply_funct (a, b) =
  19.146 -          (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
  19.147 -        fun apply_val (a, b) =
  19.148 -          (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
  19.149 -      in
  19.150 -        List.app apply_fix fixes;
  19.151 -        List.app apply_type types;
  19.152 -        List.app apply_sig signatures;
  19.153 -        List.app apply_struct structures;
  19.154 -        List.app apply_funct functors;
  19.155 -        List.app apply_val values
  19.156 -      end;
  19.157 -
  19.158 -    exception STATIC_ERRORS of unit;
  19.159 -
  19.160 -    fun result_fun (phase1, phase2) () =
  19.161 -     ((case phase1 of
  19.162 -        NONE => ()
  19.163 -      | SOME parse_tree => report_parse_tree depth space parse_tree);
  19.164 -      (case phase2 of
  19.165 -        NONE => raise STATIC_ERRORS ()
  19.166 -      | SOME code =>
  19.167 -          apply_result
  19.168 -            ((code
  19.169 -              |> Runtime.debugging
  19.170 -              |> Runtime.toplevel_error (err o exn_message)) ())));
  19.171 -
  19.172 -
  19.173 -    (* compiler invocation *)
  19.174 -
  19.175 -    val parameters =
  19.176 -     [PolyML.Compiler.CPOutStream write,
  19.177 -      PolyML.Compiler.CPNameSpace space,
  19.178 -      PolyML.Compiler.CPErrorMessageProc message,
  19.179 -      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
  19.180 -      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
  19.181 -      PolyML.Compiler.CPFileName location_props,
  19.182 -      PolyML.Compiler.CPCompilerResultFun result_fun,
  19.183 -      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
  19.184 -    val _ =
  19.185 -      (while not (List.null (! input_buffer)) do
  19.186 -        PolyML.compiler (get, parameters) ())
  19.187 -      handle exn =>
  19.188 -        if Exn.is_interrupt exn then reraise exn
  19.189 -        else
  19.190 -          let
  19.191 -            val exn_msg =
  19.192 -              (case exn of
  19.193 -                STATIC_ERRORS () => ""
  19.194 -              | Runtime.TOPLEVEL_ERROR => ""
  19.195 -              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
  19.196 -            val _ = output_warnings ();
  19.197 -            val _ = output_writeln ();
  19.198 -          in raise_error exn_msg end;
  19.199 -  in
  19.200 -    if verbose then (output_warnings (); flush_error (); output_writeln ())
  19.201 -    else ()
  19.202 -  end;
  19.203 -
  19.204 -end;
  19.205 -
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Thu May 24 15:54:38 2012 +0200
    20.3 @@ -0,0 +1,202 @@
    20.4 +(*  Title:      Pure/ML/ml_compiler_polyml.ML
    20.5 +    Author:     Makarius
    20.6 +
    20.7 +Advanced runtime compilation for Poly/ML 5.3.0 or later.
    20.8 +*)
    20.9 +
   20.10 +structure ML_Compiler: ML_COMPILER =
   20.11 +struct
   20.12 +
   20.13 +(* source locations *)
   20.14 +
   20.15 +fun position_of (loc: PolyML.location) =
   20.16 +  let
   20.17 +    val {file = text, startLine = line, startPosition = offset,
   20.18 +      endLine = _, endPosition = end_offset} = loc;
   20.19 +    val props =
   20.20 +      (case YXML.parse text of
   20.21 +        XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
   20.22 +      | XML.Text s => Position.file_name s);
   20.23 +  in
   20.24 +    Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
   20.25 +  end;
   20.26 +
   20.27 +fun exn_position exn =
   20.28 +  (case PolyML.exceptionLocation exn of
   20.29 +    NONE => Position.none
   20.30 +  | SOME loc => position_of loc);
   20.31 +
   20.32 +val exn_messages = Runtime.exn_messages exn_position;
   20.33 +val exn_message = Runtime.exn_message exn_position;
   20.34 +
   20.35 +
   20.36 +(* parse trees *)
   20.37 +
   20.38 +fun report_parse_tree depth space =
   20.39 +  let
   20.40 +    val reported_text =
   20.41 +      (case Context.thread_data () of
   20.42 +        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
   20.43 +      | _ => Position.reported_text);
   20.44 +
   20.45 +    fun reported_entity kind loc decl =
   20.46 +      reported_text (position_of loc)
   20.47 +        (Isabelle_Markup.entityN,
   20.48 +          (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
   20.49 +
   20.50 +    fun reported loc (PolyML.PTtype types) =
   20.51 +          cons
   20.52 +            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
   20.53 +              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
   20.54 +              |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
   20.55 +      | reported loc (PolyML.PTdeclaredAt decl) =
   20.56 +          cons (reported_entity Isabelle_Markup.ML_defN loc decl)
   20.57 +      | reported loc (PolyML.PTopenedAt decl) =
   20.58 +          cons (reported_entity Isabelle_Markup.ML_openN loc decl)
   20.59 +      | reported loc (PolyML.PTstructureAt decl) =
   20.60 +          cons (reported_entity Isabelle_Markup.ML_structN loc decl)
   20.61 +      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
   20.62 +      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
   20.63 +      | reported _ _ = I
   20.64 +    and reported_tree (loc, props) = fold (reported loc) props;
   20.65 +  in fn tree => Output.report (implode (reported_tree tree [])) end;
   20.66 +
   20.67 +
   20.68 +(* eval ML source tokens *)
   20.69 +
   20.70 +fun eval verbose pos toks =
   20.71 +  let
   20.72 +    val _ = Secure.secure_mltext ();
   20.73 +    val space = ML_Env.name_space;
   20.74 +
   20.75 +
   20.76 +    (* input *)
   20.77 +
   20.78 +    val location_props =
   20.79 +      op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
   20.80 +            (filter (member (op =)
   20.81 +              [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
   20.82 +
   20.83 +    val input_buffer =
   20.84 +      Unsynchronized.ref (toks |> map
   20.85 +        (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
   20.86 +
   20.87 +    fun get () =
   20.88 +      (case ! input_buffer of
   20.89 +        (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
   20.90 +      | ([], _) :: rest => (input_buffer := rest; SOME #" ")
   20.91 +      | [] => NONE);
   20.92 +
   20.93 +    fun get_pos () =
   20.94 +      (case ! input_buffer of
   20.95 +        (_ :: _, tok) :: _ => ML_Lex.pos_of tok
   20.96 +      | ([], tok) :: _ => ML_Lex.end_pos_of tok
   20.97 +      | [] => Position.none);
   20.98 +
   20.99 +
  20.100 +    (* output channels *)
  20.101 +
  20.102 +    val writeln_buffer = Unsynchronized.ref Buffer.empty;
  20.103 +    fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
  20.104 +    fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
  20.105 +
  20.106 +    val warnings = Unsynchronized.ref ([]: string list);
  20.107 +    fun warn msg = Unsynchronized.change warnings (cons msg);
  20.108 +    fun output_warnings () = List.app warning (rev (! warnings));
  20.109 +
  20.110 +    val error_buffer = Unsynchronized.ref Buffer.empty;
  20.111 +    fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
  20.112 +    fun flush_error () = writeln (Buffer.content (! error_buffer));
  20.113 +    fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
  20.114 +
  20.115 +    fun message {message = msg, hard, location = loc, context = _} =
  20.116 +      let
  20.117 +        val pos = position_of loc;
  20.118 +        val txt =
  20.119 +          (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
  20.120 +            ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
  20.121 +          Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
  20.122 +          Position.reported_text pos Isabelle_Markup.report "";
  20.123 +      in if hard then err txt else warn txt end;
  20.124 +
  20.125 +
  20.126 +    (* results *)
  20.127 +
  20.128 +    val depth = get_print_depth ();
  20.129 +
  20.130 +    fun apply_result {fixes, types, signatures, structures, functors, values} =
  20.131 +      let
  20.132 +        fun display disp x =
  20.133 +          if depth > 0 then
  20.134 +            (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
  20.135 +          else ();
  20.136 +
  20.137 +        fun apply_fix (a, b) =
  20.138 +          (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
  20.139 +        fun apply_type (a, b) =
  20.140 +          (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
  20.141 +        fun apply_sig (a, b) =
  20.142 +          (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
  20.143 +        fun apply_struct (a, b) =
  20.144 +          (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
  20.145 +        fun apply_funct (a, b) =
  20.146 +          (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
  20.147 +        fun apply_val (a, b) =
  20.148 +          (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
  20.149 +      in
  20.150 +        List.app apply_fix fixes;
  20.151 +        List.app apply_type types;
  20.152 +        List.app apply_sig signatures;
  20.153 +        List.app apply_struct structures;
  20.154 +        List.app apply_funct functors;
  20.155 +        List.app apply_val values
  20.156 +      end;
  20.157 +
  20.158 +    exception STATIC_ERRORS of unit;
  20.159 +
  20.160 +    fun result_fun (phase1, phase2) () =
  20.161 +     ((case phase1 of
  20.162 +        NONE => ()
  20.163 +      | SOME parse_tree => report_parse_tree depth space parse_tree);
  20.164 +      (case phase2 of
  20.165 +        NONE => raise STATIC_ERRORS ()
  20.166 +      | SOME code =>
  20.167 +          apply_result
  20.168 +            ((code
  20.169 +              |> Runtime.debugging
  20.170 +              |> Runtime.toplevel_error (err o exn_message)) ())));
  20.171 +
  20.172 +
  20.173 +    (* compiler invocation *)
  20.174 +
  20.175 +    val parameters =
  20.176 +     [PolyML.Compiler.CPOutStream write,
  20.177 +      PolyML.Compiler.CPNameSpace space,
  20.178 +      PolyML.Compiler.CPErrorMessageProc message,
  20.179 +      PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
  20.180 +      PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
  20.181 +      PolyML.Compiler.CPFileName location_props,
  20.182 +      PolyML.Compiler.CPCompilerResultFun result_fun,
  20.183 +      PolyML.Compiler.CPPrintInAlphabeticalOrder false];
  20.184 +    val _ =
  20.185 +      (while not (List.null (! input_buffer)) do
  20.186 +        PolyML.compiler (get, parameters) ())
  20.187 +      handle exn =>
  20.188 +        if Exn.is_interrupt exn then reraise exn
  20.189 +        else
  20.190 +          let
  20.191 +            val exn_msg =
  20.192 +              (case exn of
  20.193 +                STATIC_ERRORS () => ""
  20.194 +              | Runtime.TOPLEVEL_ERROR => ""
  20.195 +              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
  20.196 +            val _ = output_warnings ();
  20.197 +            val _ = output_writeln ();
  20.198 +          in raise_error exn_msg end;
  20.199 +  in
  20.200 +    if verbose then (output_warnings (); flush_error (); output_writeln ())
  20.201 +    else ()
  20.202 +  end;
  20.203 +
  20.204 +end;
  20.205 +
    21.1 --- a/src/Pure/ROOT.ML	Thu May 24 15:11:53 2012 +0200
    21.2 +++ b/src/Pure/ROOT.ML	Thu May 24 15:54:38 2012 +0200
    21.3 @@ -74,7 +74,7 @@
    21.4  if Multithreading.available then ()
    21.5  else use "Concurrent/single_assignment_sequential.ML";
    21.6  
    21.7 -if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML";
    21.8 +if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
    21.9  
   21.10  if Multithreading.available
   21.11  then use "Concurrent/bash.ML"
   21.12 @@ -191,8 +191,7 @@
   21.13  use "ML/ml_env.ML";
   21.14  use "Isar/runtime.ML";
   21.15  use "ML/ml_compiler.ML";
   21.16 -if ML_System.name = "polyml-5.2.1" orelse ML_System.is_smlnj then ()
   21.17 -else use "ML/ml_compiler_polyml-5.3.ML";
   21.18 +if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
   21.19  use "ML/ml_context.ML";
   21.20  
   21.21  (*theory sources*)
    22.1 --- a/src/Pure/pure_setup.ML	Thu May 24 15:11:53 2012 +0200
    22.2 +++ b/src/Pure/pure_setup.ML	Thu May 24 15:54:38 2012 +0200
    22.3 @@ -36,11 +36,7 @@
    22.4  toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
    22.5  toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
    22.6  
    22.7 -if ML_System.name = "polyml-5.2.1"
    22.8 -then use "ML/install_pp_polyml.ML"
    22.9 -else if ML_System.is_polyml
   22.10 -then use "ML/install_pp_polyml-5.3.ML"
   22.11 -else ();
   22.12 +if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
   22.13  
   22.14  
   22.15  (* ML toplevel use commands *)