diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 12 | ||||
| -rw-r--r-- | library/library.mli | 1 |
2 files changed, 13 insertions, 0 deletions
diff --git a/library/library.ml b/library/library.ml index 8b390832f..1088bcb16 100644 --- a/library/library.ml +++ b/library/library.ml @@ -394,6 +394,18 @@ let intern_from_file f = close_in ch; library +let load_library_todo f = + let paths = Loadpath.get_paths () in + let _, longf = + System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in + let f = longf^"i" in + let ch = System.with_magic_number_check raw_intern_library f in + let _ = System.skip_in_segment f ch in + let tasks, _, _ = System.marshal_in_segment f ch in + match tasks with + | Some a -> a, longf + | None -> errorlabstrm "load_library_todo" (str"not a .vi file") + let rec intern_library needed (dir, f) = (* Look if in the current logical environment *) try find_library dir, needed diff --git a/library/library.mli b/library/library.mli index 530209485..647138483 100644 --- a/library/library.mli +++ b/library/library.mli @@ -38,6 +38,7 @@ val start_library : string -> DirPath.t * string (** {6 End the compilation of a library and save it to a ".vo" file } *) val save_library_to : ?todo:'a -> DirPath.t -> string -> unit +val load_library_todo : string -> 'a * string (** {6 Interrogate the status of libraries } *) |