# HG changeset patch
# User wenzelm
# Date 1353441713 -3600
# Node ID d5132bba6a831c38282c982aaa5f84643f0f3d06
# Parent  13211e07d9312b38cf18fa0aefac7bedc59d7e02
tuned;

diff -r 13211e07d931 -r d5132bba6a83 src/Tools/WWW_Find/unicode_symbols.ML
--- a/src/Tools/WWW_Find/unicode_symbols.ML	Tue Nov 20 18:59:35 2012 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML	Tue Nov 20 21:01:53 2012 +0100
@@ -1,17 +1,17 @@
 (*  Title:      Tools/WWW_Find/unicode_symbols.ML
     Author:     Timothy Bourke, NICTA
 
-Parse the ISABELLE_HOME/etc/symbols file.
+Ad-hoc parsing of ~~/etc/symbols.
 *)
 
 signature UNICODE_SYMBOLS =
 sig
-val symbol_to_unicode : string -> int option
-val abbrev_to_unicode : string -> int option
-val unicode_to_symbol : int -> string option
-val unicode_to_abbrev : int -> string option
-val utf8_to_symbols   : string -> string
-val utf8              : int list -> string
+  val symbol_to_unicode : string -> int option
+  val abbrev_to_unicode : string -> int option
+  val unicode_to_symbol : int -> string option
+  val unicode_to_abbrev : int -> string option
+  val utf8_to_symbols : string -> string
+  val utf8 : int list -> string
 end;
 
 structure UnicodeSymbols : UNICODE_SYMBOLS =
@@ -134,7 +134,7 @@
 
 in
 
-val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
+val line = (symbol -- unicode -- font -- abbr) >> (fn (((a, b), c), d) => (a, b, d));
 
 end;