equal
deleted
inserted
replaced
497 (** xsymbols **) |
497 (** xsymbols **) |
498 |
498 |
499 val xsymbolsN = "xsymbols"; |
499 val xsymbolsN = "xsymbols"; |
500 |
500 |
501 fun sym_len s = |
501 fun sym_len s = |
502 if not (is_printable s) then 0 |
502 if not (is_printable s) then (0: int) |
503 else if String.isPrefix "\\<long" s then 2 |
503 else if String.isPrefix "\\<long" s then 2 |
504 else if String.isPrefix "\\<Long" s then 2 |
504 else if String.isPrefix "\\<Long" s then 2 |
505 else if s = "\\<spacespace>" then 2 |
505 else if s = "\\<spacespace>" then 2 |
506 else 1; |
506 else 1; |
507 |
507 |