--- 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 ^ "))");
+
--- 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 **)