equal
deleted
inserted
replaced
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; |