1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
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
|
