--- a/src/Pure/PIDE/resources.ML Thu Feb 28 21:59:58 2019 +0100
+++ b/src/Pure/PIDE/resources.ML Fri Mar 01 16:49:41 2019 +0100
@@ -31,6 +31,7 @@
imports: (string * Position.T) list, keywords: Thy_Header.keywords}
val parse_files: string -> (theory -> Token.file list) parser
val provide: Path.T * SHA1.digest -> theory -> theory
+ val provide_file: Token.file -> theory -> theory
val provide_parse_files: string -> (theory -> Token.file list * theory) parser
val loaded_files_current: theory -> bool
val check_path: Proof.context -> Path.T -> string * Position.T -> Path.T
@@ -215,6 +216,8 @@
error ("Duplicate use of source file: " ^ Path.print src_path)
else (master_dir, imports, (src_path, id) :: provided));
+fun provide_file (file: Token.file) = provide (#src_path file, #digest file);
+
fun provide_parse_files cmd =
parse_files cmd >> (fn files => fn thy =>
let