Several bug-fixes and improvements of coqdoc

- make links to section variables working (used qualified names for
  disambiguation and fixed the place in intern_var where to dump them)
  (wish #2277)
- mapping of physical to logical paths now follows coq (see bug #2274)
  (incidentally, it was also incorrectly seeing foobar.v as a in directory foo)
- added links for notations
- added new category "other" for indexing entries not starting with latin letter
  (e.g. notations or non-latin identifiers which was otherwise broken)
- protected non-notation strings (from String.v) from utf8 symbol interpretation
- incidentally quoted parseable _ in notations to avoid confusion with
  placeholder in the "_ + _" form of notation
- improved several "Sys_error" error messages
- fixed old bug about second dot of ".." being interpreted as regular dot
- removed obsolete lexer in index.mll (and renamed index.mll to index.ml)
- added a test-suite file for testing various features of coqdoc

Things that still do not work:
- when a notation is redefined several times in the same scope, only
  the link to the first definition works
- if chars and symbols are not separated in advance, idents
  that immediately follow symbols are not detected
  (e.g. as in {True}+{True} where coqdoc sees a symbol "+{True}")
- parentheses, curly brackets and semi-colon not linked in notations

Things that can probably be improved:
- all notations are indexed in the same category "other"; can we do better?
- all non-latin identifiers (e.g. Greek letters) are also indexed in the
  same "other" category; can we do better?
- globalization data for notations could be compacted (currently there is one
  line per each proper location covered by the notation)

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

7 files changed, 68 insertions, 56 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 009a219650..eb1d1985ff 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -337,7 +337,7 @@ let rec subst_aconstr_in_rawconstr loc interp (subst,substlist as sub) infos c =
 let intern_notation intern (_,_,tmp_scope,scopes as env) loc ntn fullargs =
   let ntn,(args,argslist as fullargs) = contract_notation ntn fullargs in
   let (((ids,idsl),c),df) = interp_notation loc ntn (tmp_scope,scopes) in
-  Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) df;
+  Dumpglob.dump_notation_location (ntn_loc loc fullargs ntn) ntn df;
   let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids args in
   let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl argslist in
   subst_aconstr_in_rawconstr loc intern (subst,substlist) ([],env) c
@@ -383,9 +383,8 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
   with Not_found ->
   (* Is [id] bound in current env or is an ltac var bound to constr *)
   if Idset.mem id env or List.mem id vars1
-  then (
-    Dumpglob.dump_reference loc "<>" (string_of_id id) "var";
-    RVar (loc,id), [], [], [])
+  then
+    RVar (loc,id), [], [], []
   (* Is [id] a notation variable *)
   else if List.mem_assoc id vars3
   then
@@ -404,7 +403,10 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
 	(* [id] a section variable *)
 	(* Redundant: could be done in intern_qualid *)
 	let ref = VarRef id in
-	  RRef (loc, ref), implicits_of_global ref, find_arguments_scope ref, []
+	let impls = implicits_of_global ref in
+	let scopes = find_arguments_scope ref in
+	Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
+	RRef (loc, ref), impls, scopes, []
       with _ ->
 	(* [id] a goal variable *)
 	RVar (loc,id), [], [], []
@@ -811,7 +813,7 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
   | CPatNotation (loc, ntn, fullargs) ->
       let ntn,(args,argsl as fullargs) = contract_pat_notation ntn fullargs in
       let (((ids',idsl'),c),df) = Notation.interp_notation loc ntn (tmp_scope,scopes) in
-      Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) df;
+      Dumpglob.dump_notation_location (patntn_loc loc fullargs ntn) ntn df;
       let subst = List.map2 (fun (id,scl) a -> (id,(a,scl))) ids' args in
       let substlist = List.map2 (fun (id,scl) a -> (id,(a,scl))) idsl' argsl in
       let ids'',pl =
@@ -820,9 +822,8 @@ let rec intern_cases_pattern genv scopes (ids,asubst as aliases) tmp_scope pat=
       in ids@ids'', pl
   | CPatPrim (loc, p) ->
       let a = alias_of aliases in
-      let (c,df) = Notation.interp_prim_token_cases_pattern loc p a
+      let (c,_) = Notation.interp_prim_token_cases_pattern loc p a
 	(tmp_scope,scopes) in
-      Dumpglob.dump_notation_location (fst (unloc loc)) df;
       (ids,[asubst,c])
   | CPatDelimiters (loc, key, e) ->
       intern_pat (find_delimiters_scope loc key::scopes) aliases None e
