# HG changeset patch
# User wenzelm
# Date 850218900 -3600
# Node ID 4744b27cdf895f6c61cd22dcec959d47d0294a56
# Parent  74c99949ad84c898f7e8b0924b3093db20aac8fc
added read_charnames, write_charnames;

diff -r 74c99949ad84 -r 4744b27cdf89 src/Pure/Syntax/symbol_font.ML
--- 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;