src/Pure/General/pretty.ML
changeset 62672 068b430e678f
parent 62667 254582abf067
child 62783 75ee05386b90
equal deleted inserted replaced
62671:a9ee1f240b81 62672:068b430e678f
   392 val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
   392 val to_polyml = to_ML ~1 #> ML_Pretty.to_polyml;
   393 val from_polyml = ML_Pretty.from_polyml #> from_ML;
   393 val from_polyml = ML_Pretty.from_polyml #> from_ML;
   394 
   394 
   395 end;
   395 end;
   396 
   396 
   397 val _ =
   397 val _ = PolyML.addPrettyPrinter (fn d => fn _ => ML_Pretty.to_polyml o to_ML (d + 1) o quote);
   398   PolyML.addPrettyPrinter (fn depth => fn _ => ML_Pretty.to_polyml o to_ML (depth * 2 + 1) o quote);
       
   399 
       
   400 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
   398 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => to_polyml o position);
   401 
   399 
   402 end;
   400 end;