src/Pure/ML/ml_syntax.ML
changeset 62663 bea354f6ff21
parent 62528 c8c532b22947
child 62819 d3ff367a16a0
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
   121     val body' =
   121     val body' =
   122       if length body <= max_len then body
   122       if length body <= max_len then body
   123       else take (Int.max (max_len, 0)) body @ ["..."];
   123       else take (Int.max (max_len, 0)) body @ ["..."];
   124   in Pretty.str (quote (implode (map print_char body'))) end;
   124   in Pretty.str (quote (implode (map print_char body'))) end;
   125 
   125 
       
   126 val _ =
       
   127   PolyML.addPrettyPrinter (fn depth => fn _ => fn str =>
       
   128     Pretty.to_polyml (pretty_string (FixedInt.toInt (depth * 100)) str));
       
   129 
   126 end;
   130 end;