@@ -1118,9 +1119,7 @@ let internalise sigma globalenv env allow_patvar lvar c =
     | CGeneralization (loc,b,a,c) ->
         intern_generalization intern env lvar loc b a c
     | CPrim (loc, p) ->
-	let c,df = Notation.interp_prim_token loc p (tmp_scope,scopes) in
-	Dumpglob.dump_notation_location (fst (unloc loc)) df;
-	c
+	fst (Notation.interp_prim_token loc p (tmp_scope,scopes))
     | CDelimiters (loc, key, e) ->
 	intern (ids,unb,None,find_delimiters_scope loc key::scopes) e
     | CAppExpl (loc, (isproj,ref), args) ->
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 9faea54065..519f902bae 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -47,23 +47,10 @@ let previous_state = ref MultFiles
 let pause () = previous_state := !glob_output; glob_output := NoGlob
 let continue () = glob_output := !previous_state
 
+type coqdoc_state = Lexer.location_table
 
-let token_number = ref 0
-let last_pos = ref 0
-
-type coqdoc_state = Lexer.location_table * int * int
-
-let coqdoc_freeze () =
-  let lt = Lexer.location_table() in
-  let state = (lt,!token_number,!last_pos) in
-    token_number := 0;
-    last_pos := 0;
-    state
-
-let coqdoc_unfreeze (lt,tn,lp) =
-  Lexer.restore_location_table lt;
-  token_number := tn;
-  last_pos := lp
+let coqdoc_freeze = Lexer.location_table
+let coqdoc_unfreeze = Lexer.restore_location_table
 
 open Decl_kinds
 
@@ -200,19 +187,31 @@ let dump_libref loc dp ty =
   dump_string (Printf.sprintf "R%d %s <> <> %s\n"
 		  (fst (Util.unloc loc)) (Names.string_of_dirpath dp) ty)
 
-let dump_notation_location pos ((path,df),sc) =
+let cook_notation df sc =
+  let ntn = String.make (String.length df * 3) '_' in
+  let j = ref 0 in
+  let quoted = ref false in
+  for i = 0 to String.length df - 1 do
+    if df.[i] = '\'' then quoted := not !quoted;
+    if df.[i] = ' ' then (ntn.[!j] <- '_'; incr j) else
+    if df.[i] = '_' && not !quoted then (ntn.[!j] <- 'x'; incr j) else
+    if df.[i] = 'x' && not !quoted then (String.blit "'x'" 0 ntn !j 3; j := !j + 3) else
+    (ntn.[!j] <- df.[i]; incr j)
+  done;
+  let df = String.sub ntn 0 !j in
+  match sc with Some sc -> ":" ^ sc ^ ":" ^ df | _ -> "::" ^ df
+
+let dump_notation (loc,(df,_)) sc sec =
+  (* We dump the location of the opening '"' *)
+  dump_string (Printf.sprintf "not %d %s %s\n" (fst (Util.unloc loc))
+    (Names.string_of_dirpath (Lib.current_dirpath sec)) (cook_notation df sc))
+
+let dump_notation_location posl df (((path,secpath),_),sc) =
   if dump () then
-    let rec next growing =
-      let loc = Lexer.location_function !token_number in
-      let (bp,_) = Util.unloc loc in
-	if growing then if bp >= pos then loc else (incr token_number; next true)
-	else if bp = pos then loc
-	else if bp > pos then (decr token_number;next false)
-	else (incr token_number;next true) in
-    let loc = next (pos >= !last_pos) in
-      last_pos := pos;
-      let path = Names.string_of_dirpath path in
-      let _sc = match sc with Some sc -> " "^sc | _ -> "" in
-	dump_string (Printf.sprintf "R%d %s \"%s\" not\n" (fst (Util.unloc loc)) path df)
-
-
+    let path = Names.string_of_dirpath path in
+    let secpath = Names.string_of_dirpath secpath in
+    let df = cook_notation df sc in
+    List.iter (fun (bl,el) ->
+      for pos=bl to el do
+	dump_string (Printf.sprintf "R%d %s %s %s not\n" pos path secpath df)
+      done) posl
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 2f36c25c59..f6d7baefec 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -23,8 +23,9 @@ val dump_to_dotglob : unit -> unit
 val pause : unit -> unit
 val continue : unit -> unit
 
