diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/aux_file.ml | 83 | ||||
-rw-r--r-- | lib/aux_file.mli | 21 | ||||
-rw-r--r-- | lib/clib.mllib | 1 |
3 files changed, 105 insertions, 0 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml new file mode 100644 index 000000000..98f1a51b8 --- /dev/null +++ b/lib/aux_file.ml @@ -0,0 +1,83 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* The file format is a header + * ("COQAUX%d %s %s\n" version hex_hash path) + * followed by an arbitrary number of entries + * ("%d %d %s %S\n" loc_begin loc_end key value) *) + +open Filename + +let version = 1 + +let oc = ref None + +let aux_file_name_for vfile = + dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" + +let start_aux_file_for vfile = + oc := Some (open_out (aux_file_name_for vfile)); + Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n" + version (Digest.to_hex (Digest.file vfile)) (CUnix.strip_path vfile) + +let stop_aux_file () = + close_out (Option.get !oc); + oc := None + +let recording () = not (Option.is_empty !oc) + +module H = Map.Make(struct type t = int * int let compare = compare end) +module M = Map.Make(String) +type data = string M.t +type aux_file = data H.t + +let empty_aux_file = H.empty + +let get aux loc key = M.find key (H.find (Loc.unloc loc) aux) + +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 + +let current_loc = ref Loc.ghost + +let record_in_aux_set_at loc = current_loc := loc + +let record_in_aux key v = record_in_aux_at !current_loc key v + +exception Outdated + +let load_aux_file_for vfile = + let ret3 x y z = x, y, z in + let ret4 x y z t = x, y, z, t in + let h = ref empty_aux_file in + let add loc k v = + let m = try H.find loc !h with Not_found -> M.empty in + h := H.add loc (M.add k v m) !h 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 + if ver <> version then raise (Failure "aux file version mismatch"); + if fname <> CUnix.strip_path vfile then + raise (Failure "aux file name mismatch"); + if Digest.to_hex (Digest.file vfile) <> hash then raise Outdated; + while true do + let i, j, k, v = Scanf.fscanf ic "%d %d %s %S\n" ret4 in + add (i,j) k v; + done; + raise End_of_file + with + | End_of_file -> !h + | Outdated -> empty_aux_file + | Sys_error s | Scanf.Scan_failure s + | Failure s | Invalid_argument s -> + Pp.(msg_error (str"Error loading file "++str aux_fname++str" : "++str s)); + empty_aux_file diff --git a/lib/aux_file.mli b/lib/aux_file.mli new file mode 100644 index 000000000..b24515c99 --- /dev/null +++ b/lib/aux_file.mli @@ -0,0 +1,21 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +type aux_file + +val load_aux_file_for : string -> aux_file +val get : aux_file -> Loc.t -> string -> string +val empty_aux_file : aux_file + +val start_aux_file_for : string -> unit +val stop_aux_file : unit -> unit +val recording : unit -> bool + +val record_in_aux_at : Loc.t -> string -> string -> unit +val record_in_aux : string -> string -> unit +val record_in_aux_set_at : Loc.t -> unit diff --git a/lib/clib.mllib b/lib/clib.mllib index 833182bce..d36fba36c 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -28,3 +28,4 @@ Serialize Xml_utils CUnix Envars +Aux_file |