src/Tools/cache_io.ML
2016-03-07 wenzelm 2016-03-07 File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output; clarified treatment of whitespace in some bash scripts;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2012-12-03 wenzelm 2012-12-03 synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic); clarified signature -- cache init is unsynchronized and hopefully used at most once per file;
2012-12-03 wenzelm 2012-12-03 tuned;
2011-07-16 wenzelm 2011-07-16 moved bash operations to Isabelle_System (cf. Scala version);
2011-03-26 wenzelm 2011-03-26 Isabelle_System.create_tmp_path/with_tmp_file: optional extension; thread-safe versions of Present.display_graph, Present.isabelle_browser, Present.drafts -- using Isabelle_System.with_tmp_dir;
2011-03-13 wenzelm 2011-03-13 explicit type SHA1.digest;
2011-03-13 wenzelm 2011-03-13 more conventional variable name;
2010-12-20 wenzelm 2010-12-20 slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version); more robust rm_tree -- somewhat dangerous and not exported; tuned;
2010-11-27 wenzelm 2010-11-27 more explicit Isabelle_System operations;
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-11-17 boehmes 2010-11-17 keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
2010-11-12 boehmes 2010-11-12 check the return code of the SMT solver and raise an exception if the prover failed
2010-11-08 boehmes 2010-11-08 return the process return code along with the process outputs
2010-07-08 haftmann 2010-07-08 combinator with_tmp_dir
2010-04-07 boehmes 2010-04-07 simplified Cache_IO interface (input is just a string and not already stored in a file)
2010-03-24 boehmes 2010-03-24 use internal SHA1 digest implementation for generating hash keys
2010-03-24 boehmes 2010-03-24 remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation)