--- a/Admin/CHECKLIST Thu May 24 15:11:53 2012 +0200
+++ b/Admin/CHECKLIST Thu May 24 15:54:38 2012 +0200
@@ -1,7 +1,7 @@
Checklist for official releases
===============================
-- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, polyml-5.2.1, smlnj;
+- test polyml-5.4.1, polyml-5.4.0, polyml-5.3.0, smlnj;
- test Proof General 4.1, 3.7.1.1;
--- a/Admin/isatest/settings/at-poly Thu May 24 15:11:53 2012 +0200
+++ b/Admin/isatest/settings/at-poly Thu May 24 15:54:38 2012 +0200
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/polyml/polyml-5.2.1"
- ML_SYSTEM="polyml-5.2.1"
+ POLYML_HOME="/home/polyml/polyml-5.3.0"
+ ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86-linux"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 500"
--- a/NEWS Thu May 24 15:11:53 2012 +0200
+++ b/NEWS Thu May 24 15:54:38 2012 +0200
@@ -10,6 +10,13 @@
is called fastforce / fast_force_tac already since Isabelle2011-1.
+*** System ***
+
+* Discontinued support for Poly/ML 5.2.1, which was the last version
+without exception positions and advanced ML compiler/toplevel
+configuration.
+
+
New in Isabelle2012 (May 2012)
------------------------------
--- a/doc-src/System/Thy/Presentation.thy Thu May 24 15:11:53 2012 +0200
+++ b/doc-src/System/Thy/Presentation.thy Thu May 24 15:54:38 2012 +0200
@@ -465,12 +465,12 @@
Build object-logic or run examples. Also creates browsing
information (HTML etc.) according to settings.
- ISABELLE_USEDIR_OPTIONS=
+ ISABELLE_USEDIR_OPTIONS=...
- ML_PLATFORM=x86-linux
- ML_HOME=/usr/local/polyml-5.2.1/x86-linux
- ML_SYSTEM=polyml-5.2.1
- ML_OPTIONS=-H 500
+ ML_PLATFORM=...
+ ML_HOME=...
+ ML_SYSTEM=...
+ ML_OPTIONS=...
\end{ttbox}
Note that the value of the @{setting_ref ISABELLE_USEDIR_OPTIONS}
--- a/doc-src/System/Thy/document/Presentation.tex Thu May 24 15:11:53 2012 +0200
+++ b/doc-src/System/Thy/document/Presentation.tex Thu May 24 15:54:38 2012 +0200
@@ -491,12 +491,12 @@
Build object-logic or run examples. Also creates browsing
information (HTML etc.) according to settings.
- ISABELLE_USEDIR_OPTIONS=
+ ISABELLE_USEDIR_OPTIONS=...
- ML_PLATFORM=x86-linux
- ML_HOME=/usr/local/polyml-5.2.1/x86-linux
- ML_SYSTEM=polyml-5.2.1
- ML_OPTIONS=-H 500
+ ML_PLATFORM=...
+ ML_HOME=...
+ ML_SYSTEM=...
+ ML_OPTIONS=...
\end{ttbox}
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}}}}
--- a/src/Pure/General/linear_set.ML Thu May 24 15:11:53 2012 +0200
+++ b/src/Pure/General/linear_set.ML Thu May 24 15:54:38 2012 +0200
@@ -133,7 +133,7 @@
in (start, entries') end)));
-(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
+(* ML pretty-printing *)
val _ =
PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
--- a/src/Pure/General/table.ML Thu May 24 15:11:53 2012 +0200
+++ b/src/Pure/General/table.ML Thu May 24 15:54:38 2012 +0200
@@ -394,7 +394,7 @@
fun merge_list eq = join (fn _ => Library.merge eq);
-(* ML pretty-printing -- requires Poly/ML 5.3.0 or later *)
+(* ML pretty-printing *)
val _ =
PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
--- a/src/Pure/IsaMakefile Thu May 24 15:11:53 2012 +0200
+++ b/src/Pure/IsaMakefile Thu May 24 15:54:38 2012 +0200
@@ -23,19 +23,15 @@
BOOTSTRAP_FILES = \
General/exn.ML \
- ML-Systems/compiler_polyml-5.2.ML \
- ML-Systems/compiler_polyml-5.3.ML \
+ ML-Systems/compiler_polyml.ML \
ML-Systems/ml_name_space.ML \
ML-Systems/ml_pretty.ML \
ML-Systems/ml_system.ML \
ML-Systems/multithreading.ML \
ML-Systems/multithreading_polyml.ML \
ML-Systems/overloading_smlnj.ML \
- ML-Systems/polyml-5.2.1.ML \
ML-Systems/polyml.ML \
- ML-Systems/polyml_common.ML \
ML-Systems/pp_dummy.ML \
- ML-Systems/pp_polyml.ML \
ML-Systems/proper_int.ML \
ML-Systems/single_assignment.ML \
ML-Systems/single_assignment_polyml.ML \
@@ -144,11 +140,10 @@
Isar/token.ML \
Isar/toplevel.ML \
Isar/typedecl.ML \
- ML/install_pp_polyml-5.3.ML \
ML/install_pp_polyml.ML \
ML/ml_antiquote.ML \
ML/ml_compiler.ML \
- ML/ml_compiler_polyml-5.3.ML \
+ ML/ml_compiler_polyml.ML \
ML/ml_context.ML \
ML/ml_env.ML \
ML/ml_lex.ML \
--- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML Thu May 24 15:11:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: Pure/ML-Systems/compiler_polyml-5.2.ML
-
-Runtime compilation for Poly/ML 5.2.x.
-*)
-
-local
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (start_line, name) verbose txt =
- let
- val current_line = Unsynchronized.ref start_line;
- val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
- val out_buffer = Unsynchronized.ref ([]: string list);
- fun output () = drop_newline (implode (rev (! out_buffer)));
-
- fun get () =
- (case ! in_buffer of
- [] => NONE
- | c :: cs =>
- (in_buffer := cs; if c = #"\n" then current_line := ! current_line + 1 else (); SOME c));
- fun put s = out_buffer := s :: ! out_buffer;
- fun message (msg, is_err, line) =
- (if is_err then "Error: " else "Warning: ") ^ drop_newline msg ^ str_of_pos line name ^ "\n";
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPLineNo (fn () => ! current_line),
- PolyML.Compiler.CPErrorMessageProc (put o message),
- PolyML.Compiler.CPNameSpace name_space];
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- if Exn.is_interrupt exn then reraise exn
- else
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); reraise exn);
- in if verbose then print (output ()) else () end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
-
-end;
-
--- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML Thu May 24 15:11:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,57 +0,0 @@
-(* Title: Pure/ML-Systems/compiler_polyml-5.3.ML
-
-Runtime compilation for Poly/ML 5.3.0 and 5.4.0.
-*)
-
-local
-
-fun drop_newline s =
- if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
- else s;
-
-in
-
-fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
- (start_line, name) verbose txt =
- let
- val line = Unsynchronized.ref start_line;
- val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
- val out_buffer = Unsynchronized.ref ([]: string list);
- fun output () = drop_newline (implode (rev (! out_buffer)));
-
- fun get () =
- (case ! in_buffer of
- [] => NONE
- | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
- fun put s = out_buffer := s :: ! out_buffer;
- fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
- (put (if hard then "Error: " else "Warning: ");
- PolyML.prettyPrint (put, 76) msg1;
- (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
- put ("At" ^ str_of_pos line name ^ "\n"));
-
- val parameters =
- [PolyML.Compiler.CPOutStream put,
- PolyML.Compiler.CPNameSpace name_space,
- PolyML.Compiler.CPErrorMessageProc put_message,
- PolyML.Compiler.CPLineNo (fn () => ! line),
- PolyML.Compiler.CPFileName name,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false];
- val _ =
- (while not (List.null (! in_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- if Exn.is_interrupt exn then reraise exn
- else
- (put ("Exception- " ^ General.exnMessage exn ^ " raised");
- error (output ()); reraise exn);
- in if verbose then print (output ()) else () end;
-
-fun use_file context verbose name =
- let
- val instream = TextIO.openIn name;
- val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
- in use_text context (1, name) verbose txt end;
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/compiler_polyml.ML Thu May 24 15:54:38 2012 +0200
@@ -0,0 +1,59 @@
+(* Title: Pure/ML-Systems/compiler_polyml.ML
+
+Runtime compilation for Poly/ML 5.3.0 or later.
+
+See also Pure/ML/ml_compiler_polyml.ML for advanced version.
+*)
+
+local
+
+fun drop_newline s =
+ if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
+ else s;
+
+in
+
+fun use_text ({tune_source, name_space, str_of_pos, print, error, ...}: use_context)
+ (start_line, name) verbose txt =
+ let
+ val line = Unsynchronized.ref start_line;
+ val in_buffer = Unsynchronized.ref (String.explode (tune_source txt));
+ val out_buffer = Unsynchronized.ref ([]: string list);
+ fun output () = drop_newline (implode (rev (! out_buffer)));
+
+ fun get () =
+ (case ! in_buffer of
+ [] => NONE
+ | c :: cs => (in_buffer := cs; if c = #"\n" then line := ! line + 1 else (); SOME c));
+ fun put s = out_buffer := s :: ! out_buffer;
+ fun put_message {message = msg1, hard, location = {startLine = line, ...}, context} =
+ (put (if hard then "Error: " else "Warning: ");
+ PolyML.prettyPrint (put, 76) msg1;
+ (case context of NONE => () | SOME msg2 => PolyML.prettyPrint (put, 76) msg2);
+ put ("At" ^ str_of_pos line name ^ "\n"));
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream put,
+ PolyML.Compiler.CPNameSpace name_space,
+ PolyML.Compiler.CPErrorMessageProc put_message,
+ PolyML.Compiler.CPLineNo (fn () => ! line),
+ PolyML.Compiler.CPFileName name,
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false];
+ val _ =
+ (while not (List.null (! in_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else
+ (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+ error (output ()); reraise exn);
+ in if verbose then print (output ()) else () end;
+
+fun use_file context verbose name =
+ let
+ val instream = TextIO.openIn name;
+ val txt = Exn.release (Exn.capture TextIO.inputAll instream before TextIO.closeIn instream);
+ in use_text context (1, name) verbose txt end;
+
+end;
+
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Thu May 24 15:11:53 2012 +0200
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Thu May 24 15:54:38 2012 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/ML-Systems/multithreading_polyml.ML
Author: Makarius
-Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml).
+Multithreading in Poly/ML 5.3.0 or later (cf. polyml/basis/Thread.sml).
*)
signature MULTITHREADING_POLYML =
--- a/src/Pure/ML-Systems/polyml-5.2.1.ML Thu May 24 15:11:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,35 +0,0 @@
-(* Title: Pure/ML-Systems/polyml-5.2.1.ML
-
-Compatibility wrapper for Poly/ML 5.2.1.
-*)
-
-open Thread;
-
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
-end;
-
-fun reraise exn = raise exn;
-fun set_exn_serial (_: int) (exn: exn) = exn;
-fun get_exn_serial (exn: exn) : int option = NONE;
-
-use "ML-Systems/polyml_common.ML";
-use "ML-Systems/multithreading_polyml.ML";
-use "ML-Systems/unsynchronized.ML";
-
-val _ = PolyML.Compiler.forgetValue "ref";
-val _ = PolyML.Compiler.forgetType "ref";
-
-val pointer_eq = PolyML.pointerEq;
-
-fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-
-use "ML-Systems/compiler_polyml-5.2.ML";
-use "ML-Systems/pp_polyml.ML";
-use "ML-Systems/pp_dummy.ML";
-
-use "ML-Systems/ml_system.ML";
-
--- a/src/Pure/ML-Systems/polyml.ML Thu May 24 15:11:53 2012 +0200
+++ b/src/Pure/ML-Systems/polyml.ML Thu May 24 15:54:38 2012 +0200
@@ -1,16 +1,10 @@
(* Title: Pure/ML-Systems/polyml.ML
+ Author: Makarius
-Compatibility wrapper for Poly/ML 5.3 and 5.4.
+Compatibility wrapper for Poly/ML 5.3.0 or later.
*)
-open Thread;
-
-structure ML_Name_Space =
-struct
- open PolyML.NameSpace;
- type T = PolyML.NameSpace.nameSpace;
- val global = PolyML.globalNameSpace;
-end;
+(* exceptions *)
fun reraise exn =
(case PolyML.exceptionLocation exn of
@@ -33,22 +27,104 @@
NONE => NONE
| SOME i => if i >= 0 then NONE else SOME (~ i));
-use "ML-Systems/polyml_common.ML";
+exception Interrupt = SML90.Interrupt;
+
+use "General/exn.ML";
+
+
+(* multithreading *)
+
+val seconds = Time.fromReal;
+
+if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
+then ()
+else use "ML-Systems/single_assignment_polyml.ML";
+
+open Thread;
+use "ML-Systems/multithreading.ML";
use "ML-Systems/multithreading_polyml.ML";
+
use "ML-Systems/unsynchronized.ML";
-
val _ = PolyML.Compiler.forgetValue "ref";
val _ = PolyML.Compiler.forgetType "ref";
+
+(* pervasive environment *)
+
+fun op before (a, _: unit) = a;
+
+val _ = PolyML.Compiler.forgetValue "isSome";
+val _ = PolyML.Compiler.forgetValue "getOpt";
+val _ = PolyML.Compiler.forgetValue "valOf";
+val _ = PolyML.Compiler.forgetValue "foldl";
+val _ = PolyML.Compiler.forgetValue "foldr";
+val _ = PolyML.Compiler.forgetValue "print";
+val _ = PolyML.Compiler.forgetValue "explode";
+val _ = PolyML.Compiler.forgetValue "concat";
+
+val ord = SML90.ord;
+val chr = SML90.chr;
+val raw_explode = SML90.explode;
+val implode = SML90.implode;
+
+fun quit () = exit 0;
+
+
+(* ML system identification *)
+
+use "ML-Systems/ml_system.ML";
+
+
+(* ML runtime system *)
+
+val exception_trace = PolyML.exception_trace;
+val timing = PolyML.timing;
+val profiling = PolyML.profiling;
+
+fun profile 0 f x = f x
+ | profile n f x =
+ let
+ val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
+ val res = Exn.capture f x;
+ val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
+ in Exn.release res end;
+
val pointer_eq = PolyML.pointerEq;
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
-use "ML-Systems/compiler_polyml-5.3.ML";
+
+(* ML compiler *)
+
+structure ML_Name_Space =
+struct
+ open PolyML.NameSpace;
+ type T = PolyML.NameSpace.nameSpace;
+ val global = PolyML.globalNameSpace;
+end;
+
+use "ML-Systems/use_context.ML";
+use "ML-Systems/compiler_polyml.ML";
+
PolyML.Compiler.reportUnreferencedIds := true;
+PolyML.Compiler.printInAlphabeticalOrder := false;
+PolyML.Compiler.maxInlineSize := 80;
+
+fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-(* toplevel pretty printing *)
+(* ML toplevel pretty printing *)
+
+use "ML-Systems/ml_pretty.ML";
+
+local
+ val depth = Unsynchronized.ref 10;
+in
+ fun get_print_depth () = ! depth;
+ fun print_depth n = (depth := n; PolyML.print_depth n);
+end;
+
+val error_depth = PolyML.error_depth;
val pretty_ml =
let
@@ -87,5 +163,3 @@
val ml_make_string =
"(fn x => Pretty.string_of (Pretty.from_ML (pretty_ml (PolyML.prettyRepresentation (x, get_print_depth ())))))";
-use "ML-Systems/ml_system.ML";
-
--- a/src/Pure/ML-Systems/polyml_common.ML Thu May 24 15:11:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,88 +0,0 @@
-(* Title: Pure/ML-Systems/polyml_common.ML
-
-Compatibility file for Poly/ML -- common part for 5.x.
-*)
-
-fun op before (a, _: unit) = a;
-
-exception Interrupt = SML90.Interrupt;
-
-use "General/exn.ML";
-
-if List.exists (fn s => s = "SingleAssignment") (PolyML.Compiler.structureNames ())
-then ()
-else use "ML-Systems/single_assignment_polyml.ML";
-
-use "ML-Systems/multithreading.ML";
-use "ML-Systems/ml_pretty.ML";
-use "ML-Systems/use_context.ML";
-
-val seconds = Time.fromReal;
-
-
-
-(** ML system and platform related **)
-
-val _ = PolyML.Compiler.forgetValue "isSome";
-val _ = PolyML.Compiler.forgetValue "getOpt";
-val _ = PolyML.Compiler.forgetValue "valOf";
-val _ = PolyML.Compiler.forgetValue "foldl";
-val _ = PolyML.Compiler.forgetValue "foldr";
-val _ = PolyML.Compiler.forgetValue "print";
-val _ = PolyML.Compiler.forgetValue "explode";
-val _ = PolyML.Compiler.forgetValue "concat";
-
-
-(* Compiler options *)
-
-PolyML.Compiler.printInAlphabeticalOrder := false;
-PolyML.Compiler.maxInlineSize := 80;
-
-
-(* old Poly/ML emulation *)
-
-fun quit () = exit 0;
-
-
-(* restore old-style character / string functions *)
-
-val ord = SML90.ord;
-val chr = SML90.chr;
-val raw_explode = SML90.explode;
-val implode = SML90.implode;
-
-
-(* prompts *)
-
-fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
-
-
-(* toplevel printing *)
-
-local
- val depth = ref 10;
-in
- fun get_print_depth () = ! depth;
- fun print_depth n = (depth := n; PolyML.print_depth n);
-end;
-
-val error_depth = PolyML.error_depth;
-
-val ml_make_string = "PolyML.makestring";
-
-
-
-(** Runtime system **)
-
-val exception_trace = PolyML.exception_trace;
-val timing = PolyML.timing;
-val profiling = PolyML.profiling;
-
-fun profile 0 f x = f x
- | profile n f x =
- let
- val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler n;
- val res = Exn.capture f x;
- val _ = RunCall.run_call1 RuntimeCalls.POLY_SYS_profiler 0;
- in Exn.release res end;
-
--- a/src/Pure/ML-Systems/pp_polyml.ML Thu May 24 15:11:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(* Title: Pure/ML-Systems/pp_polyml.ML
-
-Toplevel pretty printing for Poly/ML before 5.3.
-*)
-
-fun ml_pprint (print, begin_blk, brk, end_blk) =
- let
- fun str "" = ()
- | str s = print s;
- fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
- (str bg; begin_blk (ind, false); List.app pprint prts; end_blk (); str en)
- | pprint (ML_Pretty.String (s, _)) = str s
- | pprint (ML_Pretty.Break (false, wd)) = brk (wd, 0)
- | pprint (ML_Pretty.Break (true, _)) = brk (99999, 0);
- in pprint end;
-
-fun toplevel_pp context (_: string list) pp =
- use_text context (1, "pp") false
- ("PolyML.install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
-
--- a/src/Pure/ML/install_pp_polyml-5.3.ML Thu May 24 15:11:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(* Title: Pure/ML/install_pp_polyml-5.3.ML
- Author: Makarius
-
-Extra toplevel pretty-printing for Poly/ML 5.3.0.
-*)
-
-PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
- ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
-
-PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
- ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
- pretty (Synchronized.value var, depth));
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
- (case Future.peek x of
- NONE => PolyML.PrettyString "<future>"
- | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Res y) => pretty (y, depth)));
-
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
- (case Lazy.peek x of
- NONE => PolyML.PrettyString "<lazy>"
- | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
- | SOME (Exn.Res y) => pretty (y, depth)));
-
-PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
- let
- open PolyML;
- val from_ML = Pretty.from_ML o pretty_ml;
- fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
- fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
- fun prt_term parens dp (t as _ $ _) =
- op :: (strip_comb t)
- |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
- |> Pretty.separate " $"
- |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
- | prt_term _ dp (Abs (x, T, body)) =
- prt_apps "Abs"
- [from_ML (prettyRepresentation (x, dp - 1)),
- from_ML (prettyRepresentation (T, dp - 2)),
- prt_term false (dp - 3) body]
- | prt_term _ dp (Const const) =
- prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
- | prt_term _ dp (Free free) =
- prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
- | prt_term _ dp (Var var) =
- prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
- | prt_term _ dp (Bound i) =
- prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
- in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
-
--- a/src/Pure/ML/install_pp_polyml.ML Thu May 24 15:11:53 2012 +0200
+++ b/src/Pure/ML/install_pp_polyml.ML Thu May 24 15:54:38 2012 +0200
@@ -1,20 +1,53 @@
(* Title: Pure/ML/install_pp_polyml.ML
Author: Makarius
-Extra toplevel pretty-printing for Poly/ML.
+Extra toplevel pretty-printing for Poly/ML 5.3.0 or later.
*)
-PolyML.install_pp
- (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a future) =>
- (case Future.peek x of
- NONE => str "<future>"
- | SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Res y) => print (y, depth)));
+PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
+ ml_pretty (Pretty.to_ML (ML_Syntax.pretty_string (depth * 100) str)));
+
+PolyML.addPrettyPrinter (fn depth => fn _ => fn tree =>
+ ml_pretty (Pretty.to_ML (XML.pretty depth tree)));
+
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
+ pretty (Synchronized.value var, depth));
+
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ (case Future.peek x of
+ NONE => PolyML.PrettyString "<future>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+ | SOME (Exn.Res y) => pretty (y, depth)));
+
+PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ (case Lazy.peek x of
+ NONE => PolyML.PrettyString "<lazy>"
+ | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
+ | SOME (Exn.Res y) => pretty (y, depth)));
-PolyML.install_pp
- (fn (str, _, _, _) => fn depth => fn (print: 'a * int -> unit) => fn (x: 'a lazy) =>
- (case Lazy.peek x of
- NONE => str "<lazy>"
- | SOME (Exn.Exn _) => str "<failed>"
- | SOME (Exn.Res y) => print (y, depth)));
+PolyML.addPrettyPrinter (fn depth => fn _ => fn tm =>
+ let
+ open PolyML;
+ val from_ML = Pretty.from_ML o pretty_ml;
+ fun prt_app name prt = Pretty.block [Pretty.str (name ^ " "), prt];
+ fun prt_apps name = Pretty.enum "," (name ^ " (") ")";
+ fun prt_term parens dp (t as _ $ _) =
+ op :: (strip_comb t)
+ |> map_index (fn (i, u) => prt_term true (dp - i - 1) u)
+ |> Pretty.separate " $"
+ |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
+ | prt_term _ dp (Abs (x, T, body)) =
+ prt_apps "Abs"
+ [from_ML (prettyRepresentation (x, dp - 1)),
+ from_ML (prettyRepresentation (T, dp - 2)),
+ prt_term false (dp - 3) body]
+ | prt_term _ dp (Const const) =
+ prt_app "Const" (from_ML (prettyRepresentation (const, dp - 1)))
+ | prt_term _ dp (Free free) =
+ prt_app "Free" (from_ML (prettyRepresentation (free, dp - 1)))
+ | prt_term _ dp (Var var) =
+ prt_app "Var" (from_ML (prettyRepresentation (var, dp - 1)))
+ | prt_term _ dp (Bound i) =
+ prt_app "Bound" (from_ML (prettyRepresentation (i, dp - 1)));
+ in ml_pretty (Pretty.to_ML (prt_term false depth tm)) end);
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Thu May 24 15:11:53 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,202 +0,0 @@
-(* Title: Pure/ML/ml_compiler_polyml-5.3.ML
- Author: Makarius
-
-Advanced runtime compilation for Poly/ML 5.3.0 or later.
-*)
-
-structure ML_Compiler: ML_COMPILER =
-struct
-
-(* source locations *)
-
-fun position_of (loc: PolyML.location) =
- let
- val {file = text, startLine = line, startPosition = offset,
- endLine = _, endPosition = end_offset} = loc;
- val props =
- (case YXML.parse text of
- XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
- | XML.Text s => Position.file_name s);
- in
- Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
- end;
-
-fun exn_position exn =
- (case PolyML.exceptionLocation exn of
- NONE => Position.none
- | SOME loc => position_of loc);
-
-val exn_messages = Runtime.exn_messages exn_position;
-val exn_message = Runtime.exn_message exn_position;
-
-
-(* parse trees *)
-
-fun report_parse_tree depth space =
- let
- val reported_text =
- (case Context.thread_data () of
- SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
- | _ => Position.reported_text);
-
- fun reported_entity kind loc decl =
- reported_text (position_of loc)
- (Isabelle_Markup.entityN,
- (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
-
- fun reported loc (PolyML.PTtype types) =
- cons
- (PolyML.NameSpace.displayTypeExpression (types, depth, space)
- |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
- |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
- | reported loc (PolyML.PTdeclaredAt decl) =
- cons (reported_entity Isabelle_Markup.ML_defN loc decl)
- | reported loc (PolyML.PTopenedAt decl) =
- cons (reported_entity Isabelle_Markup.ML_openN loc decl)
- | reported loc (PolyML.PTstructureAt decl) =
- cons (reported_entity Isabelle_Markup.ML_structN loc decl)
- | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
- | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
- | reported _ _ = I
- and reported_tree (loc, props) = fold (reported loc) props;
- in fn tree => Output.report (implode (reported_tree tree [])) end;
-
-
-(* eval ML source tokens *)
-
-fun eval verbose pos toks =
- let
- val _ = Secure.secure_mltext ();
- val space = ML_Env.name_space;
-
-
- (* input *)
-
- val location_props =
- op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
- (filter (member (op =)
- [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
-
- val input_buffer =
- Unsynchronized.ref (toks |> map
- (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
-
- fun get () =
- (case ! input_buffer of
- (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
- | ([], _) :: rest => (input_buffer := rest; SOME #" ")
- | [] => NONE);
-
- fun get_pos () =
- (case ! input_buffer of
- (_ :: _, tok) :: _ => ML_Lex.pos_of tok
- | ([], tok) :: _ => ML_Lex.end_pos_of tok
- | [] => Position.none);
-
-
- (* output channels *)
-
- val writeln_buffer = Unsynchronized.ref Buffer.empty;
- fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
- fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
-
- val warnings = Unsynchronized.ref ([]: string list);
- fun warn msg = Unsynchronized.change warnings (cons msg);
- fun output_warnings () = List.app warning (rev (! warnings));
-
- val error_buffer = Unsynchronized.ref Buffer.empty;
- fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
- fun flush_error () = writeln (Buffer.content (! error_buffer));
- fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
-
- fun message {message = msg, hard, location = loc, context = _} =
- let
- val pos = position_of loc;
- val txt =
- (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
- ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
- Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
- Position.reported_text pos Isabelle_Markup.report "";
- in if hard then err txt else warn txt end;
-
-
- (* results *)
-
- val depth = get_print_depth ();
-
- fun apply_result {fixes, types, signatures, structures, functors, values} =
- let
- fun display disp x =
- if depth > 0 then
- (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
- else ();
-
- fun apply_fix (a, b) =
- (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
- fun apply_type (a, b) =
- (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
- fun apply_sig (a, b) =
- (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
- fun apply_struct (a, b) =
- (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
- fun apply_funct (a, b) =
- (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
- fun apply_val (a, b) =
- (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
- in
- List.app apply_fix fixes;
- List.app apply_type types;
- List.app apply_sig signatures;
- List.app apply_struct structures;
- List.app apply_funct functors;
- List.app apply_val values
- end;
-
- exception STATIC_ERRORS of unit;
-
- fun result_fun (phase1, phase2) () =
- ((case phase1 of
- NONE => ()
- | SOME parse_tree => report_parse_tree depth space parse_tree);
- (case phase2 of
- NONE => raise STATIC_ERRORS ()
- | SOME code =>
- apply_result
- ((code
- |> Runtime.debugging
- |> Runtime.toplevel_error (err o exn_message)) ())));
-
-
- (* compiler invocation *)
-
- val parameters =
- [PolyML.Compiler.CPOutStream write,
- PolyML.Compiler.CPNameSpace space,
- PolyML.Compiler.CPErrorMessageProc message,
- PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
- PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
- PolyML.Compiler.CPFileName location_props,
- PolyML.Compiler.CPCompilerResultFun result_fun,
- PolyML.Compiler.CPPrintInAlphabeticalOrder false];
- val _ =
- (while not (List.null (! input_buffer)) do
- PolyML.compiler (get, parameters) ())
- handle exn =>
- if Exn.is_interrupt exn then reraise exn
- else
- let
- val exn_msg =
- (case exn of
- STATIC_ERRORS () => ""
- | Runtime.TOPLEVEL_ERROR => ""
- | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
- val _ = output_warnings ();
- val _ = output_writeln ();
- in raise_error exn_msg end;
- in
- if verbose then (output_warnings (); flush_error (); output_writeln ())
- else ()
- end;
-
-end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_compiler_polyml.ML Thu May 24 15:54:38 2012 +0200
@@ -0,0 +1,202 @@
+(* Title: Pure/ML/ml_compiler_polyml.ML
+ Author: Makarius
+
+Advanced runtime compilation for Poly/ML 5.3.0 or later.
+*)
+
+structure ML_Compiler: ML_COMPILER =
+struct
+
+(* source locations *)
+
+fun position_of (loc: PolyML.location) =
+ let
+ val {file = text, startLine = line, startPosition = offset,
+ endLine = _, endPosition = end_offset} = loc;
+ val props =
+ (case YXML.parse text of
+ XML.Elem ((e, atts), _) => if e = Isabelle_Markup.positionN then atts else []
+ | XML.Text s => Position.file_name s);
+ in
+ Position.make {line = line, offset = offset, end_offset = end_offset, props = props}
+ end;
+
+fun exn_position exn =
+ (case PolyML.exceptionLocation exn of
+ NONE => Position.none
+ | SOME loc => position_of loc);
+
+val exn_messages = Runtime.exn_messages exn_position;
+val exn_message = Runtime.exn_message exn_position;
+
+
+(* parse trees *)
+
+fun report_parse_tree depth space =
+ let
+ val reported_text =
+ (case Context.thread_data () of
+ SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
+ | _ => Position.reported_text);
+
+ fun reported_entity kind loc decl =
+ reported_text (position_of loc)
+ (Isabelle_Markup.entityN,
+ (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
+
+ fun reported loc (PolyML.PTtype types) =
+ cons
+ (PolyML.NameSpace.displayTypeExpression (types, depth, space)
+ |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
+ |> reported_text (position_of loc) Isabelle_Markup.ML_typing)
+ | reported loc (PolyML.PTdeclaredAt decl) =
+ cons (reported_entity Isabelle_Markup.ML_defN loc decl)
+ | reported loc (PolyML.PTopenedAt decl) =
+ cons (reported_entity Isabelle_Markup.ML_openN loc decl)
+ | reported loc (PolyML.PTstructureAt decl) =
+ cons (reported_entity Isabelle_Markup.ML_structN loc decl)
+ | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
+ | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
+ | reported _ _ = I
+ and reported_tree (loc, props) = fold (reported loc) props;
+ in fn tree => Output.report (implode (reported_tree tree [])) end;
+
+
+(* eval ML source tokens *)
+
+fun eval verbose pos toks =
+ let
+ val _ = Secure.secure_mltext ();
+ val space = ML_Env.name_space;
+
+
+ (* input *)
+
+ val location_props =
+ op ^ (YXML.output_markup (Isabelle_Markup.position |> Markup.properties
+ (filter (member (op =)
+ [Isabelle_Markup.idN, Isabelle_Markup.fileN] o #1) (Position.properties_of pos))));
+
+ val input_buffer =
+ Unsynchronized.ref (toks |> map
+ (`(maps (String.explode o Symbol.esc) o Symbol.explode o ML_Lex.check_content_of)));
+
+ fun get () =
+ (case ! input_buffer of
+ (c :: cs, tok) :: rest => (input_buffer := (cs, tok) :: rest; SOME c)
+ | ([], _) :: rest => (input_buffer := rest; SOME #" ")
+ | [] => NONE);
+
+ fun get_pos () =
+ (case ! input_buffer of
+ (_ :: _, tok) :: _ => ML_Lex.pos_of tok
+ | ([], tok) :: _ => ML_Lex.end_pos_of tok
+ | [] => Position.none);
+
+
+ (* output channels *)
+
+ val writeln_buffer = Unsynchronized.ref Buffer.empty;
+ fun write s = Unsynchronized.change writeln_buffer (Buffer.add s);
+ fun output_writeln () = writeln (Buffer.content (! writeln_buffer));
+
+ val warnings = Unsynchronized.ref ([]: string list);
+ fun warn msg = Unsynchronized.change warnings (cons msg);
+ fun output_warnings () = List.app warning (rev (! warnings));
+
+ val error_buffer = Unsynchronized.ref Buffer.empty;
+ fun err msg = Unsynchronized.change error_buffer (Buffer.add msg #> Buffer.add "\n");
+ fun flush_error () = writeln (Buffer.content (! error_buffer));
+ fun raise_error msg = error (Buffer.content (Buffer.add msg (! error_buffer)));
+
+ fun message {message = msg, hard, location = loc, context = _} =
+ let
+ val pos = position_of loc;
+ val txt =
+ (Position.is_reported pos ? Markup.markup Isabelle_Markup.no_report)
+ ((if hard then "Error" else "Warning") ^ Position.str_of pos ^ ":\n") ^
+ Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
+ Position.reported_text pos Isabelle_Markup.report "";
+ in if hard then err txt else warn txt end;
+
+
+ (* results *)
+
+ val depth = get_print_depth ();
+
+ fun apply_result {fixes, types, signatures, structures, functors, values} =
+ let
+ fun display disp x =
+ if depth > 0 then
+ (disp x |> pretty_ml |> Pretty.from_ML |> Pretty.string_of |> write; write "\n")
+ else ();
+
+ fun apply_fix (a, b) =
+ (#enterFix space (a, b); display PolyML.NameSpace.displayFix (a, b));
+ fun apply_type (a, b) =
+ (#enterType space (a, b); display PolyML.NameSpace.displayType (b, depth, space));
+ fun apply_sig (a, b) =
+ (#enterSig space (a, b); display PolyML.NameSpace.displaySig (b, depth, space));
+ fun apply_struct (a, b) =
+ (#enterStruct space (a, b); display PolyML.NameSpace.displayStruct (b, depth, space));
+ fun apply_funct (a, b) =
+ (#enterFunct space (a, b); display PolyML.NameSpace.displayFunct (b, depth, space));
+ fun apply_val (a, b) =
+ (#enterVal space (a, b); display PolyML.NameSpace.displayVal (b, depth, space));
+ in
+ List.app apply_fix fixes;
+ List.app apply_type types;
+ List.app apply_sig signatures;
+ List.app apply_struct structures;
+ List.app apply_funct functors;
+ List.app apply_val values
+ end;
+
+ exception STATIC_ERRORS of unit;
+
+ fun result_fun (phase1, phase2) () =
+ ((case phase1 of
+ NONE => ()
+ | SOME parse_tree => report_parse_tree depth space parse_tree);
+ (case phase2 of
+ NONE => raise STATIC_ERRORS ()
+ | SOME code =>
+ apply_result
+ ((code
+ |> Runtime.debugging
+ |> Runtime.toplevel_error (err o exn_message)) ())));
+
+
+ (* compiler invocation *)
+
+ val parameters =
+ [PolyML.Compiler.CPOutStream write,
+ PolyML.Compiler.CPNameSpace space,
+ PolyML.Compiler.CPErrorMessageProc message,
+ PolyML.Compiler.CPLineNo (the_default 0 o Position.line_of o get_pos),
+ PolyML.Compiler.CPLineOffset (the_default 0 o Position.offset_of o get_pos),
+ PolyML.Compiler.CPFileName location_props,
+ PolyML.Compiler.CPCompilerResultFun result_fun,
+ PolyML.Compiler.CPPrintInAlphabeticalOrder false];
+ val _ =
+ (while not (List.null (! input_buffer)) do
+ PolyML.compiler (get, parameters) ())
+ handle exn =>
+ if Exn.is_interrupt exn then reraise exn
+ else
+ let
+ val exn_msg =
+ (case exn of
+ STATIC_ERRORS () => ""
+ | Runtime.TOPLEVEL_ERROR => ""
+ | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
+ val _ = output_warnings ();
+ val _ = output_writeln ();
+ in raise_error exn_msg end;
+ in
+ if verbose then (output_warnings (); flush_error (); output_writeln ())
+ else ()
+ end;
+
+end;
+
--- a/src/Pure/ROOT.ML Thu May 24 15:11:53 2012 +0200
+++ b/src/Pure/ROOT.ML Thu May 24 15:54:38 2012 +0200
@@ -74,7 +74,7 @@
if Multithreading.available then ()
else use "Concurrent/single_assignment_sequential.ML";
-if ML_System.is_smlnj then () else use "Concurrent/time_limit.ML";
+if ML_System.is_polyml then use "Concurrent/time_limit.ML" else ();
if Multithreading.available
then use "Concurrent/bash.ML"
@@ -191,8 +191,7 @@
use "ML/ml_env.ML";
use "Isar/runtime.ML";
use "ML/ml_compiler.ML";
-if ML_System.name = "polyml-5.2.1" orelse ML_System.is_smlnj then ()
-else use "ML/ml_compiler_polyml-5.3.ML";
+if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
use "ML/ml_context.ML";
(*theory sources*)
--- a/src/Pure/pure_setup.ML Thu May 24 15:11:53 2012 +0200
+++ b/src/Pure/pure_setup.ML Thu May 24 15:54:38 2012 +0200
@@ -36,11 +36,7 @@
toplevel_pp ["Proof", "state"] "(fn _: Proof.state => Pretty.str \"<Proof.state>\")";
toplevel_pp ["Toplevel", "state"] "Toplevel.pretty_abstract";
-if ML_System.name = "polyml-5.2.1"
-then use "ML/install_pp_polyml.ML"
-else if ML_System.is_polyml
-then use "ML/install_pp_polyml-5.3.ML"
-else ();
+if ML_System.is_polyml then use "ML/install_pp_polyml.ML" else ();
(* ML toplevel use commands *)