expose basic Symbol.properties (uninterpreted);
authorwenzelm
Wed, 04 Sep 2013 13:22:03 +0200
changeset 53400 673eb869e6ee
parent 53399 43b3b3fa6967
child 53402 50cc036f1522
expose basic Symbol.properties (uninterpreted);
src/Pure/General/symbol.scala
--- 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