Cablage des syntactif defs avec la Nametab des objets

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@859 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 20 insertions, 13 deletions

diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
index 00ed971c1..0038b69d5 100644
--- a/pretyping/syntax_def.ml
+++ b/pretyping/syntax_def.ml
@@ -8,35 +8,42 @@ open Lib
 
 (* Syntactic definitions. *)
 
-let syntax_table = ref (Idmap.empty : rawconstr Idmap.t)
+let syntax_table = ref (Spmap.empty : rawconstr Spmap.t)
 
 let _ = Summary.declare_summary
 	  "SYNTAXCONSTANT"
 	  { Summary.freeze_function = (fun () -> !syntax_table);
 	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
-	    Summary.init_function = (fun () -> syntax_table := Idmap.empty) }
+	    Summary.init_function = (fun () -> syntax_table := Spmap.empty) }
 
-let add_syntax_constant id c =
-  syntax_table := Idmap.add id c !syntax_table
+let add_syntax_constant sp c =
+  syntax_table := Spmap.add sp c !syntax_table
 
-let cache_syntax_constant (sp,c) = 
-  add_syntax_constant (basename sp) c;
-  Nametab.push (basename sp) sp
-
-let open_syntax_constant (sp,_) =
-  Nametab.push (basename sp) sp
+(* Impossible de rendre récursive la définition de in_syntax_constant
+   et cache_syntax_constant, alors on triche ... *)
+let cache_syntax_constant = ref (fun c -> failwith "Undefined function")
 
 let (in_syntax_constant, out_syntax_constant) =
   let od = {
-    cache_function = cache_syntax_constant;
+    cache_function = (fun c -> !cache_syntax_constant c);
     load_function = (fun _ -> ());
-    open_function = cache_syntax_constant;
+    open_function = (fun c -> !cache_syntax_constant c);
     export_function = (fun x -> Some x) } 
   in
   declare_object ("SYNTAXCONSTANT", od)
 
+let _ =
+  cache_syntax_constant := fun (sp,c) ->
+    add_syntax_constant sp c;
+    Nametab.push_obj (basename sp) (sp, in_syntax_constant c)
+
 let declare_syntactic_definition id c =
   let _ = add_leaf id CCI (in_syntax_constant c) in ()
 
-let search_syntactic_definition id = Idmap.find id !syntax_table
+let search_syntactic_definition sp = Spmap.find sp !syntax_table
+
+let locate_syntactic_definition sp =
+  let (sp,obj) = Nametab.locate_obj sp in
+  if object_tag obj = "SYNTAXCONSTANT" then sp else raise Not_found
+