# 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 **)