equal
deleted
inserted
replaced
114 |
114 |
115 (* make string *) |
115 (* make string *) |
116 |
116 |
117 local |
117 local |
118 fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))"; |
118 fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))"; |
119 fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))"; |
119 fun pretty_value depth = "ML_system_pretty (x, FixedInt.fromInt (" ^ depth ^ "))"; |
120 in |
120 in |
121 |
121 |
122 fun make_string_fn local_env = |
122 fun make_string_fn local_env = |
123 if local_env <> "" then |
123 if local_env <> "" then |
124 pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()")) |
124 pretty_string_of (pretty_value (local_env ^ ".ML_print_depth ()")) |