Export information des references de notations pour coqdoc

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

3 files changed, 37 insertions, 15 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 84be738495..e4bf4c9d77 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -137,6 +137,23 @@ let add_glob loc ref =
   let dp = string_of_dirpath (Lib.library_part ref) in
   dump_string (Printf.sprintf "R%d %s.%s\n" (fst loc) dp id)
 
+let loc_of_notation f loc args ntn =
+  if args=[] or ntn.[0] <> '_' then fst loc else snd (f (List.hd args))
+
+let ntn_loc = loc_of_notation constr_loc
+let patntn_loc = loc_of_notation cases_pattern_loc
+
+let dump_notation_location =
+  let token_number = ref 0 in
+  fun pos ntn ((path,df),sc) ->
+    let rec next () =
+      let (bp,_ as loc) = !Lexer.current_location_function !token_number in
+      if bp >= pos then loc else (incr token_number; next ()) in
+    let loc = next () in
+    let path = string_of_dirpath path in
+    let sc = match sc with Some sc -> " "^sc | None -> "" in
+    dump_string (Printf.sprintf "R%d %s \"%s\"%s\n" (fst loc) path df sc)
+
 (**********************************************************************)
 (* Remembering the parsing scope of variables in notations            *)
 
@@ -408,7 +425,8 @@ let rec intern_cases_pattern scopes aliases tmp_scope = function
       intern_cases_pattern scopes aliases tmp_scope a
   | CPatNotation (loc, ntn, args) ->
       let scopes = option_cons tmp_scope scopes in
-      let (ids,c) = Symbols.interp_notation ntn scopes in
+      let ((ids,c),df) = Symbols.interp_notation ntn scopes in
+      if !dump then dump_notation_location (patntn_loc loc args ntn) ntn df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
       subst_cases_pattern loc aliases intern_cases_pattern subst scopes c
   | CPatNumeral (loc, n) ->
@@ -630,7 +648,8 @@ let internalise sigma env allow_soapp lvar c =
     | CNotation (_,"( _ )",[a]) -> intern env a
     | CNotation (loc,ntn,args) ->
 	let scopes = option_cons tmp_scope scopes in
-	let (ids,c) = Symbols.interp_notation ntn scopes in
+	let ((ids,c),df) = Symbols.interp_notation ntn scopes in
+        if !dump then dump_notation_location (ntn_loc loc args ntn) ntn df;
 	let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
 	subst_rawconstr loc intern subst env c
     | CNumeral (loc, n) ->
diff --git a/interp/symbols.ml b/interp/symbols.ml
index 44237b6c99..32d74b651a 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -43,11 +43,11 @@ type level = precedence * tolerability list
 type delimiters = string
 
 type scope = {
-  notations: (interpretation * string * bool) Stringmap.t;
+  notations: (interpretation * (dir_path * string) * bool) Stringmap.t;
   delimiters: delimiters option
 }
 
-(* Uninterpreted notation map: notation -> level *)
+(* Uninterpreted notation map: notation -> level * dir_path *)
 let notation_level_map = ref Stringmap.empty
 
 (* Scopes table: scope_name -> symbol_interpretation *)
@@ -284,15 +284,16 @@ let rec find_interpretation f = function
       let scope = match sce with
 	| Scope s -> s 
 	| SingleNotation _ -> default_scope in
-      (try f (find_scope scope)
+      (try f scope
       with Not_found -> find_interpretation f scopes)
   | [] -> raise Not_found
 
 let rec interp_notation ntn scopes =
-  let f scope =
-    let (pat,_,pp8only) = Stringmap.find ntn scope.notations in
+  let f sc =
+    let scope = find_scope sc in
+    let (pat,df,pp8only) = Stringmap.find ntn scope.notations in
     if pp8only then raise Not_found;
-    pat in
+    pat,(df,if sc = default_scope then None else Some sc) in
   try find_interpretation f (List.fold_right push_scope scopes !scope_stack)
   with Not_found -> error ("Unknown interpretation for notation \""^ntn^"\"")
 
@@ -488,7 +489,7 @@ let pr_named_scope prraw scope sc =
   ++ fnl ()
   ++ pr_scope_classes scope
   ++ Stringmap.fold
-       (fun ntn ((_,r),df,_) strm ->
+       (fun ntn ((_,r),(_,df),_) strm ->
 	 pr_notation_info prraw df r ++ fnl () ++ strm)
        sc.notations (mt ())
 
@@ -542,7 +543,7 @@ let locate_notation prraw ntn =
     prlist (fun (ntn,l) ->
       let scope = find_default ntn !scope_stack in
       prlist 
-	(fun (sc,r,df) ->
+	(fun (sc,r,(_,df)) ->
 	  hov 0 (
 	    pr_notation_info prraw df r ++ tbrk (1,2) ++
 	    (if sc = default_scope then mt () else (str ": " ++ str sc)) ++ 
@@ -554,7 +555,7 @@ let locate_notation prraw ntn =
 let collect_notation_in_scope scope sc known =
   assert (scope <> default_scope);
   Stringmap.fold
-    (fun ntn ((_,r),df,_) (l,known as acc) ->
+    (fun ntn ((_,r),(_,df),_) (l,known as acc) ->
       if List.mem ntn known then acc else ((df,r)::l,ntn::known))
     sc.notations ([],known)
 
@@ -570,7 +571,7 @@ let collect_notations stack =
       | SingleNotation ntn ->
 	  if List.mem ntn knownntn then (all,knownntn)
 	  else
-	    let ((_,r),df,_) =
+	    let ((_,r),(_,df),_) =
 	      Stringmap.find ntn (find_scope default_scope).notations in
 	    let all' = match all with
 	      | (s,lonelyntn)::rest when s = default_scope ->
diff --git a/interp/symbols.mli b/interp/symbols.mli
index ffd82c8084..a86ed49f1b 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -88,12 +88,13 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of kernel_name
 val declare_notation_interpretation : notation -> scope_name option ->
-      interpretation -> string -> bool -> unit
+      interpretation -> dir_path * string -> bool -> unit
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
 (* Returns the interpretation bound to a notation *)
-val interp_notation : notation -> scope_name list -> interpretation
+val interp_notation : notation -> scope_name list -> 
+      interpretation * ((dir_path * string) * scope_name option)
 
 (* Returns the possible notations for a given term *)
 val uninterp_notations : rawconstr ->
@@ -111,7 +112,8 @@ val availability_of_notation : scope_name option * notation -> scopes ->
 (*s Declare and test the level of a (possibly uninterpreted) notation *)
 
 val declare_notation_level : notation -> level option * level -> unit
-val level_of_notation : notation -> level option * level (* [Not_found] if no level *)
+val level_of_notation : notation -> level option * level 
+      (* raise [Not_found] if no level *)
 
 (*s** Miscellaneous *)