equal
deleted
inserted
replaced
783 fun avoid_clash_with_dfg_keywords s = |
783 fun avoid_clash_with_dfg_keywords s = |
784 let val n = String.size s in |
784 let val n = String.size s in |
785 if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse |
785 if n < 2 orelse (n = 2 andalso String.sub (s, 0) = String.sub (s, 1)) orelse |
786 String.isSubstring "_" s then |
786 String.isSubstring "_" s then |
787 s |
787 s |
|
788 else if s = "Dl" orelse s = "DL" then |
|
789 (* "DL" appears to be a SPASS 3.7 keyword *) |
|
790 s ^ "_" |
788 else |
791 else |
789 String.substring (s, 0, n - 1) ^ |
792 String.substring (s, 0, n - 1) ^ |
790 String.str (Char.toUpper (String.sub (s, n - 1))) |
793 String.str (Char.toUpper (String.sub (s, n - 1))) |
791 end |
794 end |
792 |
795 |