# HG changeset patch
# User wenzelm
# Date 1237663333 -3600
# Node ID 5bfea958f893965af368c8281f70bc8a722cfac8
# Parent  be354d68c4e4e98be1974fb3a3e71e86c92cdd0a# Parent  4078276bcace17e42c59ebf5ca7b5372a1e74e94
merged

diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Concurrent/future.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -44,6 +44,7 @@
   val join_result: 'a future -> 'a Exn.result
   val join: 'a future -> 'a
   val map: ('a -> 'b) -> 'a future -> 'b future
+  val interruptible_task: ('a -> 'b) -> 'a -> 'b
   val interrupt_task: string -> unit
   val cancel_group: group -> unit
   val cancel: 'a future -> unit
@@ -350,6 +351,15 @@
 
 (* cancellation *)
 
+fun interruptible_task f x =
+  if Multithreading.available then
+    Multithreading.with_attributes
+      (if is_some (thread_data ())
+       then Multithreading.restricted_interrupts
+       else Multithreading.regular_interrupts)
+      (fn _ => f) x
+  else interruptible f x;
+
 (*interrupt: permissive signal, may get ignored*)
 fun interrupt_task id = SYNCHRONIZED "interrupt"
   (fn () => Task_Queue.interrupt_external (! queue) id);
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/General/pretty.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -19,9 +19,6 @@
 a unit for breaking).
 *)
 
-type pprint_args = (output -> unit) * (int -> unit) * (int -> unit) *
-  (unit -> unit) * (unit -> unit);
-
 signature PRETTY =
 sig
   val default_indent: string -> int -> output
@@ -49,6 +46,7 @@
   val commas: T list -> T list
   val enclose: string -> string -> T list -> T
   val enum: string -> string -> string -> T list -> T
+  val position: Position.T -> T
   val list: string -> string -> T list -> T
   val str_list: string -> string -> string list -> T
   val big_list: string -> T list -> T
@@ -57,7 +55,8 @@
   val setmargin: int -> unit
   val setmp_margin: int -> ('a -> 'b) -> 'a -> 'b
   val setdepth: int -> unit
-  val pprint: T -> pprint_args -> unit
+  val to_ML: T -> ML_Pretty.pretty
+  val from_ML: ML_Pretty.pretty -> T
   val symbolicN: string
   val output_buffer: T -> Buffer.T
   val output: T -> output
@@ -159,6 +158,9 @@
 
 fun enum sep lpar rpar prts = enclose lpar rpar (separate sep prts);
 
+val position =
+  enum "," "{" "}" o map (fn (x, y) => str (x ^ "=" ^ y)) o Position.properties_of;
+
 val list = enum ",";
 fun str_list lpar rpar strs = list lpar rpar (map str strs);
 
@@ -318,20 +320,16 @@
       | fmt (Break (true, _)) = Buffer.add (output_spaces 1);
   in fmt (prune prt) Buffer.empty end;
 
