--- a/src/Pure/General/symbol.scala Wed Sep 04 13:13:14 2013 +0200
+++ b/src/Pure/General/symbol.scala Wed Sep 04 13:22:03 2013 +0200
@@ -247,7 +247,9 @@
})._1
- /* misc properties */
+ /* basic properties */
+
+ val properties: Map[Symbol, Properties.T] = Map(symbols: _*)
val names: Map[Symbol, String] =
{
@@ -381,6 +383,7 @@
/* tables */
+ def properties: Map[Symbol, Properties.T] = symbols.properties
def names: Map[Symbol, String] = symbols.names
def groups: List[(String, List[Symbol])] = symbols.groups
def abbrevs: Multi_Map[Symbol, String] = symbols.abbrevs