# HG changeset patch # User wenzelm # Date 1345726722 -7200 # Node ID 5b192d6b7a54226641566aedce9d8db0d4b6791d # Parent 04576657cf947d3063e6b744131a2be41b51394e tuned signature; diff -r 04576657cf94 -r 5b192d6b7a54 src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Thu Aug 23 13:55:27 2012 +0200 +++ b/src/Pure/Thy/thy_load.ML Thu Aug 23 14:58:42 2012 +0200 @@ -8,11 +8,13 @@ sig val master_directory: theory -> Path.T val imports_of: theory -> string list - val provide: Path.T * SHA1.digest -> theory -> theory val thy_path: Path.T -> Path.T + val parse_files: string -> (theory -> Token.file list) parser val check_thy: Path.T -> string -> {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list, keywords: Thy_Header.keywords} + val provide: Path.T * SHA1.digest -> theory -> theory + val provide_parse_files: string -> (theory -> Token.file list * theory) parser val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string val use_file: Path.T -> theory -> string * theory val loaded_files: theory -> Path.T list @@ -22,7 +24,6 @@ val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string -> theory list -> theory * unit future - val parse_files: string -> (theory -> Token.file list) parser val set_master_path: Path.T -> unit val get_master_path: unit -> Path.T end; @@ -58,12 +59,6 @@ fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, [])); -fun provide (src_path, id) = - map_files (fn (master_dir, imports, provided) => - if AList.defined (op =) provided src_path then - error ("Duplicate use of source file: " ^ Path.print src_path) - else (master_dir, imports, (src_path, id) :: provided)); - (* inlined files *) @@ -147,6 +142,19 @@ (* load files *) +fun provide (src_path, id) = + map_files (fn (master_dir, imports, provided) => + if AList.defined (op =) provided src_path then + error ("Duplicate use of source file: " ^ Path.print src_path) + else (master_dir, imports, (src_path, id) :: provided)); + +fun provide_parse_files cmd = + parse_files cmd >> (fn files => fn thy => + let + val fs = files thy; + val thy' = fold (fn {src_path, text, ...} => provide (src_path, SHA1.digest text)) fs thy; + in (fs, thy') end); + fun load_file thy src_path = let val full_path = check_file (master_directory thy) src_path;