# HG changeset patch
# User wenzelm
# Date 1353448324 -3600
# Node ID a96bd08258a227208a294e75c2ace47508dd51fb
# Parent  d5132bba6a831c38282c982aaa5f84643f0f3d06
support for symbol groups, retaining original order of declarations;
updated WWW_Find: untested change of ad-hoc parser of ~~/etc/symbols;

diff -r d5132bba6a83 -r a96bd08258a2 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Nov 20 21:01:53 2012 +0100
+++ b/src/Pure/General/symbol.scala	Tue Nov 20 22:52:04 2012 +0100
@@ -208,8 +208,8 @@
   {
     /* read symbols */
 
-    private val empty = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
-    private val key = new Regex("""(?xs) (.+): """)
+    private val No_Decl = new Regex("""(?xs) ^\s* (?: \#.* )? $ """)
+    private val Key = new Regex("""(?xs) (.+): """)
 
     private def read_decl(decl: String): (Symbol, Map[String, String]) =
     {
@@ -220,7 +220,7 @@
         props match {
           case Nil => Map()
           case _ :: Nil => err()
-          case key(x) :: y :: rest => read_props(rest) + (x -> y)
+          case Key(x) :: y :: rest => read_props(rest) + (x -> y)
           case _ => err()
         }
       }
@@ -231,9 +231,14 @@
     }
 
     private val symbols: List[(Symbol, Map[String, String])] =
-      Map((
-        for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
-          yield read_decl(decl)): _*).toList
+      (((List.empty[(Symbol, Map[String, String])], Set.empty[Symbol]) /:
+          split_lines(symbols_spec).reverse)
+        { case (res, No_Decl()) => res
+          case ((list, known), decl) =>
+            val (sym, props) = read_decl(decl)
+            if (known(sym)) (list, known)
+            else ((sym, props) :: list, known + sym)
+        })._1
 
 
     /* misc properties */
@@ -244,6 +249,11 @@
       Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
     }
 
+    val groups: List[(String, List[Symbol])] =
+      symbols.map({ case (sym, props) => (sym, props.get("group") getOrElse "other") })
+        .groupBy(_._2).toList.map({ case (group, list) => (group, list.map(_._1)) })
+        .sortBy(_._1)
+
     val abbrevs: Map[Symbol, String] =
       Map((
         for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
@@ -365,6 +375,7 @@
   /* tables */
 
   def names: Map[Symbol, String] = symbols.names
+  def groups: List[(String, List[Symbol])] = symbols.groups
   def abbrevs: Map[Symbol, String] = symbols.abbrevs
 
   def decode(text: String): String = symbols.decode(text)
@@ -391,8 +402,6 @@
     sym.startsWith("\\<") && sym.endsWith(">") && !sym.startsWith("\\<^")
 
 
-
-
   /* control symbols */
 
   def is_ctrl(sym: Symbol): Boolean =
diff -r d5132bba6a83 -r a96bd08258a2 src/Tools/WWW_Find/unicode_symbols.ML
--- 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;