equal
deleted
inserted
replaced
8 signature SYMBOL_FONT = |
8 signature SYMBOL_FONT = |
9 sig |
9 sig |
10 val char: string -> string option |
10 val char: string -> string option |
11 val name: string -> string option |
11 val name: string -> string option |
12 val read_charnames: string list -> string list |
12 val read_charnames: string list -> string list |
13 val write_charnames: string list -> string list |
13 val write_charnames: string list -> string list (*normal backslashes*) |
|
14 val write_charnames': string list -> string list (*escaped backslashes*) |
14 end; |
15 end; |
15 |
16 |
16 |
17 |
17 structure SymbolFont : SYMBOL_FONT = |
18 structure SymbolFont : SYMBOL_FONT = |
18 struct |
19 struct |
74 end; |
75 end; |
75 |
76 |
76 |
77 |
77 (* write_charnames *) |
78 (* write_charnames *) |
78 |
79 |
79 fun write_char ch = |
80 fun write_char prfx ch = |
80 (case name ch of |
81 (case name ch of |
81 None => ch |
82 None => ch |
82 | Some nm => "\\<" ^ nm ^ ">"); |
83 | Some nm => prfx ^ "\\<" ^ nm ^ ">"); |
83 |
84 |
84 val write_charnames = map write_char; |
85 val write_charnames = map (write_char ""); |
|
86 val write_charnames' = map (write_char "\\"); |
85 |
87 |
86 |
88 |
87 end; |
89 end; |