-(*ML toplevel pretty printing*)
-fun pprint prt (put_str0, begin_blk, put_brk, put_fbrk, end_blk) =
-  let
-    fun put_str "" = ()
-      | put_str s = put_str0 s;
-    fun pp (Block (m, prts, ind, _)) =
-          let val (bg, en) = Markup.output m
-          in put_str bg; begin_blk ind; pp_lst prts; end_blk (); put_str en end
-      | pp (String (s, _)) = put_str s
-      | pp (Break (false, wd)) = put_brk wd
-      | pp (Break (true, _)) = put_fbrk ()
-    and pp_lst [] = ()
-      | pp_lst (prt :: prts) = (pp prt; pp_lst prts);
-  in pp (prune prt) end;
+
+(* ML toplevel pretty printing *)
+
+fun to_ML (Block (m, prts, ind, _)) = ML_Pretty.Block (Markup.output m, map to_ML prts, ind)
+  | to_ML (String s) = ML_Pretty.String s
+  | to_ML (Break b) = ML_Pretty.Break b;
+
+fun from_ML (ML_Pretty.Block (_, prts, ind)) = blk (ind, map from_ML prts)
+  | from_ML (ML_Pretty.String s) = String s
+  | from_ML (ML_Pretty.Break b) = Break b;
 
 
 (* output interfaces *)
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/General/secure.ML
--- a/src/Pure/General/secure.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/General/secure.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -14,6 +14,7 @@
   val use_file: ML_NameSpace.nameSpace ->
     (string -> unit) * (string -> 'a) -> bool -> string -> unit
   val use: string -> unit
+  val toplevel_pp: string list -> string -> unit
   val commit: unit -> unit
   val system_out: string -> string * int
   val system: string -> int
@@ -41,6 +42,8 @@
 
 fun raw_use_text ns = use_text ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
 fun raw_use_file ns = use_file ML_Parse.fix_ints (Position.str_of oo Position.line_file) ns;
+fun raw_toplevel_pp x =
+  toplevel_pp ML_Parse.fix_ints (Position.str_of oo Position.line_file) Output.ml_output x;
 
 fun use_text ns pos pr verbose txt =
   (secure_mltext (); raw_use_text ns pos pr verbose txt);
@@ -50,6 +53,8 @@
 
 fun use name = use_file ML_NameSpace.global Output.ml_output true name;
 
+fun toplevel_pp path pp = (secure_mltext (); raw_toplevel_pp path pp);
+
 (*commit is dynamically bound!*)
 fun commit () = raw_use_text ML_NameSpace.global (0, "") Output.ml_output false "commit();";
 
@@ -73,5 +78,6 @@
 val use_text = Secure.use_text;
 val use_file = Secure.use_file;
 fun use s = Secure.use s handle ERROR msg => (writeln msg; raise Fail "ML error");
+val toplevel_pp = Secure.toplevel_pp;
 val system_out = Secure.system_out;
 val system = Secure.system;
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/IsaMakefile	Sat Mar 21 20:22:13 2009 +0100
@@ -20,17 +20,17 @@
 ## Pure
 
 BOOTSTRAP_FILES = ML-Systems/exn.ML ML-Systems/ml_name_space.ML		\
-  ML-Systems/mosml.ML ML-Systems/multithreading.ML			\
-  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
-  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
-  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
-  ML-Systems/polyml-5.1.ML ML-Systems/polyml-experimental.ML		\
-  ML-Systems/polyml.ML ML-Systems/polyml_common.ML			\
-  ML-Systems/polyml_old_compiler4.ML					\
-  ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
-  ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
-  ML-Systems/thread_dummy.ML ML-Systems/time_limit.ML			\
-  ML-Systems/universal.ML
+  ML-Systems/ml_pretty.ML ML-Systems/mosml.ML				\
+  ML-Systems/multithreading.ML ML-Systems/multithreading_polyml.ML	\
+  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
+  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
+  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
+  ML-Systems/polyml-experimental.ML ML-Systems/polyml.ML		\
+  ML-Systems/polyml_common.ML ML-Systems/polyml_old_compiler4.ML	\
+  ML-Systems/polyml_old_compiler5.ML ML-Systems/polyml_pp.ML		\
+  ML-Systems/proper_int.ML ML-Systems/smlnj.ML				\
+  ML-Systems/system_shell.ML ML-Systems/thread_dummy.ML			\
+  ML-Systems/time_limit.ML ML-Systems/universal.ML
 
 RAW: $(OUT)/RAW
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Isar/proof_context.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -36,7 +36,6 @@
   val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
   val extern_fact: Proof.context -> string -> xstring
   val pretty_term_abbrev: Proof.context -> term -> Pretty.T
-  val pretty_thm_legacy: thm -> Pretty.T
   val pretty_thm: Proof.context -> thm -> Pretty.T
   val pretty_thms: Proof.context -> thm list -> Pretty.T
   val pretty_fact: Proof.context -> string * thm list -> Pretty.T
@@ -296,10 +295,6 @@
 
 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
 
-fun pretty_thm_legacy th =
-  let val thy = Thm.theory_of_thm th
-  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
-
 fun pretty_thm ctxt th =
   let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
   in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Isar/proof_display.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -6,12 +6,12 @@
 
 signature PROOF_DISPLAY =
 sig
-  val pprint_context: Proof.context -> pprint_args -> unit
-  val pprint_typ: theory -> typ -> pprint_args -> unit
-  val pprint_term: theory -> term -> pprint_args -> unit
-  val pprint_ctyp: ctyp -> pprint_args -> unit
-  val pprint_cterm: cterm -> pprint_args -> unit
-  val pprint_thm: thm -> pprint_args -> unit
+  val pp_context: Proof.context -> Pretty.T
+  val pp_thm: thm -> Pretty.T
+  val pp_typ: theory -> typ -> Pretty.T
+  val pp_term: theory -> term -> Pretty.T
+  val pp_ctyp: ctyp -> Pretty.T
+  val pp_cterm: cterm -> Pretty.T
   val print_theorems_diff: theory -> theory -> unit
   val print_theorems: theory -> unit
   val pretty_full_theory: bool -> theory -> Pretty.T
@@ -26,18 +26,20 @@
 
 (* toplevel pretty printing *)
 
-fun pprint_context ctxt = Pretty.pprint
+fun pp_context ctxt =
  (if ! ProofContext.debug then
     Pretty.quote (Pretty.big_list "proof context:" (ProofContext.pretty_context ctxt))
   else Pretty.str "<context>");
 
-fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (Syntax.init_pretty_global thy);
+fun pp_thm th =
+  let val thy = Thm.theory_of_thm th
+  in Display.pretty_thm_aux (Syntax.pp_global thy) true false [] th end;
 
-val pprint_typ = pprint Syntax.pretty_typ;
-val pprint_term = pprint Syntax.pretty_term;
-fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
-fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
-val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
+val pp_typ = Pretty.quote oo Syntax.pretty_typ_global;
+val pp_term = Pretty.quote oo Syntax.pretty_term_global;
+
+fun pp_ctyp cT = pp_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
+fun pp_cterm ct = pp_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
 
 
 (* theorems and theory *)
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Isar/toplevel.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -311,7 +311,7 @@
 fun controlled_execution f =
   f
   |> debugging
-  |> interruptible;
+  |> Future.interruptible_task;
 
 fun program f =
  (f
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/ml_pretty.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/ml_pretty.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/ml_pretty.ML
+    Author:     Makarius
+
+Raw datatype for ML pretty printing.
+*)
+
+structure ML_Pretty =
+struct
+
+datatype pretty =
+  Block of (string * string) * pretty list * int |
+  String of string * int |
+  Break of bool * int;
+
+end;
+
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/mosml.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -45,6 +45,7 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
 
 
 (*low-level pointer equality*)
@@ -118,10 +119,8 @@
     Meta.printLength := n);
 end;
 
