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