src/Pure/Syntax/symbol_font.ML
changeset 2913 ce271fa4d8e2
parent 2769 77903c147673
child 2942 ada10e31bf66
     1.1 --- a/src/Pure/Syntax/symbol_font.ML	Fri Apr 04 16:33:28 1997 +0200
     1.2 +++ b/src/Pure/Syntax/symbol_font.ML	Fri Apr 04 19:07:54 1997 +0200
     1.3 @@ -11,8 +11,11 @@
     1.4    val char: string -> string option
     1.5    val name: string -> string option
     1.6    val read_charnames: string list -> string list
     1.7 -  val write_charnames:  string list -> string list	(*normal backslashes*)
     1.8 -  val write_charnames':  string list -> string list	(*escaped backslashes*)
     1.9 +  val read_chnames: string -> string
    1.10 +  val write_charnames: string list -> string list	(*normal backslashes*)
    1.11 +  val write_chnames: string -> string
    1.12 +  val write_charnames': string list -> string list	(*escaped backslashes*)
    1.13 +  val write_chnames': string -> string
    1.14  end;
    1.15  
    1.16  
    1.17 @@ -78,6 +81,8 @@
    1.18    fun read_charnames chs =
    1.19      if forall (not_equal "\\") chs then chs
    1.20      else #1 (repeat (scan_symbol || scan_one (K true)) chs);
    1.21 +
    1.22 +  val read_chnames = implode o read_charnames o explode;
    1.23  end;
    1.24  
    1.25  
    1.26 @@ -95,5 +100,7 @@
    1.27  val write_charnames = write_chars "";
    1.28  val write_charnames' = write_chars "\\";
    1.29  
    1.30 +val write_chnames = implode o write_charnames o explode;
    1.31 +val write_chnames' = implode o write_charnames' o explode;
    1.32  
    1.33  end;