diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-19 14:17:35 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-19 14:17:35 +0000 |
commit | 76e3b2928b766a76ee7e29dd3f6867cd48f95a52 (patch) | |
tree | 5a5a73ee8770cba524b8c24892f709a308e9ab3b /library/nametab.ml | |
parent | 5393ee683be9e19ab25888925f561ea4f4b1dddb (diff) |
- un effort sur la doc (ocamlweb)
- module Nametab
- module Impargs
- correction bug : Parameter id : t => vérification que t est bien un type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@76 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.ml')
-rwxr-xr-x | library/nametab.ml | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/library/nametab.ml b/library/nametab.ml new file mode 100755 index 000000000..b84eda23a --- /dev/null +++ b/library/nametab.ml @@ -0,0 +1,44 @@ + +(* $Id$ *) + +open Names + +let cci_tab = ref Idmap.empty +let fw_tab = ref Idmap.empty + +let fw_sp_of_id id = + Idmap.find id !fw_tab + +let sp_of_id kind id = + match kind with + | FW -> Idmap.find id !fw_tab + | CCI -> Idmap.find id !cci_tab + | OBJ -> invalid_arg "Nametab.sp_of_id" + +let push id sp = + match kind_of_path sp with + | FW -> fw_tab := Idmap.add id sp !fw_tab + | CCI -> cci_tab := Idmap.add id sp !cci_tab + | OBJ -> invalid_arg "Nametab.push" + +(* Registration as a global table and roolback. *) + +let init () = + cci_tab := Idmap.empty; + cci_tab := Idmap.empty + +type frozen = section_path Idmap.t * section_path Idmap.t + +let freeze () = (!cci_tab, !fw_tab) + +let unfreeze (cci,fw) = cci_tab := cci; fw_tab := fw + +let _ = + Summary.declare_summary "names" + { Summary.freeze_function = freeze; + Summary.unfreeze_function = unfreeze; + Summary.init_function = init } + +let rollback f x = + let fs = freeze () in + try f x with e -> begin unfreeze fs; raise e end |