src/Pure/ML/ml_pretty.ML
changeset 62663 bea354f6ff21
parent 62662 291cc01f56f5
child 62672 068b430e678f
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
   112 
   112 
   113 
   113 
   114 (* make string *)
   114 (* make string *)
   115 
   115 
   116 local
   116 local
   117   fun pretty_string_of s =
   117   fun pretty_string_of s = "(fn x => Pretty.string_of (Pretty.from_polyml (" ^ s ^ ")))";
   118     "(fn x => Pretty.string_of (Pretty.from_ML (ML_Pretty.from_polyml (" ^ s ^ "))))";
       
   119   fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
   118   fun pretty_value depth = "PolyML.prettyRepresentation (x, FixedInt.fromInt (" ^ depth ^ "))";
   120 in
   119 in
   121 
   120 
   122 fun make_string_fn local_env =
   121 fun make_string_fn local_env =
   123   if local_env <> "" then
   122   if local_env <> "" then