src/Pure/context.ML
changeset 62663 bea354f6ff21
parent 61878 fa4dbb82732f
child 62819 d3ff367a16a0
equal deleted inserted replaced
62662:291cc01f56f5 62663:bea354f6ff21
   167     val ancestor_names = map theory_name (ancestors_of thy);
   167     val ancestor_names = map theory_name (ancestors_of thy);
   168   in rev (name :: ancestor_names) end;
   168   in rev (name :: ancestor_names) end;
   169 
   169 
   170 val pretty_thy = Pretty.str_list "{" "}" o display_names;
   170 val pretty_thy = Pretty.str_list "{" "}" o display_names;
   171 
   171 
       
   172 val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_thy);
       
   173 
   172 fun pretty_abbrev_thy thy =
   174 fun pretty_abbrev_thy thy =
   173   let
   175   let
   174     val names = display_names thy;
   176     val names = display_names thy;
   175     val n = length names;
   177     val n = length names;
   176     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;
   178     val abbrev = if n > 5 then "..." :: List.drop (names, n - 5) else names;