equal
deleted
inserted
replaced
53 val tab_width = (8: int); |
53 val tab_width = (8: int); |
54 |
54 |
55 fun untabify ("\t", pos) = |
55 fun untabify ("\t", pos) = |
56 (case Position.column_of pos of |
56 (case Position.column_of pos of |
57 SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width)) |
57 SOME n => Symbol.spaces (tab_width - ((n - 1) mod tab_width)) |
58 | NONE => error "No column information -- cannot interpret tabulators") |
58 | NONE => Symbol.space) |
59 | untabify (s, _) = s; |
59 | untabify (s, _) = s; |
60 |
60 |
61 val untabify_content = implode o map untabify; |
61 val untabify_content = implode o map untabify; |
62 |
62 |
63 |
63 |