diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 17:45:27 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-09-29 17:45:27 +0200 |
| commit | 05ab666a1283de5500dbc0520d18bdb05d95f286 (patch) | |
| tree | 538cb7b07372d4e83a6c7823d5cb59ee54606099 /checker | |
| parent | 82a618e8a4945752698a7900c8af7a51091f7b1b (diff) | |
Make the interface of System.raw_extern_intern much saner.
There is no reason (any longer?) to create simultaneous closures for
interning and externing files. This patch makes the code more readable
by separating both functions and their signatures.
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 18 |
1 files changed, 4 insertions, 14 deletions
diff --git a/checker/check.ml b/checker/check.ml index c835cec82..2bc470aea 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -271,20 +271,10 @@ let try_locate_qualified_library qid = | LibNotFound -> error_lib_not_found qid (************************************************************************) -(*s Low-level interning/externing of libraries to files *) +(*s Low-level interning of libraries from files *) -(*s Loading from disk to cache (preparation phase) *) - -let raw_intern_library = - snd (System.raw_extern_intern Coq_config.vo_magic_number) - -let with_magic_number_check f a = - try f a - with System.Bad_magic_number fname -> - errorlabstrm "with_magic_number_check" - (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++ - spc () ++ str"It is corrupted" ++ spc () ++ - str"or was compiled with another version of Coq.") +let raw_intern_library f = + System.raw_intern_state Coq_config.vo_magic_number f (************************************************************************) (* Internalise libraries *) @@ -312,7 +302,7 @@ let intern_from_file (dir, f) = Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); let (sd,md,table,opaque_csts,digest) = try - let ch = with_magic_number_check raw_intern_library f in + let ch = System.with_magic_number_check raw_intern_library f in let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in |