# HG changeset patch
# User wenzelm
# Date 1378293723 -7200
# Node ID 673eb869e6ee3b179bb24512f55b36c717c2cf0f
# Parent  43b3b3fa69674fe8512f27d1699b808c54ed5cb9
expose basic Symbol.properties (uninterpreted);

diff -r 43b3b3fa6967 -r 673eb869e6ee 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