//print(cacheFile);
// disabled at present!@!!
- if (cacheFile && File.exists(cacheFile)) {
+ if (false && cacheFile && File.exists(cacheFile)) {
// check filetime?
- var c_mt = File.getTimes(cacheFile);
- var o_mt = File.getTimes(srcFile);
+ var c_mt = File.mtime(cacheFile);
+ var o_mt = File.mtime(srcFile);
//println(c_mt.toSource());
// println(o_mt.toSource());
// this check does not appear to work according to the doc's - need to check it out.
- if (c_mt[0] > o_mt[0]) { // cached time > original time!
+ if (c_mt > o_mt) { // cached time > original time!
// use the cached mtimes..
var syms = JSON.parse(File.read(cacheFile));
if (cacheFile) {
File.write(cacheFile,
JSON.stringify(
- Parser.filesSymbols.toArray(srcFile)
- );
+ Parser.symbolsToObject(srcFile),
+ null,2
+ )
);
}