# 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