-val coqdoc_freeze : unit -> Lexer.location_table * int * int
-val coqdoc_unfreeze : Lexer.location_table * int * int -> unit
+type coqdoc_state = Lexer.location_table
+val coqdoc_freeze : unit -> coqdoc_state
+val coqdoc_unfreeze : coqdoc_state -> unit
 
 val add_glob : Util.loc -> Libnames.global_reference -> unit
 val add_glob_kn : Util.loc -> Names.kernel_name -> unit
@@ -34,8 +35,9 @@ val dump_moddef : Util.loc -> Names.module_path -> string -> unit
 val dump_modref  : Util.loc -> Names.module_path -> string -> unit
 val dump_reference  : Util.loc -> string -> string -> string -> unit
 val dump_libref : Util.loc -> Names.dir_path -> string -> unit
-val dump_notation_location : int -> (Notation.notation_location * Topconstr.scope_name option) -> unit
+val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation.notation_location * Topconstr.scope_name option) -> unit
 val dump_binding : Util.loc -> Names.Idset.elt -> unit
+val dump_notation : Util.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit
 val dump_constraint :  Topconstr.typeclass_constraint -> bool -> string -> unit
 val dump_local_binder : Topconstr.local_binder -> bool -> string -> unit
 
diff --git a/interp/notation.ml b/interp/notation.ml
index 39ae278230..bee6c5c931 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -42,7 +42,7 @@ open Ppextend
 
 type level = precedence * tolerability list
 type delimiters = string
-type notation_location = dir_path * string
+type notation_location = (dir_path * dir_path) * string
 
 type scope = {
   notations: (string, interpretation * notation_location) Gmap.t;
@@ -355,7 +355,7 @@ let find_prim_token g loc p sc =
   (* Try for a primitive numerical notation *)
   let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
   check_required_module loc sc spdir;
-  g (interp ()), (dirpath (fst spdir),"")
+  g (interp ()), ((dirpath (fst spdir),empty_dirpath),"")
 
 let interp_prim_token_gen g loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
@@ -536,6 +536,7 @@ type symbol =
 
 let rec string_of_symbol = function
   | NonTerminal _ -> ["_"]
+  | Terminal "_" -> ["'_'"]
   | Terminal s -> [s]
   | SProdList (_,l) ->
      let l = List.flatten (List.map string_of_symbol l) in "_"::l@".."::l@["_"]
diff --git a/interp/notation.mli b/interp/notation.mli
index 3dc3c95c20..d549bb3878 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -65,7 +65,7 @@ val find_delimiters_scope : loc -> delimiters -> scope_name
    negative numbers are not supported, the interpreter must fail with
    an appropriate error message *)
 
-type notation_location = dir_path * string
+type notation_location = (dir_path * dir_path) * string
 type required_module = full_path * string list
 type cases_pattern_status = bool (* true = use prim token in patterns *)
 
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index a20cd1bc23..c0b624110a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1015,9 +1015,17 @@ type 'a module_signature =
   | Enforce of 'a (* ... : T *)
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
 
-let loc_of_notation f loc (args,_) ntn =
-  if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)
-  else snd (Util.unloc (f (List.hd args)))
-
-let ntn_loc = loc_of_notation constr_loc
-let patntn_loc = loc_of_notation cases_pattern_expr_loc
+(* Returns the ranges of locs of the notation that are not occupied by args  *)
+(* and which are them occupied by proper symbols of the notation (or spaces) *)
+
+let locs_of_notation f loc (args,argslist) ntn =
+  let (bl,el) = Util.unloc loc in
+  let rec aux pos = function
+    | [] -> if pos = el then [] else [(pos,el-1)]
+    | a::l ->
+	let ba,ea = Util.unloc (f a) in
+	if pos = ba then aux ea l else (pos,ba-1)::aux ea l
+  in aux bl (args@List.flatten argslist)
+
+let ntn_loc = locs_of_notation constr_loc
+let patntn_loc = locs_of_notation cases_pattern_expr_loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 3b5832f18c..2f25be94c8 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -252,5 +252,8 @@ type 'a module_signature =
   | Enforce of 'a (* ... : T *)
   | Check of 'a list (* ... <: T1 <: T2, possibly empty *)
 
-val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int
-val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int
+val ntn_loc :
+  Util.loc -> constr_expr notation_substitution -> string -> (int * int) list
+val patntn_loc :
+  Util.loc -> cases_pattern_expr notation_substitution -> string ->
+  (int * int) list