diff options
Diffstat (limited to 'lib/aux_file.ml')
| -rw-r--r-- | lib/aux_file.ml | 41 |
1 files changed, 21 insertions, 20 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 0f0f09aa..0f947660 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (* The file format is a header @@ -17,10 +19,6 @@ let version = 1 let oc = ref None -let chop_extension f = - if check_suffix f ".v" then chop_extension f - else f - let aux_file_name_for vfile = dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" @@ -50,19 +48,21 @@ let contents x = x let empty_aux_file = H.empty -let get aux loc key = M.find key (H.find (Loc.unloc loc) aux) +let get ?loc aux key = M.find key (H.find (Option.cata Loc.unloc (0,0) loc) aux) -let record_in_aux_at loc key v = +let record_in_aux_at ?loc key v = Option.iter (fun oc -> - let i, j = Loc.unloc loc in - Printf.fprintf oc "%d %d %s %S\n" i j key v) - !oc + match loc with + | Some loc -> let i, j = Loc.unloc loc in + Printf.fprintf oc "%d %d %s %S\n" i j key v + | None -> Printf.fprintf oc "0 0 %s %S\n" key v + ) !oc -let current_loc = ref Loc.ghost +let current_loc : Loc.t option ref = ref None -let record_in_aux_set_at loc = current_loc := loc +let record_in_aux_set_at ?loc () = current_loc := loc -let record_in_aux key v = record_in_aux_at !current_loc key v +let record_in_aux key v = record_in_aux_at ?loc:!current_loc key v let set h loc k v = let m = try H.find loc h with Not_found -> M.empty in @@ -76,14 +76,15 @@ let load_aux_file_for vfile = let add loc k v = h := set !h loc k v in let aux_fname = aux_file_name_for vfile in try - let ic = open_in aux_fname in - let ver, hash, fname = Scanf.fscanf ic "COQAUX%d %s %s\n" ret3 in + let ib = Scanf.Scanning.from_channel (open_in aux_fname) in + let ver, hash, fname = + Scanf.bscanf ib "COQAUX%d %s %s\n" ret3 in if ver <> version then raise (Failure "aux file version mismatch"); if fname <> vfile then raise (Failure "aux file name mismatch"); let only_dummyloc = Digest.to_hex (Digest.file vfile) <> hash in while true do - let i, j, k, v = Scanf.fscanf ic "%d %d %s %S\n" ret4 in + let i, j, k, v = Scanf.bscanf ib "%d %d %s %S\n" ret4 in if not only_dummyloc || (i = 0 && j = 0) then add (i,j) k v; done; raise End_of_file @@ -94,4 +95,4 @@ let load_aux_file_for vfile = Flags.if_verbose Feedback.msg_info Pp.(str"Loading file "++str aux_fname++str": "++str s); empty_aux_file -let set h loc k v = set h (Loc.unloc loc) k v +let set ?loc h k v = set h (Option.cata Loc.unloc (0,0) loc) k v |