--- a/src/Pure/Syntax/symbol_font.ML Tue Dec 10 12:51:06 1996 +0100
+++ b/src/Pure/Syntax/symbol_font.ML Tue Dec 10 12:55:00 1996 +0100
@@ -7,14 +7,20 @@
signature SYMBOL_FONT =
sig
- val char_names: string list
val char: string -> string option
+ val name: string -> string option
+ val read_charnames: string list -> string list
+ val write_charnames: string list -> string list
end;
+
structure SymbolFont : SYMBOL_FONT =
struct
-(** the encoding vector **)
+
+(** font encoding vector **)
+
+(* tables *)
val enc_start = 161;
val enc_end = 255;
@@ -35,13 +41,47 @@
"infinity", "box", "diamond", "circ", "bullet", "parallel", "tick", "copyright"
];
-val enc_tab = Symtab.make (enc_vector ~~ (enc_start upto enc_end));
+val enc_rel = enc_vector ~~ (map chr (enc_start upto enc_end));
+
+val enc_tab = Symtab.make enc_rel;
+val dec_tab = Symtab.make (map swap enc_rel);
+
+
+(* chars and names *)
+
+fun char name = Symtab.lookup (enc_tab, name);
+fun name char = Symtab.lookup (dec_tab, char);
+
-(** chars by name **)
+(** input and output of symbols **)
+
+(* read_charnames *)
+
+local
+ open Scanner;
-val char_names = enc_vector;
+ fun scan_symbol ("\\" :: "<" :: cs) =
+ let
+ val (name, cs') = (scan_id -- $$ ">" >> #1) cs handle LEXICAL_ERROR
+ => error ("Malformed symbolic char specification: \"\\<" ^ implode cs ^ "\"");
+ val c = the (char name) handle OPTION _
+ => error ("Unknown symbolic char name: " ^ quote name);
+ in (c, cs') end
+ | scan_symbol _ = raise LEXICAL_ERROR;
+in
+ val read_charnames = #1 o repeat (scan_symbol || scan_one (K true));
+end;
-fun char name = apsome chr (Symtab.lookup (enc_tab, name));
+
+(* write_charnames *)
+
+fun write_char ch =
+ (case name ch of
+ None => ch
+ | Some nm => "\\<" ^ nm ^ ">");
+
+val write_charnames = map write_char;
+
end;