clarified signature: load_file is still required internally;
authorwenzelm
Wed Apr 30 22:45:26 2014 +0200 (2014-04-30 ago)
changeset 56803d3cc56ca54c9
parent 56802 c83eb2435b27
child 56804 38eaaa54cd6a
clarified signature: load_file is still required internally;
src/Pure/PIDE/resources.ML
     1.1 --- a/src/Pure/PIDE/resources.ML	Wed Apr 30 22:35:42 2014 +0200
     1.2 +++ b/src/Pure/PIDE/resources.ML	Wed Apr 30 22:45:26 2014 +0200
     1.3 @@ -15,7 +15,6 @@
     1.4    val parse_files: string -> (theory -> Token.file list) parser
     1.5    val provide: Path.T * SHA1.digest -> theory -> theory
     1.6    val provide_parse_files: string -> (theory -> Token.file list * theory) parser
     1.7 -  val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
     1.8    val loaded_files: theory -> Path.T list
     1.9    val loaded_files_current: theory -> bool
    1.10    val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
    1.11 @@ -108,7 +107,6 @@
    1.12      val full_path = check_file (master_directory thy) src_path;
    1.13      val text = File.read full_path;
    1.14      val id = SHA1.digest text;
    1.15 -    val _ = legacy_feature ("Raw file-system access to load file " ^ Path.print full_path);
    1.16    in ((full_path, id), text) end;
    1.17  
    1.18  fun loaded_files_current thy =