equal
deleted
inserted
replaced
503 fun readable_name full_name s = |
503 fun readable_name full_name s = |
504 if s = full_name then |
504 if s = full_name then |
505 s |
505 s |
506 else |
506 else |
507 s |> no_qualifiers |
507 s |> no_qualifiers |
|
508 |> perhaps (try (unprefix "'")) |
508 |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) |
509 |> Name.desymbolize (Char.isUpper (String.sub (full_name, 0))) |
509 |> (fn s => |
510 |> (fn s => |
510 if size s > max_readable_name_size then |
511 if size s > max_readable_name_size then |
511 String.substring (s, 0, max_readable_name_size div 2 - 4) ^ |
512 String.substring (s, 0, max_readable_name_size div 2 - 4) ^ |
512 string_of_int (hash_string full_name) ^ |
513 string_of_int (hash_string full_name) ^ |
526 let |
527 let |
527 val nice_prefix = readable_name full_name desired_name |
528 val nice_prefix = readable_name full_name desired_name |
528 fun add j = |
529 fun add j = |
529 let |
530 let |
530 val nice_name = |
531 val nice_name = |
531 nice_prefix ^ (if j = 0 then "" else "_" ^ string_of_int j) |
532 nice_prefix ^ (if j = 0 then "" else string_of_int j) |
532 in |
533 in |
533 case Symtab.lookup (snd the_pool) nice_name of |
534 case Symtab.lookup (snd the_pool) nice_name of |
534 SOME full_name' => |
535 SOME full_name' => |
535 if full_name = full_name' then (nice_name, the_pool) |
536 if full_name = full_name' then (nice_name, the_pool) |
536 else add (j + 1) |
537 else add (j + 1) |