1 (* Title: Pure/section-utils |
1 (* Title: Pure/section-utils |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Utilities for writing new theory sections |
6 Utilities for writing new theory sections |
7 *) |
7 *) |
8 |
8 |
47 |
47 |
48 (*Apply string escapes to a quoted string; see Def of Standard ML, page 3 |
48 (*Apply string escapes to a quoted string; see Def of Standard ML, page 3 |
49 Does not handle the \ddd form; no error checking*) |
49 Does not handle the \ddd form; no error checking*) |
50 fun escape [] = [] |
50 fun escape [] = [] |
51 | escape cs = (case take_prefix (not o is_backslash) cs of |
51 | escape cs = (case take_prefix (not o is_backslash) cs of |
52 (front, []) => front |
52 (front, []) => front |
53 | (front, _::"n"::rest) => front @ ("\n" :: escape rest) |
53 | (front, _::"n"::rest) => front @ ("\n" :: escape rest) |
54 | (front, _::"t"::rest) => front @ ("\t" :: escape rest) |
54 | (front, _::"t"::rest) => front @ ("\t" :: escape rest) |
55 | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest) |
55 | (front, _::"^"::c::rest) => front @ (chr(ord(c)-64) :: escape rest) |
56 | (front, _::"\""::rest) => front @ ("\"" :: escape rest) |
56 | (front, _::"\""::rest) => front @ ("\"" :: escape rest) |
57 | (front, _::"\\"::rest) => front @ ("\\" :: escape rest) |
57 | (front, _::"\\"::rest) => front @ ("\\" :: escape rest) |
58 | (front, b::c::rest) => |
58 | (front, b::c::rest) => |
59 if is_blank c (*remove any further blanks and the following \ *) |
59 if is_blank c (*remove any further blanks and the following \ *) |
60 then front @ escape (tl (snd (take_prefix is_blank rest))) |
60 then front @ escape (tl (snd (take_prefix is_blank rest))) |
61 else error ("Unrecognized string escape: " ^ implode(b::c::rest))); |
61 else error ("Unrecognized string escape: " ^ implode(b::c::rest))); |
62 |
62 |
63 (*Remove the first and last charaters -- presumed to be quotes*) |
63 (*Remove the first and last charaters -- presumed to be quotes*) |
64 val trim = implode o escape o rev o tl o rev o tl o explode; |
64 val trim = implode o escape o rev o tl o rev o tl o explode; |
65 |
65 |
66 |
66 |