# HG changeset patch
# User wenzelm
# Date 850736195 -3600
# Node ID 98a571307d5ee479089bf430a6f4b267afd2baab
# Parent  6b6a92d05fb24cfbf9bfd5b7ec94cf5ef37bd505
tuned read and write functions;

diff -r 6b6a92d05fb2 -r 98a571307d5e src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Mon Dec 16 11:13:44 1996 +0100
+++ b/src/Pure/Syntax/symbol_font.ML	Mon Dec 16 12:36:35 1996 +0100
@@ -51,7 +51,10 @@
 (* chars and names *)
 
 fun char name = Symtab.lookup (enc_tab, name);
-fun name char = Symtab.lookup (dec_tab, char);
+
+fun name char =
+  if ord char < enc_start then None
+  else Symtab.lookup (dec_tab, char);
 
 
 
@@ -71,7 +74,9 @@
         in (c, cs') end
     | scan_symbol _ = raise LEXICAL_ERROR;
 in
-  val read_charnames = #1 o repeat (scan_symbol || scan_one (K true));
+  fun read_charnames chs =
+    if forall (not_equal "\\") chs then chs
+    else #1 (repeat (scan_symbol || scan_one (K true)) chs);
 end;
 
 
@@ -82,8 +87,12 @@
     None => ch
   | Some nm => prfx ^ "\\<" ^ nm ^ ">");
 
-val write_charnames = map (write_char "");
-val write_charnames' = map (write_char "\\");
+fun write_chars prfx chs =
+  if forall (fn ch => ord ch < enc_start) chs then chs
+  else map (write_char prfx) chs;
+
+val write_charnames = write_chars "";
+val write_charnames' = write_chars "\\";
 
 
 end;