if (c_mt > o_mt) { // cached time > original time!
// use the cached mtimes..
+ print("Read " + cacheFile);
var syms = JSON.parse(File.read(cacheFile), function(k, v) {
//print(k);
if (typeof(v) != 'object') {
XObject.extend(ret, v);
return ret;
});
-
- for (var sy in syms) {
+ print("Add sybmols " + cacheFile);
+ for (var sy in syms._index) {
//println("ADD:" + sy );
Parser.symbols.addSymbol(syms[sy]);
}