# HG changeset patch # User wenzelm # Date 1395821251 -3600 # Node ID 7ede6ca96c617b56624fce7811b10a4fcde16c77 # Parent 9315d3988d736d2d331d0f66ff44368e5908c02c superseded by (provide_)parse_files; diff -r 9315d3988d73 -r 7ede6ca96c61 src/Pure/PIDE/resources.ML --- a/src/Pure/PIDE/resources.ML Wed Mar 26 08:59:53 2014 +0100 +++ b/src/Pure/PIDE/resources.ML Wed Mar 26 09:07:31 2014 +0100 @@ -108,6 +108,7 @@ val full_path = check_file (master_directory thy) src_path; val text = File.read full_path; val id = SHA1.digest text; + val _ = legacy_feature ("Raw file-system access to load file " ^ Path.print full_path); in ((full_path, id), text) end; fun loaded_files_current thy =