equal
deleted
inserted
replaced
28 val is_ascii_quasi: symbol -> bool |
28 val is_ascii_quasi: symbol -> bool |
29 val is_ascii_blank: symbol -> bool |
29 val is_ascii_blank: symbol -> bool |
30 val is_raw: symbol -> bool |
30 val is_raw: symbol -> bool |
31 val decode_raw: symbol -> string |
31 val decode_raw: symbol -> string |
32 val encode_raw: string -> symbol list |
32 val encode_raw: string -> symbol list |
|
33 datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string |
|
34 exception DECODE of string |
|
35 val decode: symbol -> sym |
33 datatype kind = Letter | Digit | Quasi | Blank | Other |
36 datatype kind = Letter | Digit | Quasi | Blank | Other |
34 val kind: symbol -> kind |
37 val kind: symbol -> kind |
35 val is_letter: symbol -> bool |
38 val is_letter: symbol -> bool |
36 val is_digit: symbol -> bool |
39 val is_digit: symbol -> bool |
37 val is_quasi: symbol -> bool |
40 val is_quasi: symbol -> bool |
162 fun encode_raw s = |
165 fun encode_raw s = |
163 if exists_string (not o raw_chr) s then encode (explode s) |
166 if exists_string (not o raw_chr) s then encode (explode s) |
164 else [enclose "\\<^raw:" ">" s]; |
167 else [enclose "\\<^raw:" ">" s]; |
165 |
168 |
166 end; |
169 end; |
|
170 |
|
171 |
|
172 (* symbol variants *) |
|
173 |
|
174 datatype sym = Char of string | Sym of string | Ctrl of string | Raw of string; |
|
175 |
|
176 exception DECODE of string; |
|
177 |
|
178 fun decode s = |
|
179 if is_char s then Char s |
|
180 else if is_raw s then Raw (decode_raw s) |
|
181 else if String.isPrefix "\\<^" s then Ctrl (String.substring (s, 3, size s - 4)) |
|
182 else if String.isPrefix "\\<" s then Sym (String.substring (s, 2, size s - 3)) |
|
183 else raise DECODE s; (*NB: no error message in order to avoid looping in output!*) |
167 |
184 |
168 |
185 |
169 (* standard symbol kinds *) |
186 (* standard symbol kinds *) |
170 |
187 |
171 datatype kind = Letter | Digit | Quasi | Blank | Other; |
188 datatype kind = Letter | Digit | Quasi | Blank | Other; |