glob.ml 1.35 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2013   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9 10
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)
11 12 13

open Ident

Andrei Paskevich's avatar
Andrei Paskevich committed
14 15
let flag = Debug.register_flag "track_symbol_use"
  ~desc:"Track@ symbol@ occurrences@ in@ source@ files.@ Used@ by@ why3doc."
16

17
let () = Debug.unset_flag flag (* make sure it is unset by default *)
18

19
let dummy_id = id_register (id_fresh "dummy")
20

21 22
let glob = Hashtbl.create 5003
  (* could be improved with nested hash tables *)
23

24
(* dead code
25 26 27 28
let with_loc f = function
  | None -> ()
  | Some loc when loc = Loc.dummy_position -> ()
  | Some loc -> f loc
29
*)
30

31 32 33 34
let use loc id =
  let f, l, c, _ = Loc.get loc in
(* Format.eprintf "GLOB USE: id=%s at %s/%d/%d@." id.id_string f l c; *)
  Hashtbl.add glob (f, l, c) id
35

36 37
let locate pos =
  Hashtbl.find glob pos