# HG changeset patch
# User wenzelm
# Date 1245184790 -7200
# Node ID 7d6a518b5a2badde61e6d61ad60d377fdfef5df8
# Parent  cfaed41ee2c569955627482808d6a59ed7a9cc7b
added names, abbrevs;

diff -r cfaed41ee2c5 -r 7d6a518b5a2b src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Jun 16 21:45:35 2009 +0200
+++ b/src/Pure/General/symbol.scala	Tue Jun 16 22:39:50 2009 +0200
@@ -118,6 +118,18 @@
         yield read_decl(decl)
 
 
+    /* misc properties */
+
+    val names: Map[String, String] = {
+      val name = new Regex("""\\<([A-Za-z][A-Za-z0-9_']*)>""")
+      Map((for ((sym @ name(a), _) <- symbols) yield (sym -> a)): _*)
+    }
+
+    val abbrevs: Map[String, String] = Map((
+      for ((sym, props) <- symbols if props.isDefinedAt("abbrev"))
+        yield (sym -> props("abbrev"))): _*)
+
+
     /* main recoder methods */
 
     private val (decoder, encoder) =