+ # Cache a file as `{filepath}.tmp` and replace the original if different
+ private fun cache_file(filepath: String): FileWriter do
+ if toolcontext.opt_ant.value and filepath.file_exists then
+ return new FileWriter.open("{filepath}.tmp")
+ else
+ return new FileWriter.open(filepath)
+ end
+ end
+
+ # Close the writer and move tmp file to original if modified
+ private fun close_cache(filepath: String, file: FileWriter) do
+ file.close
+ if "{filepath}.tmp".file_exists then
+ sys.system("if ! diff {filepath}.tmp {filepath} > /dev/null; then mv {filepath}.tmp {filepath}; else rm {filepath}.tmp; fi")
+ end
+ end
+