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;

renamed "pairself" to "apply2", in accordance to @{apply 2};

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;

tuned;

moved bash operations to Isabelle_System (cf. Scala version);

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;

explicit type SHA1.digest;

more conventional variable name;

slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
more robust rm_tree -- somewhat dangerous and not exported;
tuned;

more explicit Isabelle_System operations;

renamed raw "explode" function to "raw_explode" to emphasize its meaning;

keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)

check the return code of the SMT solver and raise an exception if the prover failed

return the process return code along with the process outputs

combinator with_tmp_dir

simplified Cache_IO interface (input is just a string and not already stored in a file)

use internal SHA1 digest implementation for generating hash keys

remove component Cache_IO (external dependency on MD5 will be replaced by internal SHA1 digest implementation)

--HG--
rename : src/Tools/Cache_IO/cache_io.ML => src/Tools/cache_io.ML