diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-01 14:22:13 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-01 14:23:37 +0200 |
| commit | 5ea872c80cc8b9d2845629cc75369f061e3bad05 (patch) | |
| tree | 5c6183c776812e100a6694094ec9631e38fbc980 /kernel/nativecode.ml | |
| parent | 5776f7d2b4753b89efa095a0f6774dac702fdfbd (diff) | |
More efficient data structure to check if a native file is loaded.
Spotted by PMP.
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index e2f43b93e..87302dcf5 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1930,13 +1930,15 @@ let compile_constant env sigma prefix ~interactive con cb = arg|]))):: [Glet(gn, mkMLlam [|c_uid|] code)], Linked prefix -let loaded_native_files = ref ([] : string list) +module StringOrd = struct type t = string let compare = String.compare end +module StringSet = Set.Make(StringOrd) -let is_loaded_native_file s = String.List.mem s !loaded_native_files +let loaded_native_files = ref StringSet.empty + +let is_loaded_native_file s = StringSet.mem s !loaded_native_files let register_native_file s = - if not (is_loaded_native_file s) then - loaded_native_files := s :: !loaded_native_files + loaded_native_files := StringSet.add s !loaded_native_files let is_code_loaded ~interactive name = match !name with |