# HG changeset patch
# User wenzelm
# Date 850727052 -3600
# Node ID f733d555b3d041c2568c3c6d44ab1413852d803f
# Parent  7becd4dd5ca7143245dbf0b3f029c0d9ac1b7461
added write_charnames';

diff -r 7becd4dd5ca7 -r f733d555b3d0 src/Pure/Syntax/symbol_font.ML
--- a/src/Pure/Syntax/symbol_font.ML	Mon Dec 16 10:03:30 1996 +0100
+++ b/src/Pure/Syntax/symbol_font.ML	Mon Dec 16 10:04:12 1996 +0100
@@ -10,7 +10,8 @@
   val char: string -> string option
   val name: string -> string option
   val read_charnames: string list -> string list
-  val write_charnames:  string list -> string list
+  val write_charnames:  string list -> string list	(*normal backslashes*)
+  val write_charnames':  string list -> string list	(*escaped backslashes*)
 end;
 
 
@@ -76,12 +77,13 @@
 
 (* write_charnames *)
 
-fun write_char ch =
+fun write_char prfx ch =
   (case name ch of
     None => ch
-  | Some nm => "\\<" ^ nm ^ ">");
+  | Some nm => prfx ^ "\\<" ^ nm ^ ">");
 
-val write_charnames = map write_char;
+val write_charnames = map (write_char "");
+val write_charnames' = map (write_char "\\");
 
 
 end;