src/Pure/General/file.ML
2012-08-23 wenzelm 2012-08-23 tuned messages: end-of-input rarely means physical end-of-file from the past;
2012-07-23 wenzelm 2012-07-23 removed redundant check (cf. a8ed41b6280b);
2011-09-11 wenzelm 2011-09-11 more orthogonal signature;
2011-07-16 wenzelm 2011-07-16 some file and directory operations;
2011-07-16 wenzelm 2011-07-16 added File.fold_pages for streaming of large files; prefer \f notation;
2011-07-01 noschinl 2011-07-01 reverted 782991e4180d: fold_fields was never used
2011-04-13 noschinl 2011-04-13 Generalized File.fold_lines to File.fold_fields
2011-03-20 wenzelm 2011-03-20 replaced File.check by specific File.check_file, File.check_dir; clarified File.full_path -- include parts of former Thy_Load.get_file; simplified Thy_Load.check_file -- do not read/digest yet; merged Thy_Load.check_thy/deps_thy -- always read text and parse header; clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator; Thy_Info.check_deps etc.: File.read exactly once;
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2010-11-28 wenzelm 2010-11-28 more permissive Isabelle_System.mkdir; exported File.is_dir (weak test);
2010-11-27 wenzelm 2010-11-27 explicit check for requirement;
2010-11-27 wenzelm 2010-11-27 tuned;
2010-11-27 wenzelm 2010-11-27 more explicit Isabelle_System operations;
2010-11-27 wenzelm 2010-11-27 moved file identification to thy_load.ML (where it is actually used);
2010-07-08 haftmann 2010-07-08 rm_tree: remove entire file system trees
2010-07-01 haftmann 2010-07-01 refined semantics of mkdir_leaf: do not fail if directory already exists
2010-06-30 haftmann 2010-06-30 mkdir_leaf -- avoiding surprises with typos in user-given paths
2010-02-06 wenzelm 2010-02-06 renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2009-10-27 wenzelm 2009-10-27 non-critical atomic accesses;
2009-10-15 wenzelm 2009-10-15 exported File.shell_quote;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-06-27 wenzelm 2009-06-27 builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
2009-01-21 wenzelm 2009-01-21 removed Ids;
2008-10-06 wenzelm 2008-10-06 fold_lines: more tuning, avoiding extra split_last;
2008-10-04 wenzelm 2008-10-04 replaced ISATOOL by ISABELLE_TOOL;
2008-10-04 wenzelm 2008-10-04 renamed isatool to isabelle_tool in programming interfaces;
2008-08-28 wenzelm 2008-08-28 tuned fold_lines;
2008-08-28 wenzelm 2008-08-28 fold_lines: simplified, more efficient due to String.fields;
2008-08-27 wenzelm 2008-08-27 renamed Buffer.write to File.write_buffer; added scalable iterator fold_lines; tuned;
2008-05-24 wenzelm 2008-05-24 ident: naive caching prevents potentially slow external invocations; tuned comments; tuned;
2008-05-18 wenzelm 2008-05-18 removed norm_absolute (not thread safe; chdir does not guarantee normalization anyway); full_path: no link expansion here (reverted change of 1.18); ident: OS.FileSys.fullPath takes care of link expansion;
2008-04-15 wenzelm 2008-04-15 Library.is_equal;
2008-03-31 wenzelm 2008-03-31 discontinued unused hooks explode_platform_path_fn, platform_path_fn, shell_path_fn; norm_absolute: non-critical (not thread-safe!); added open_input, open_output, open_append combinators; tuned;
2008-03-06 wenzelm 2008-03-06 common setup for system_out/system;
2007-08-28 wenzelm 2007-08-28 norm_absolute: CRITICAL;
2007-08-20 wenzelm 2007-08-20 File.read/write/append: non-critical (basic IO operations already thread-safe);
2007-07-29 wenzelm 2007-07-29 NAMED_CRITICAL;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections (for multithreading);
2007-07-19 wenzelm 2007-07-19 added rep_ident;
2007-07-19 wenzelm 2007-07-19 replaced info by ident (for full identification, potentially content-based); ident: invoke external lib/scripts/fileident, depending on ISABELLE_FILE_IDENT;
2007-07-17 wenzelm 2007-07-17 moved cd/pwd to ML compatibility layer (simplifies bootstrapping with Alice);
2007-01-21 wenzelm 2007-01-21 moved File.use to ML_Context.use;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-15 wenzelm 2006-12-15 avoid conflict with Alice keywords: renamed pack -> implode, unpack -> explode, any -> many, avoided assert;
2006-06-29 kleing 2006-06-29 use -f in cp to overwrite read-only files (e.g. .svn in document/)
2006-04-26 wenzelm 2006-04-26 tuned;
2006-01-19 wenzelm 2006-01-19 use: Output.ML_errors;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2005-10-11 wenzelm 2005-10-11 added assert; tuned;
2005-07-06 wenzelm 2005-07-06 added write_list, append_list;
2005-06-29 wenzelm 2005-06-29 added eq; improved copy/copy_dir: only copy if non-eq;
2005-06-06 wenzelm 2005-06-06 copy_dir: be permissive wrt. errors;
2005-06-05 wenzelm 2005-06-05 removed sysify_path, quote_sysity_path etc.; added platform_path, shell_path etc.; improved copy: support dir as target; added copy_dir; added isatool; tuned;
2005-05-18 wenzelm 2005-05-18 tuned;
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-08-23 berghofe 2004-08-23 Added function for "normalizing" absolute paths (i.e. dereferencing of symbolic links; the functions in path.ML cannot do this). This is used by function full_path.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2002-02-15 wenzelm 2002-02-15 moved copy_all to Thy/present.ML;
2001-11-09 wenzelm 2001-11-09 got rid of obsolete input filtering;