From 201a53ff145e8c85f6e98337331b0bce44dafde5 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 20 Nov 2000 08:40:11 +0000
Subject: 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
---
 pretyping/syntax_def.ml  | 33 ++++++++++++++++++++-------------
 pretyping/syntax_def.mli |  4 +++-
 2 files changed, 23 insertions(+), 14 deletions(-)

(limited to 'pretyping')

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
+  
 
diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli
index f889f2473..48a996991 100644
--- a/pretyping/syntax_def.mli
+++ b/pretyping/syntax_def.mli
@@ -10,6 +10,8 @@ open Rawterm
 
 val declare_syntactic_definition : identifier -> rawconstr -> unit
 
-val search_syntactic_definition : identifier -> rawconstr
+val search_syntactic_definition : section_path -> rawconstr
+
+val locate_syntactic_definition : section_path -> section_path
 
 
-- 
cgit v1.2.3