755 val oct_char = chr o octal; |
755 val oct_char = chr o octal; |
756 |
756 |
757 |
757 |
758 (*** Printing ***) |
758 (*** Printing ***) |
759 |
759 |
760 (*Makes a variant of the name c distinct from the names in bs. |
760 (*Makes a variant of a name distinct from the names in bs. |
761 First attaches the suffix "a" and then increments this; |
761 First attaches the suffix and then increments this; |
762 preserves a suffix of underscores "_". *) |
762 preserves a suffix of underscores "_". *) |
763 fun variant bs name = |
763 fun variant bs name = |
764 let |
764 let |
765 val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name)); |
765 val (c, u) = pairself implode (Library.take_suffix (equal "_") (Symbol.explode name)); |
766 fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c; |
766 fun vary2 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_string c) else c; |
767 fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (c ^ "a") else c; |
767 fun vary1 c = if ((c ^ u) mem_string bs) then vary2 (Symbol.bump_init c) else c; |
768 in vary1 (if c = "" then "u" else c) ^ u end; |
768 in vary1 (if c = "" then "u" else c) ^ u end; |
769 |
769 |
770 (*Create variants of the list of names, with priority to the first ones*) |
770 (*Create variants of the list of names, with priority to the first ones*) |
771 fun variantlist ([], used) = [] |
771 fun variantlist ([], used) = [] |
772 | variantlist(b::bs, used) = |
772 | variantlist(b::bs, used) = |