--- a/Admin/polyml/future/ROOT.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/Admin/polyml/future/ROOT.ML Sat Apr 02 21:10:07 2016 +0200
@@ -116,16 +116,16 @@
use "Concurrent/mailbox.ML";
use "Concurrent/cache.ML";
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
+ML_system_pp (fn depth => fn pretty => fn var =>
pretty (Synchronized.value var, depth));
-PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ML_system_pp (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 =>
+ML_system_pp (fn depth => fn pretty => fn x =>
(case Lazy.peek x of
NONE => PolyML.PrettyString "<lazy>"
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
--- a/src/Pure/Concurrent/future.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/future.ML Sat Apr 02 21:10:07 2016 +0200
@@ -100,7 +100,7 @@
fun is_finished x = is_some (peek x);
val _ =
- PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ ML_system_pp (fn depth => fn pretty => fn x =>
(case peek x of
NONE => PolyML.PrettyString "<future>"
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
--- a/src/Pure/Concurrent/lazy.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/lazy.ML Sat Apr 02 21:10:07 2016 +0200
@@ -103,7 +103,7 @@
(* toplevel pretty printing *)
val _ =
- PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
+ ML_system_pp (fn depth => fn pretty => fn x =>
(case peek x of
NONE => PolyML.PrettyString "<lazy>"
| SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
--- a/src/Pure/Concurrent/synchronized.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/synchronized.ML Sat Apr 02 21:10:07 2016 +0200
@@ -69,6 +69,6 @@
(* toplevel pretty printing *)
-val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => pretty (value var, depth));
+val _ = ML_system_pp (fn depth => fn pretty => fn var => pretty (value var, depth));
end;
--- a/src/Pure/Concurrent/task_queue.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Sat Apr 02 21:10:07 2016 +0200
@@ -397,7 +397,7 @@
(* toplevel pretty printing *)
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
end;
--- a/src/Pure/General/binding.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/binding.ML Sat Apr 02 21:10:07 2016 +0200
@@ -154,7 +154,7 @@
val print = Pretty.unformatted_string_of o pretty;
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
(* check *)
--- a/src/Pure/General/linear_set.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/linear_set.ML Sat Apr 02 21:10:07 2016 +0200
@@ -136,11 +136,11 @@
(* ML pretty-printing *)
val _ =
- PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
+ ML_system_pp (fn depth => fn pretty => fn set =>
ML_Pretty.to_polyml
(ML_Pretty.enum "," "{" "}"
(ML_Pretty.pair
- (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+ (ML_Pretty.from_polyml o ML_system_pretty)
(ML_Pretty.from_polyml o pretty))
(dest set, depth)));
--- a/src/Pure/General/path.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/path.ML Sat Apr 02 21:10:07 2016 +0200
@@ -173,7 +173,7 @@
val print = Pretty.unformatted_string_of o pretty;
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
(* base element *)
--- a/src/Pure/General/pretty.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/pretty.ML Sat Apr 02 21:10:07 2016 +0200
@@ -402,7 +402,7 @@
end;
-val _ = PolyML.addPrettyPrinter (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
+val _ = ML_system_pp (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
+val _ = ML_system_pp (fn _ => fn _ => to_polyml o position);
end;
--- a/src/Pure/General/sha1.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/sha1.ML Sat Apr 02 21:10:07 2016 +0200
@@ -182,7 +182,7 @@
fun rep (Digest s) = s;
val fake = Digest;
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
fun digest_string str = digest_string_external str
handle CInterface.Foreign msg =>
--- a/src/Pure/General/table.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/General/table.ML Sat Apr 02 21:10:07 2016 +0200
@@ -411,11 +411,11 @@
(* ML pretty-printing *)
val _ =
- PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
+ ML_system_pp (fn depth => fn pretty => fn tab =>
ML_Pretty.to_polyml
(ML_Pretty.enum "," "{" "}"
(ML_Pretty.pair
- (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
+ (ML_Pretty.from_polyml o ML_system_pretty)
(ML_Pretty.from_polyml o pretty))
(dest tab, depth)));
--- a/src/Pure/Isar/proof.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Isar/proof.ML Sat Apr 02 21:10:07 2016 +0200
@@ -174,7 +174,7 @@
(context * thm list list -> context -> context)};
val _ =
- PolyML.addPrettyPrinter (fn _ => fn _ => fn _: state =>
+ ML_system_pp (fn _ => fn _ => fn _: state =>
Pretty.to_polyml (Pretty.str "<Proof.state>"));
fun make_goal (statement, using, goal, before_qed, after_qed) =
--- a/src/Pure/Isar/runtime.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Isar/runtime.ML Sat Apr 02 21:10:07 2016 +0200
@@ -43,7 +43,7 @@
fun pretty_exn (exn: exn) =
Pretty.from_ML
(ML_Pretty.from_polyml
- (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
+ (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
(* exn_context *)
--- a/src/Pure/Isar/toplevel.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Isar/toplevel.ML Sat Apr 02 21:10:07 2016 +0200
@@ -199,7 +199,7 @@
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
--- a/src/Pure/ML/ml_compiler0.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_compiler0.ML Sat Apr 02 21:10:07 2016 +0200
@@ -139,3 +139,15 @@
{verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
handle ERROR msg => (#print context msg; raise error "ML error"))
end;
+
+
+(* export type-dependent functions *)
+
+ML_Compiler0.use_text
+ (ML_Compiler0.make_context
+ (ML_Name_Space.global_values
+ [("prettyRepresentation", "ML_system_pretty"),
+ ("addPrettyPrinter", "ML_system_pp"),
+ ("addOverload", "ML_system_overload")]))
+ {debug = false, file = "", line = 0, verbose = false}
+ "open PolyML RunCall";
--- a/src/Pure/ML/ml_debugger.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_debugger.ML Sat Apr 02 21:10:07 2016 +0200
@@ -42,7 +42,7 @@
end;
val _ =
- PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
+ ML_system_pp (fn _ => fn _ => fn exn_id =>
let val s = print_exn_id exn_id
in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
--- a/src/Pure/ML/ml_name_space.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML Sat Apr 02 21:10:07 2016 +0200
@@ -11,7 +11,31 @@
open PolyML.NameSpace;
type T = PolyML.NameSpace.nameSpace;
+
val global = PolyML.globalNameSpace;
+ fun global_values values : T =
+ {lookupVal = #lookupVal global,
+ lookupType = #lookupType global,
+ lookupStruct = #lookupStruct global,
+ lookupFix = #lookupFix global,
+ lookupSig = #lookupSig global,
+ lookupFunct = #lookupFunct global,
+ enterVal =
+ fn (x, value) =>
+ (case List.find (fn (y, _) => x = y) values of
+ SOME (_, x') => #enterVal global (x', value)
+ | NONE => ()),
+ enterType = fn _ => (),
+ enterFix = fn _ => (),
+ enterStruct = fn _ => (),
+ enterSig = fn _ => (),
+ enterFunct = fn _ => (),
+ allVal = #allVal global,
+ allType = #allType global,
+ allFix = #allFix global,
+ allStruct = #allStruct global,
+ allSig = #allSig global,
+ allFunct = #allFunct global};
type valueVal = Values.value;
fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
--- a/src/Pure/ML/ml_pp.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_pp.ML Sat Apr 02 21:10:07 2016 +0200
@@ -8,22 +8,22 @@
struct
val _ =
- PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
+ ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ =>
+ ML_system_pp (fn depth => fn _ =>
ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ =>
+ ML_system_pp (fn depth => fn _ =>
ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ =>
+ ML_system_pp (fn depth => fn _ =>
ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ =>
+ ML_system_pp (fn depth => fn _ =>
ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
@@ -43,17 +43,17 @@
|> (if parens then Pretty.enclose "(" ")" else Pretty.block)
| Abs (a, T, b) =>
prt_apps "Abs"
- [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
- Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
+ [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
+ Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
prt_term false (dp - 3) b]
- | Const a => prt_app "Const" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
- | Free a => prt_app "Free" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
- | Var a => prt_app "Var" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
- | Bound a => prt_app "Bound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))));
+ | Const a => prt_app "Const" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+ | Free a => prt_app "Free" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+ | Var a => prt_app "Var" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+ | Bound a => prt_app "Bound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))));
in
-val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
local
@@ -66,22 +66,22 @@
| _ %% _ => prt_proofs parens dp prf
| Abst (a, T, b) =>
prt_apps "Abst"
- [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
- Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
+ [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
+ Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
prt_proof false (dp - 3) b]
| AbsP (a, t, b) =>
prt_apps "AbsP"
- [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
- Pretty.from_polyml (PolyML.prettyRepresentation (t, dp - 2)),
+ [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
+ Pretty.from_polyml (ML_system_pretty (t, dp - 2)),
prt_proof false (dp - 3) b]
| Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
| MinProof => Pretty.str "MinProof"
- | PBound a => prt_app "PBound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
- | PAxm a => prt_app "PAxm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
- | OfClass a => prt_app "OfClass" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
- | Oracle a => prt_app "Oracle" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
- | Promise a => prt_app "Promise" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
- | PThm a => prt_app "PThm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))))
+ | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+ | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+ | OfClass a => prt_app "OfClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+ | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+ | Promise a => prt_app "Promise" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
+ | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
and prt_proofs parens dp prf =
let
@@ -94,7 +94,7 @@
strip_proof p
((fn d =>
[Pretty.str " %", Pretty.brk 1,
- Pretty.from_polyml (PolyML.prettyRepresentation (t, d))]) :: res)
+ Pretty.from_polyml (ML_system_pretty (t, d))]) :: res)
| strip_proof (p %% q) res =
strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
| strip_proof p res = (fn d => prt_proof true d p, res);
@@ -102,7 +102,7 @@
in
val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
+ ML_system_pp (fn depth => fn _ => fn prf =>
ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
end;
--- a/src/Pure/ML/ml_pretty.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_pretty.ML Sat Apr 02 21:10:07 2016 +0200
@@ -116,7 +116,7 @@
local
fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
- fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
+ fun pretty_value depth = "ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))";
in
fun make_string_fn local_env =
--- a/src/Pure/ML/ml_syntax.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/ML/ml_syntax.ML Sat Apr 02 21:10:07 2016 +0200
@@ -124,7 +124,7 @@
in Pretty.str (quote (implode (map print_char body'))) end;
val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
+ ML_system_pp (fn depth => fn _ => fn str =>
Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
end;
--- a/src/Pure/PIDE/xml.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/PIDE/xml.ML Sat Apr 02 21:10:07 2016 +0200
@@ -170,8 +170,7 @@
fun pretty depth tree =
Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
-val _ =
- PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
+val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
--- a/src/Pure/Syntax/ast.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Syntax/ast.ML Sat Apr 02 21:10:07 2016 +0200
@@ -66,7 +66,7 @@
fun pretty_rule (lhs, rhs) =
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs];
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
(* strip_positions *)
--- a/src/Pure/Syntax/lexicon.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/Syntax/lexicon.ML Sat Apr 02 21:10:07 2016 +0200
@@ -451,7 +451,7 @@
(* toplevel pretty printing *)
val _ =
- PolyML.addPrettyPrinter (fn _ => fn _ =>
+ ML_system_pp (fn _ => fn _ =>
Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
end;
--- a/src/Pure/context.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/context.ML Sat Apr 02 21:10:07 2016 +0200
@@ -169,7 +169,7 @@
val pretty_thy = Pretty.str_list "{" "}" o display_names;
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
fun pretty_abbrev_thy thy =
let
--- a/src/Pure/morphism.ML Sat Apr 02 20:33:34 2016 +0200
+++ b/src/Pure/morphism.ML Sat Apr 02 21:10:07 2016 +0200
@@ -71,7 +71,7 @@
fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
-val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
+val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
fun binding (Morphism {binding, ...}) = apply binding;
fun typ (Morphism {typ, ...}) = apply typ;