src/Pure/General/symbol.scala
changeset 73606 d8a0e996614b
parent 73602 ec52a1a6ed31
equal deleted inserted replaced
73605:78aa7846e91f 73606:d8a0e996614b
   334         case _ => err()
   334         case _ => err()
   335       }
   335       }
   336     }
   336     }
   337 
   337 
   338     private val symbols: List[(Symbol, Properties.T)] =
   338     private val symbols: List[(Symbol, Properties.T)] =
   339       (((List.empty[(Symbol, Properties.T)], Set.empty[Symbol]) /:
   339       split_lines(symbols_spec).reverse.
   340           split_lines(symbols_spec).reverse)
   340         foldLeft((List.empty[(Symbol, Properties.T)], Set.empty[Symbol])) {
   341         { case (res, No_Decl()) => res
   341           case (res, No_Decl()) => res
   342           case ((list, known), decl) =>
   342           case ((list, known), decl) =>
   343             val (sym, props) = read_decl(decl)
   343             val (sym, props) = read_decl(decl)
   344             if (known(sym)) (list, known)
   344             if (known(sym)) (list, known)
   345             else ((sym, props) :: list, known + sym)
   345             else ((sym, props) :: list, known + sym)
   346         })._1
   346         }._1
   347 
   347 
   348 
   348 
   349     /* basic properties */
   349     /* basic properties */
   350 
   350 
   351     val properties: Map[Symbol, Properties.T] = Map(symbols: _*)
   351     val properties: Map[Symbol, Properties.T] = Map(symbols: _*)