-(*interface for toplevel pretty printers, see also Pure/pure_setup.ML*)
-(*the documentation refers to an installPP but I couldn't fine it!*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
+(*dummy implementation*)
+fun toplevel_pp _ _ _ _ _ = ();
 
 (*dummy implementation*)
 fun ml_prompts p1 p2 = ();
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-4.1.3.ML
--- a/src/Pure/ML-Systems/polyml-4.1.3.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-4.1.3.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -8,6 +8,7 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
 
 val pointer_eq = Address.wordEq;
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-4.1.4.ML
--- a/src/Pure/ML-Systems/polyml-4.1.4.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-4.1.4.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -8,6 +8,7 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
 
 val pointer_eq = Address.wordEq;
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-4.2.0.ML
--- a/src/Pure/ML-Systems/polyml-4.2.0.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-4.2.0.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -7,6 +7,7 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler4.ML";
+use "ML-Systems/polyml_pp.ML";
 
 val pointer_eq = Address.wordEq;
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-5.0.ML
--- a/src/Pure/ML-Systems/polyml-5.0.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-5.0.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -7,6 +7,7 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/polyml_pp.ML";
 
 val pointer_eq = PolyML.pointerEq;
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-5.1.ML
--- a/src/Pure/ML-Systems/polyml-5.1.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-5.1.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -6,6 +6,7 @@
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/polyml_common.ML";
 use "ML-Systems/polyml_old_compiler5.ML";
+use "ML-Systems/polyml_pp.ML";
 
 val pointer_eq = PolyML.pointerEq;
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -12,13 +12,6 @@
 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
 
 
-(* toplevel pretty printers *)
-
-(*dummy version*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-
-
 (* runtime compilation *)
 
 structure ML_NameSpace =
@@ -75,3 +68,16 @@
   in use_text tune str_of_pos name_space (1, name) output verbose txt end;
 
 end;
+
+
+(* toplevel pretty printing *)
+
+fun ml_pretty (ML_Pretty.Block (_, prts, ind)) = PrettyBlock (ind, false, [], map ml_pretty prts)
+  | ml_pretty (ML_Pretty.String (s, _)) = PrettyString s
+  | ml_pretty (ML_Pretty.Break (false, wd)) = PrettyBreak (wd, 0)
+  | ml_pretty (ML_Pretty.Break (true, _)) = PrettyBreak (99999, 0);
+
+fun toplevel_pp tune str_of_pos output (_: string list) pp =
+  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+    ("addPrettyPrinter (fn _ => fn _ => ml_pretty o Pretty.to_ML o (" ^ pp ^ "))");
+
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -68,3 +68,6 @@
   in use_text tune str_of_pos name_space (1, name) output verbose txt end;
 
 end;
+
+use "ML-Systems/polyml_pp.ML";
+
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml_common.ML
--- a/src/Pure/ML-Systems/polyml_common.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/polyml_common.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -10,6 +10,7 @@
 use "ML-Systems/time_limit.ML";
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
 
 
 (** ML system and platform related **)
@@ -73,13 +74,8 @@
 fun ml_prompts p1 p2 = (PolyML.Compiler.prompt1 := p1; PolyML.Compiler.prompt2 := p2);
 
 
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
+(* print depth *)
 
-fun make_pp _ pprint (str, blk, brk, en) _ _ obj =
-  pprint obj (str, fn ind => blk (ind, false), fn wd => brk (wd, 0),
-    fn () => brk (99999, 0), en);
-
-(*print depth*)
 local
   val depth = ref 10;
 in
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/polyml_pp.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/polyml_pp.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -0,0 +1,20 @@
+(*  Title:      Pure/ML-Systems/polyml_pp.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 tune str_of_pos output (_: string list) pp =
+  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+    ("install_pp (fn args => fn _ => fn _ => ml_pprint args o Pretty.to_ML o (" ^ pp ^ "))");
+
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -13,6 +13,7 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/system_shell.ML";
 use "ML-Systems/ml_name_space.ML";
+use "ML-Systems/ml_pretty.ML";
 
 
 (*low-level pointer equality*)
@@ -97,22 +98,6 @@
 fun makestring x = "dummy string for SML New Jersey";
 
 
-(* toplevel pretty printing (see also Pure/pure_setup.ML) *)
-
-fun make_pp path pprint =
-  let
-    open PrettyPrint;
-
-    fun pp pps obj =
-      pprint obj
-        (string pps, openHOVBox pps o Rel o dest_int,
-          fn wd => break pps {nsp=dest_int wd, offset=0}, fn () => newline pps,
-          fn () => closeBox pps);
-  in (path, pp) end;
-
-fun install_pp (path, pp) = CompilerPPTable.install_pp path pp;
-
-
 (* ML command execution *)
 
 fun use_text (tune: string -> string) _ _ (line: int, name) (print, err) verbose txt =
@@ -144,6 +129,26 @@
     ("structure " ^ name ^ " = struct end");
 
 
+(* toplevel pretty printing *)
+
+fun ml_pprint pps =
+  let
+    fun str "" = ()
+      | str s = PrettyPrint.string pps s;
+    fun pprint (ML_Pretty.Block ((bg, en), prts, ind)) =
+          (str bg; PrettyPrint.openHOVBox pps (PrettyPrint.Rel (dest_int ind));
+            List.app pprint prts; PrettyPrint.closeBox pps; str en)
+      | pprint (ML_Pretty.String (s, _)) = str s
+      | pprint (ML_Pretty.Break (false, wd)) = PrettyPrint.break pps {nsp = dest_int wd, offset = 0}
+      | pprint (ML_Pretty.Break (true, _)) = PrettyPrint.newline pps;
+  in pprint end;
+
+fun toplevel_pp tune str_of_pos output path pp =
+  use_text tune str_of_pos ML_NameSpace.global (1, "pp") output false
+    ("CompilerPPTable.install_pp [" ^ String.concatWith "," (map (fn s => "\"" ^ s ^ "\"")  path) ^
+      "] (fn pps => ml_pprint pps o Pretty.to_ML o (" ^ pp ^ "))");
+
+
 
 (** interrupts **)
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/Syntax/ast.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -20,7 +20,6 @@
   val str_of_ast: ast -> string
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
-  val pprint_ast: ast -> pprint_args -> unit
   val fold_ast: string -> ast list -> ast
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
@@ -79,8 +78,6 @@
   | pretty_ast (Appl asts) =
       Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
 
-val pprint_ast = Pretty.pprint o pretty_ast;
-
 fun pretty_rule (lhs, rhs) =
   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/context.ML
--- a/src/Pure/context.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/context.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -27,8 +27,6 @@
   val display_names: theory -> string list
   val pretty_thy: theory -> Pretty.T
   val string_of_thy: theory -> string
-  val pprint_thy: theory -> pprint_args -> unit
-  val pprint_thy_ref: theory_ref -> pprint_args -> unit
   val pretty_abbrev_thy: theory -> Pretty.T
   val str_of_thy: theory -> string
   val deref: theory_ref -> theory
@@ -228,7 +226,6 @@
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;
 val string_of_thy = Pretty.string_of o pretty_thy;
-val pprint_thy = Pretty.pprint o pretty_thy;
 
 fun pretty_abbrev_thy thy =
   let
@@ -256,8 +253,6 @@
     else thy_ref
   end;
 
-val pprint_thy_ref = Pretty.pprint o pretty_thy o deref;
-
 
 (* build ids *)
 
diff -r be354d68c4e4 -r 5bfea958f893 src/Pure/pure_setup.ML
--- a/src/Pure/pure_setup.ML	Sat Mar 21 09:42:55 2009 -0700
+++ b/src/Pure/pure_setup.ML	Sat Mar 21 20:22:13 2009 +0100
@@ -27,23 +27,25 @@
 
 (* ML toplevel pretty printing *)
 
-install_pp (make_pp ["Task_Queue", "task"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_task));
-install_pp (make_pp ["Task_Queue", "group"] (Pretty.pprint o Pretty.str o Task_Queue.str_of_group));
-install_pp (make_pp ["Position", "T"] (Pretty.pprint o Pretty.enum "," "{" "}" o
-  map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
-install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
-install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o quote o Binding.str_of));
-install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
-install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
-install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
-install_pp (make_pp ["Context", "proof"] ProofDisplay.pprint_context);
-install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
-install_pp (make_pp ["typ"] (ProofDisplay.pprint_typ Pure.thy));
-install_pp (make_pp ["Path", "T"] (Pretty.pprint o Pretty.str o quote o Path.implode));
-install_pp (make_pp ["File", "ident"] (Pretty.pprint o Pretty.str o quote o File.rep_ident));
+toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
+toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
+toplevel_pp ["Position", "T"] "Pretty.position";
+toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
+toplevel_pp ["Thm", "thm"] "ProofDisplay.pp_thm";
+toplevel_pp ["Thm", "cterm"] "ProofDisplay.pp_cterm";
+toplevel_pp ["Thm", "ctyp"] "ProofDisplay.pp_ctyp";
+toplevel_pp ["typ"] "ProofDisplay.pp_typ Pure.thy";
+toplevel_pp ["Context", "theory"] "Context.pretty_thy";
+toplevel_pp ["Context", "theory_ref"] "Context.pretty_thy o Theory.deref";
+toplevel_pp ["Context", "proof"] "ProofDisplay.pp_context";
+toplevel_pp ["Syntax", "ast"] "Syntax.pretty_ast";
+toplevel_pp ["Path", "T"] "Pretty.str o quote o Path.implode";
+toplevel_pp ["File", "ident"] "Pretty.str o quote o File.rep_ident";
 
-if String.isPrefix "polyml" ml_system then use "ML-Systems/install_pp_polyml.ML"
+if File.exists (Path.explode ("ML-Systems/install_pp_" ^ ml_system ^ ".ML"))
+then use ("ML-Systems/install_pp_" ^ ml_system ^ ".ML")
+else if String.isPrefix "polyml" ml_system
+then use "ML-Systems/install_pp_polyml.ML"
 else ();