equal
deleted
inserted
replaced
977 let |
977 let |
978 val idx = string_of_int i; |
978 val idx = string_of_int i; |
979 val dot = |
979 val dot = |
980 (case rev (Symbol.explode x) of |
980 (case rev (Symbol.explode x) of |
981 _ :: "\\<^sub>" :: _ => false |
981 _ :: "\\<^sub>" :: _ => false |
982 | _ :: "\\<^isub>" :: _ => false |
982 | _ :: "\\<^isub>" :: _ => false (*legacy*) |
|
983 | _ :: "\\<^isup>" :: _ => false (*legacy*) |
983 | c :: _ => Symbol.is_digit c |
984 | c :: _ => Symbol.is_digit c |
984 | _ => true); |
985 | _ => true); |
985 in |
986 in |
986 if dot then "?" ^ x ^ "." ^ idx |
987 if dot then "?" ^ x ^ "." ^ idx |
987 else if i <> 0 then "?" ^ x ^ idx |
988 else if i <> 0 then "?" ^ x ^ idx |