careful export of type-dependent functions, without losing their special status;
authorwenzelm
Sat Apr 02 21:10:07 2016 +0200 (2016-04-02 ago)
changeset 62819d3ff367a16a0
parent 62818 2733b240bfea
child 62820 5c678ee5d34a
careful export of type-dependent functions, without losing their special status;
Admin/polyml/future/ROOT.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/lazy.ML
src/Pure/Concurrent/synchronized.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/General/binding.ML
src/Pure/General/linear_set.ML
src/Pure/General/path.ML
src/Pure/General/pretty.ML
src/Pure/General/sha1.ML
src/Pure/General/table.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_compiler0.ML
src/Pure/ML/ml_debugger.ML
src/Pure/ML/ml_name_space.ML
src/Pure/ML/ml_pp.ML
src/Pure/ML/ml_pretty.ML
src/Pure/ML/ml_syntax.ML
src/Pure/PIDE/xml.ML
src/Pure/Syntax/ast.ML
src/Pure/Syntax/lexicon.ML
src/Pure/context.ML
src/Pure/morphism.ML
     1.1 --- a/Admin/polyml/future/ROOT.ML	Sat Apr 02 20:33:34 2016 +0200
     1.2 +++ b/Admin/polyml/future/ROOT.ML	Sat Apr 02 21:10:07 2016 +0200
     1.3 @@ -116,16 +116,16 @@
     1.4  use "Concurrent/mailbox.ML";
     1.5  use "Concurrent/cache.ML";
     1.6  
     1.7 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn var =>
     1.8 +ML_system_pp (fn depth => fn pretty => fn var =>
     1.9    pretty (Synchronized.value var, depth));
    1.10  
    1.11 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    1.12 +ML_system_pp (fn depth => fn pretty => fn x =>
    1.13    (case Future.peek x of
    1.14      NONE => PolyML.PrettyString "<future>"
    1.15    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
    1.16    | SOME (Exn.Res y) => pretty (y, depth)));
    1.17  
    1.18 -PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
    1.19 +ML_system_pp (fn depth => fn pretty => fn x =>
    1.20    (case Lazy.peek x of
    1.21      NONE => PolyML.PrettyString "<lazy>"
    1.22    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
     2.1 --- a/src/Pure/Concurrent/future.ML	Sat Apr 02 20:33:34 2016 +0200
     2.2 +++ b/src/Pure/Concurrent/future.ML	Sat Apr 02 21:10:07 2016 +0200
     2.3 @@ -100,7 +100,7 @@
     2.4  fun is_finished x = is_some (peek x);
     2.5  
     2.6  val _ =
     2.7 -  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
     2.8 +  ML_system_pp (fn depth => fn pretty => fn x =>
     2.9      (case peek x of
    2.10        NONE => PolyML.PrettyString "<future>"
    2.11      | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
     3.1 --- a/src/Pure/Concurrent/lazy.ML	Sat Apr 02 20:33:34 2016 +0200
     3.2 +++ b/src/Pure/Concurrent/lazy.ML	Sat Apr 02 21:10:07 2016 +0200
     3.3 @@ -103,7 +103,7 @@
     3.4  (* toplevel pretty printing *)
     3.5  
     3.6  val _ =
     3.7 -  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
     3.8 +  ML_system_pp (fn depth => fn pretty => fn x =>
     3.9      (case peek x of
    3.10        NONE => PolyML.PrettyString "<lazy>"
    3.11      | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
     4.1 --- a/src/Pure/Concurrent/synchronized.ML	Sat Apr 02 20:33:34 2016 +0200
     4.2 +++ b/src/Pure/Concurrent/synchronized.ML	Sat Apr 02 21:10:07 2016 +0200
     4.3 @@ -69,6 +69,6 @@
     4.4  
     4.5  (* toplevel pretty printing *)
     4.6  
     4.7 -val _ = PolyML.addPrettyPrinter (fn depth => fn pretty => fn var => pretty (value var, depth));
     4.8 +val _ = ML_system_pp (fn depth => fn pretty => fn var => pretty (value var, depth));
     4.9  
    4.10  end;
     5.1 --- a/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 20:33:34 2016 +0200
     5.2 +++ b/src/Pure/Concurrent/task_queue.ML	Sat Apr 02 21:10:07 2016 +0200
     5.3 @@ -397,7 +397,7 @@
     5.4  
     5.5  (* toplevel pretty printing *)
     5.6  
     5.7 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
     5.8 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
     5.9 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_task);
    5.10 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o str_of_group);
    5.11  
    5.12  end;
     6.1 --- a/src/Pure/General/binding.ML	Sat Apr 02 20:33:34 2016 +0200
     6.2 +++ b/src/Pure/General/binding.ML	Sat Apr 02 21:10:07 2016 +0200
     6.3 @@ -154,7 +154,7 @@
     6.4  
     6.5  val print = Pretty.unformatted_string_of o pretty;
     6.6  
     6.7 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
     6.8 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty o set_pos Position.none);
     6.9  
    6.10  
    6.11  (* check *)
     7.1 --- a/src/Pure/General/linear_set.ML	Sat Apr 02 20:33:34 2016 +0200
     7.2 +++ b/src/Pure/General/linear_set.ML	Sat Apr 02 21:10:07 2016 +0200
     7.3 @@ -136,11 +136,11 @@
     7.4  (* ML pretty-printing *)
     7.5  
     7.6  val _ =
     7.7 -  PolyML.addPrettyPrinter (fn depth => fn pretty => fn set =>
     7.8 +  ML_system_pp (fn depth => fn pretty => fn set =>
     7.9      ML_Pretty.to_polyml
    7.10        (ML_Pretty.enum "," "{" "}"
    7.11          (ML_Pretty.pair
    7.12 -          (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
    7.13 +          (ML_Pretty.from_polyml o ML_system_pretty)
    7.14            (ML_Pretty.from_polyml o pretty))
    7.15          (dest set, depth)));
    7.16  
     8.1 --- a/src/Pure/General/path.ML	Sat Apr 02 20:33:34 2016 +0200
     8.2 +++ b/src/Pure/General/path.ML	Sat Apr 02 21:10:07 2016 +0200
     8.3 @@ -173,7 +173,7 @@
     8.4  
     8.5  val print = Pretty.unformatted_string_of o pretty;
     8.6  
     8.7 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
     8.8 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
     8.9  
    8.10  
    8.11  (* base element *)
     9.1 --- a/src/Pure/General/pretty.ML	Sat Apr 02 20:33:34 2016 +0200
     9.2 +++ b/src/Pure/General/pretty.ML	Sat Apr 02 21:10:07 2016 +0200
     9.3 @@ -402,7 +402,7 @@
     9.4  
     9.5  end;
     9.6  
     9.7 -val _ = PolyML.addPrettyPrinter (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
     9.8 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
     9.9 +val _ = ML_system_pp (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
    9.10 +val _ = ML_system_pp (fn _ => fn _ => to_polyml o position);
    9.11  
    9.12  end;
    10.1 --- a/src/Pure/General/sha1.ML	Sat Apr 02 20:33:34 2016 +0200
    10.2 +++ b/src/Pure/General/sha1.ML	Sat Apr 02 21:10:07 2016 +0200
    10.3 @@ -182,7 +182,7 @@
    10.4  fun rep (Digest s) = s;
    10.5  val fake = Digest;
    10.6  
    10.7 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
    10.8 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Pretty.str o quote o rep);
    10.9  
   10.10  fun digest_string str = digest_string_external str
   10.11    handle CInterface.Foreign msg =>
    11.1 --- a/src/Pure/General/table.ML	Sat Apr 02 20:33:34 2016 +0200
    11.2 +++ b/src/Pure/General/table.ML	Sat Apr 02 21:10:07 2016 +0200
    11.3 @@ -411,11 +411,11 @@
    11.4  (* ML pretty-printing *)
    11.5  
    11.6  val _ =
    11.7 -  PolyML.addPrettyPrinter (fn depth => fn pretty => fn tab =>
    11.8 +  ML_system_pp (fn depth => fn pretty => fn tab =>
    11.9      ML_Pretty.to_polyml
   11.10        (ML_Pretty.enum "," "{" "}"
   11.11          (ML_Pretty.pair
   11.12 -          (ML_Pretty.from_polyml o PolyML.prettyRepresentation)
   11.13 +          (ML_Pretty.from_polyml o ML_system_pretty)
   11.14            (ML_Pretty.from_polyml o pretty))
   11.15          (dest tab, depth)));
   11.16  
    12.1 --- a/src/Pure/Isar/proof.ML	Sat Apr 02 20:33:34 2016 +0200
    12.2 +++ b/src/Pure/Isar/proof.ML	Sat Apr 02 21:10:07 2016 +0200
    12.3 @@ -174,7 +174,7 @@
    12.4        (context * thm list list -> context -> context)};
    12.5  
    12.6  val _ =
    12.7 -  PolyML.addPrettyPrinter (fn _ => fn _ => fn _: state =>
    12.8 +  ML_system_pp (fn _ => fn _ => fn _: state =>
    12.9      Pretty.to_polyml (Pretty.str "<Proof.state>"));
   12.10  
   12.11  fun make_goal (statement, using, goal, before_qed, after_qed) =
    13.1 --- a/src/Pure/Isar/runtime.ML	Sat Apr 02 20:33:34 2016 +0200
    13.2 +++ b/src/Pure/Isar/runtime.ML	Sat Apr 02 21:10:07 2016 +0200
    13.3 @@ -43,7 +43,7 @@
    13.4  fun pretty_exn (exn: exn) =
    13.5    Pretty.from_ML
    13.6      (ML_Pretty.from_polyml
    13.7 -      (PolyML.prettyRepresentation (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
    13.8 +      (ML_system_pretty (exn, FixedInt.fromInt (ML_Options.get_print_depth ()))));
    13.9  
   13.10  
   13.11  (* exn_context *)
    14.1 --- a/src/Pure/Isar/toplevel.ML	Sat Apr 02 20:33:34 2016 +0200
    14.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Apr 02 21:10:07 2016 +0200
    14.3 @@ -199,7 +199,7 @@
    14.4  
    14.5  fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
    14.6  
    14.7 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
    14.8 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_abstract);
    14.9  
   14.10  
   14.11  
    15.1 --- a/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 20:33:34 2016 +0200
    15.2 +++ b/src/Pure/ML/ml_compiler0.ML	Sat Apr 02 21:10:07 2016 +0200
    15.3 @@ -139,3 +139,15 @@
    15.4          {verbose = true, debug = ML_Compiler0.debug_option opt_debug} file
    15.5        handle ERROR msg => (#print context msg; raise error "ML error"))
    15.6    end;
    15.7 +
    15.8 +
    15.9 +(* export type-dependent functions *)
   15.10 +
   15.11 +ML_Compiler0.use_text
   15.12 +  (ML_Compiler0.make_context
   15.13 +    (ML_Name_Space.global_values
   15.14 +      [("prettyRepresentation", "ML_system_pretty"),
   15.15 +       ("addPrettyPrinter", "ML_system_pp"),
   15.16 +       ("addOverload", "ML_system_overload")]))
   15.17 +  {debug = false, file = "", line = 0, verbose = false}
   15.18 +  "open PolyML RunCall";
    16.1 --- a/src/Pure/ML/ml_debugger.ML	Sat Apr 02 20:33:34 2016 +0200
    16.2 +++ b/src/Pure/ML/ml_debugger.ML	Sat Apr 02 21:10:07 2016 +0200
    16.3 @@ -42,7 +42,7 @@
    16.4  end;
    16.5  
    16.6  val _ =
    16.7 -  PolyML.addPrettyPrinter (fn _ => fn _ => fn exn_id =>
    16.8 +  ML_system_pp (fn _ => fn _ => fn exn_id =>
    16.9      let val s = print_exn_id exn_id
   16.10      in ML_Pretty.to_polyml (ML_Pretty.String (s, FixedInt.fromInt (size s))) end);
   16.11  
    17.1 --- a/src/Pure/ML/ml_name_space.ML	Sat Apr 02 20:33:34 2016 +0200
    17.2 +++ b/src/Pure/ML/ml_name_space.ML	Sat Apr 02 21:10:07 2016 +0200
    17.3 @@ -11,7 +11,31 @@
    17.4    open PolyML.NameSpace;
    17.5  
    17.6    type T = PolyML.NameSpace.nameSpace;
    17.7 +
    17.8    val global = PolyML.globalNameSpace;
    17.9 +  fun global_values values : T =
   17.10 +   {lookupVal = #lookupVal global,
   17.11 +    lookupType = #lookupType global,
   17.12 +    lookupStruct = #lookupStruct global,
   17.13 +    lookupFix = #lookupFix global,
   17.14 +    lookupSig = #lookupSig global,
   17.15 +    lookupFunct = #lookupFunct global,
   17.16 +    enterVal =
   17.17 +      fn (x, value) =>
   17.18 +        (case List.find (fn (y, _) => x = y) values of
   17.19 +          SOME (_, x') => #enterVal global (x', value)
   17.20 +        | NONE => ()),
   17.21 +    enterType = fn _ => (),
   17.22 +    enterFix = fn _ => (),
   17.23 +    enterStruct = fn _ => (),
   17.24 +    enterSig = fn _ => (),
   17.25 +    enterFunct = fn _ => (),
   17.26 +    allVal = #allVal global,
   17.27 +    allType = #allType global,
   17.28 +    allFix = #allFix global,
   17.29 +    allStruct = #allStruct global,
   17.30 +    allSig = #allSig global,
   17.31 +    allFunct = #allFunct global};
   17.32  
   17.33    type valueVal = Values.value;
   17.34    fun displayVal (x, depth, space) = Values.printWithType (x, depth, SOME space);
    18.1 --- a/src/Pure/ML/ml_pp.ML	Sat Apr 02 20:33:34 2016 +0200
    18.2 +++ b/src/Pure/ML/ml_pp.ML	Sat Apr 02 21:10:07 2016 +0200
    18.3 @@ -8,22 +8,22 @@
    18.4  struct
    18.5  
    18.6  val _ =
    18.7 -  PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
    18.8 +  ML_system_pp (fn _ => fn _ => Pretty.to_polyml o Proof_Display.pp_context);
    18.9  
   18.10  val _ =
   18.11 -  PolyML.addPrettyPrinter (fn depth => fn _ =>
   18.12 +  ML_system_pp (fn depth => fn _ =>
   18.13      ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_thm Thy_Info.pure_theory);
   18.14  
   18.15  val _ =
   18.16 -  PolyML.addPrettyPrinter (fn depth => fn _ =>
   18.17 +  ML_system_pp (fn depth => fn _ =>
   18.18      ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_cterm Thy_Info.pure_theory);
   18.19  
   18.20  val _ =
   18.21 -  PolyML.addPrettyPrinter (fn depth => fn _ =>
   18.22 +  ML_system_pp (fn depth => fn _ =>
   18.23      ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_ctyp Thy_Info.pure_theory);
   18.24  
   18.25  val _ =
   18.26 -  PolyML.addPrettyPrinter (fn depth => fn _ =>
   18.27 +  ML_system_pp (fn depth => fn _ =>
   18.28      ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Thy_Info.pure_theory);
   18.29  
   18.30  
   18.31 @@ -43,17 +43,17 @@
   18.32          |> (if parens then Pretty.enclose "(" ")" else Pretty.block)
   18.33      | Abs (a, T, b) =>
   18.34          prt_apps "Abs"
   18.35 -         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
   18.36 -          Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
   18.37 +         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
   18.38 +          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
   18.39            prt_term false (dp - 3) b]
   18.40 -    | Const a => prt_app "Const" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
   18.41 -    | Free a => prt_app "Free" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
   18.42 -    | Var a => prt_app "Var" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
   18.43 -    | Bound a => prt_app "Bound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))));
   18.44 +    | Const a => prt_app "Const" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
   18.45 +    | Free a => prt_app "Free" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
   18.46 +    | Var a => prt_app "Var" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
   18.47 +    | Bound a => prt_app "Bound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))));
   18.48  
   18.49  in
   18.50  
   18.51 -val _ = PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
   18.52 +val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o prt_term false depth);
   18.53  
   18.54  
   18.55  local
   18.56 @@ -66,22 +66,22 @@
   18.57      | _ %% _ => prt_proofs parens dp prf
   18.58      | Abst (a, T, b) =>
   18.59          prt_apps "Abst"
   18.60 -         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
   18.61 -          Pretty.from_polyml (PolyML.prettyRepresentation (T, dp - 2)),
   18.62 +         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
   18.63 +          Pretty.from_polyml (ML_system_pretty (T, dp - 2)),
   18.64            prt_proof false (dp - 3) b]
   18.65      | AbsP (a, t, b) =>
   18.66          prt_apps "AbsP"
   18.67 -         [Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)),
   18.68 -          Pretty.from_polyml (PolyML.prettyRepresentation (t, dp - 2)),
   18.69 +         [Pretty.from_polyml (ML_system_pretty (a, dp - 1)),
   18.70 +          Pretty.from_polyml (ML_system_pretty (t, dp - 2)),
   18.71            prt_proof false (dp - 3) b]
   18.72      | Hyp t => prt_app "Hyp" (prt_term true (dp - 1) t)
   18.73      | MinProof => Pretty.str "MinProof"
   18.74 -    | PBound a => prt_app "PBound" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
   18.75 -    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
   18.76 -    | OfClass a => prt_app "OfClass" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
   18.77 -    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
   18.78 -    | Promise a => prt_app "Promise" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1)))
   18.79 -    | PThm a => prt_app "PThm" (Pretty.from_polyml (PolyML.prettyRepresentation (a, dp - 1))))
   18.80 +    | PBound a => prt_app "PBound" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
   18.81 +    | PAxm a => prt_app "PAxm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
   18.82 +    | OfClass a => prt_app "OfClass" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
   18.83 +    | Oracle a => prt_app "Oracle" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
   18.84 +    | Promise a => prt_app "Promise" (Pretty.from_polyml (ML_system_pretty (a, dp - 1)))
   18.85 +    | PThm a => prt_app "PThm" (Pretty.from_polyml (ML_system_pretty (a, dp - 1))))
   18.86  
   18.87  and prt_proofs parens dp prf =
   18.88    let
   18.89 @@ -94,7 +94,7 @@
   18.90        strip_proof p
   18.91          ((fn d =>
   18.92            [Pretty.str " %", Pretty.brk 1,
   18.93 -            Pretty.from_polyml (PolyML.prettyRepresentation (t, d))]) :: res)
   18.94 +            Pretty.from_polyml (ML_system_pretty (t, d))]) :: res)
   18.95    | strip_proof (p %% q) res =
   18.96        strip_proof p ((fn d => [Pretty.str " %%", Pretty.brk 1, prt_proof true d q]) :: res)
   18.97    | strip_proof p res = (fn d => prt_proof true d p, res);
   18.98 @@ -102,7 +102,7 @@
   18.99  in
  18.100  
  18.101  val _ =
  18.102 -  PolyML.addPrettyPrinter (fn depth => fn _ => fn prf =>
  18.103 +  ML_system_pp (fn depth => fn _ => fn prf =>
  18.104      ML_Pretty.to_polyml (Pretty.to_ML ~1 (prt_proof false depth prf)));
  18.105  
  18.106  end;
    19.1 --- a/src/Pure/ML/ml_pretty.ML	Sat Apr 02 20:33:34 2016 +0200
    19.2 +++ b/src/Pure/ML/ml_pretty.ML	Sat Apr 02 21:10:07 2016 +0200
    19.3 @@ -116,7 +116,7 @@
    19.4  
    19.5  local
    19.6    fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
    19.7 -  fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
    19.8 +  fun pretty_value depth = "ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))";
    19.9  in
   19.10  
   19.11  fun make_string_fn local_env =
    20.1 --- a/src/Pure/ML/ml_syntax.ML	Sat Apr 02 20:33:34 2016 +0200
    20.2 +++ b/src/Pure/ML/ml_syntax.ML	Sat Apr 02 21:10:07 2016 +0200
    20.3 @@ -124,7 +124,7 @@
    20.4    in Pretty.str (quote (implode (map print_char body'))) end;
    20.5  
    20.6  val _ =
    20.7 -  PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
    20.8 +  ML_system_pp (fn depth => fn _ => fn str =>
    20.9      Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
   20.10  
   20.11  end;
    21.1 --- a/src/Pure/PIDE/xml.ML	Sat Apr 02 20:33:34 2016 +0200
    21.2 +++ b/src/Pure/PIDE/xml.ML	Sat Apr 02 21:10:07 2016 +0200
    21.3 @@ -170,8 +170,7 @@
    21.4  fun pretty depth tree =
    21.5    Pretty.str (Buffer.content (buffer_of (Int.max (0, depth)) tree));
    21.6  
    21.7 -val _ =
    21.8 -  PolyML.addPrettyPrinter (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
    21.9 +val _ = ML_system_pp (fn depth => fn _ => Pretty.to_polyml o pretty (FixedInt.toInt depth));
   21.10  
   21.11  
   21.12  
    22.1 --- a/src/Pure/Syntax/ast.ML	Sat Apr 02 20:33:34 2016 +0200
    22.2 +++ b/src/Pure/Syntax/ast.ML	Sat Apr 02 21:10:07 2016 +0200
    22.3 @@ -66,7 +66,7 @@
    22.4  fun pretty_rule (lhs, rhs) =
    22.5    Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
    22.6  
    22.7 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
    22.8 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_ast);
    22.9  
   22.10  
   22.11  (* strip_positions *)
    23.1 --- a/src/Pure/Syntax/lexicon.ML	Sat Apr 02 20:33:34 2016 +0200
    23.2 +++ b/src/Pure/Syntax/lexicon.ML	Sat Apr 02 21:10:07 2016 +0200
    23.3 @@ -451,7 +451,7 @@
    23.4  (* toplevel pretty printing *)
    23.5  
    23.6  val _ =
    23.7 -  PolyML.addPrettyPrinter (fn _ => fn _ =>
    23.8 +  ML_system_pp (fn _ => fn _ =>
    23.9      Pretty.to_polyml o Pretty.str_list "{" "}" o map quote o Scan.dest_lexicon);
   23.10  
   23.11  end;
    24.1 --- a/src/Pure/context.ML	Sat Apr 02 20:33:34 2016 +0200
    24.2 +++ b/src/Pure/context.ML	Sat Apr 02 21:10:07 2016 +0200
    24.3 @@ -169,7 +169,7 @@
    24.4  
    24.5  val pretty_thy = Pretty.str_list "{" "}" o display_names;
    24.6  
    24.7 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
    24.8 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
    24.9  
   24.10  fun pretty_abbrev_thy thy =
   24.11    let
    25.1 --- a/src/Pure/morphism.ML	Sat Apr 02 20:33:34 2016 +0200
    25.2 +++ b/src/Pure/morphism.ML	Sat Apr 02 21:10:07 2016 +0200
    25.3 @@ -71,7 +71,7 @@
    25.4  
    25.5  fun pretty (Morphism {names, ...}) = Pretty.enum ";" "{" "}" (map Pretty.str (rev names));
    25.6  
    25.7 -val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty);
    25.8 +val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty);
    25.9  
   25.10  fun binding (Morphism {binding, ...}) = apply binding;
   25.11  fun typ (Morphism {typ, ...}) = apply typ;