# HG changeset patch
# User wenzelm
# Date 1237661925 -3600
# Node ID 248de8dd839e19330902f4abd20f2ce0938f14cd
# Parent  d53d1a16d5eed8047fe4737dff85bb50e1468e70
adapted toplevel_pp to ML_Pretty.pretty;

diff -r d53d1a16d5ee -r 248de8dd839e src/Pure/ML-Systems/polyml-experimental.ML
--- a/src/Pure/ML-Systems/polyml-experimental.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/ML-Systems/polyml-experimental.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -12,19 +12,6 @@
 fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;
 
 
-(* toplevel pretty printers *)
-
-structure ML_Pretty =
-struct
-  datatype context = datatype PolyML.context;
-  datatype pretty = datatype PolyML.pretty;
-end;
-
-(*dummy version*)
-fun make_pp path pprint = ();
-fun install_pp _ = ();
-
-
 (* runtime compilation *)
 
 structure ML_NameSpace =
@@ -81,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 d53d1a16d5ee -r 248de8dd839e src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sat Mar 21 19:58:45 2009 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Sat Mar 21 19:58:45 2009 +0100
@@ -98,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 =
@@ -145,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 **)