equal
deleted
inserted
replaced
497 else if String.isPrefix "\\<long" s then 2 |
497 else if String.isPrefix "\\<long" s then 2 |
498 else if String.isPrefix "\\<Long" s then 2 |
498 else if String.isPrefix "\\<Long" s then 2 |
499 else if s = "\\<spacespace>" then 2 |
499 else if s = "\\<spacespace>" then 2 |
500 else 1; |
500 else 1; |
501 |
501 |
502 fun sym_length ss = Library.foldl (fn (n, s) => sym_len s + n) (0, ss); |
502 fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0; |
503 |
503 |
504 fun symbol_output str = |
504 fun symbol_output str = |
505 if chars_only str then default_output str |
505 if chars_only str then default_output str |
506 else |
506 else |
507 let |
507 let |