//see symbols_old.js