--- a/src/Tools/WWW_Find/unicode_symbols.ML Tue Nov 20 21:01:53 2012 +0100
+++ b/src/Tools/WWW_Find/unicode_symbols.ML Tue Nov 20 22:52:04 2012 +0100
@@ -22,7 +22,7 @@
open Basic_Symbol_Pos
val keywords =
- Scan.make_lexicon (map Symbol.explode ["code", "font", "abbrev", ":"]);
+ Scan.make_lexicon (map Symbol.explode ["code", "group", "font", "abbrev", ":"]);
datatype token_kind =
Symbol | AsciiSymbol | Keyword | Name | Code | Space | Comment | EOF;
@@ -128,13 +128,15 @@
val name = Scan.one is_name >> str_of_token;
val unicode = $$$ "code" -- $$$ ":" |-- hex_code;
+val group = Scan.option ($$$ "group" -- $$$ ":" |-- name);
val font = Scan.option ($$$ "font" -- $$$ ":" |-- name);
val abbr = Scan.option ($$$ "abbrev" -- $$$ ":"
|-- (ascii_sym || $$$ ":" || name));
in
-val line = (symbol -- unicode -- font -- abbr) >> (fn (((a, b), c), d) => (a, b, d));
+val line = (symbol -- unicode -- group -- font -- abbr)
+ >> (fn ((((a, b), _), _), c) => (a, b, c));
end;