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

1 files changed, 23 insertions, 15 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a75ee2a7d..06b751c5f 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -867,7 +867,7 @@ let compute_syntax_data (df,modifiers) =
   let typs = List.map (set_entry_type etyps) typs in
   let prec = (n,List.map (assoc_of_type n) typs) in
   let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in
-  let df' = (Lib.library_dp(),df) in
+  let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
   let i_data = (onlyparse,extrarecvars,recvars,vars,(ntn_for_interp,df')) in
   (i_data,sy_data)
 
@@ -974,7 +974,8 @@ let add_notation_in_scope local df c mods scope =
   let (acvars,ac) = interp_aconstr (vars,recvars) c in
   let a = (remove_extravars extrarecvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
-  Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
+  Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
+  df'
 
 let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse =
   let dfs = split_notation_string df in
@@ -985,55 +986,62 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
     Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules))
   end;
   (* Declare interpretation *)
-  let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in
+  let path = (Lib.library_dp(),Lib.current_dirpath true) in
+  let df' = (make_notation_key symbs,(path,df)) in
   let (acvars,ac) = interp_aconstr ~impls (vars,recvars) c in
   let a = (remove_extravars extrarecvars acvars,ac) in
   let onlyparse = onlyparse or is_not_printable ac in
-  Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'))
+  Lib.add_anonymous_leaf (inNotation (local,scope,a,onlyparse,df'));
+  df'
 
 (* Notations without interpretation (Reserved Notation) *)
 
-let add_syntax_extension local mv =
-  let (_,sy_data) = compute_syntax_data mv in
+let add_syntax_extension local ((loc,df),mods) =
+  let (_,sy_data) = compute_syntax_data (df,mods) in
   let sy_rules = make_syntax_rules sy_data in
   Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
 
 (* Notations with only interpretation *)
 
-let add_notation_interpretation (df,c,sc) =
-  add_notation_interpretation_core false df c sc false
+let add_notation_interpretation ((loc,df),c,sc) =
+  let df' = add_notation_interpretation_core false df c sc false in
+  Dumpglob.dump_notation (loc,df') sc true
 
-let set_notation_for_interpretation impls (df,c,sc) =
-  (try silently (add_notation_interpretation_core false df ~impls c sc) false;
+let set_notation_for_interpretation impls ((_,df),c,sc) =
+  (try ignore
+    (silently (add_notation_interpretation_core false df ~impls c sc) false);
   with NoSyntaxRule ->
     error "Parsing rule for this notation has to be previously declared.");
   Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
 
 (* Main entry point *)
 
-let add_notation local c (df,modifiers) sc =
-  if no_syntax_modifiers modifiers then
+let add_notation local c ((loc,df),modifiers) sc =
+  let df' =
+   if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
     let onlyparse = modifiers=[SetOnlyParsing] in
     try add_notation_interpretation_core local df c sc onlyparse
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
       add_notation_in_scope local df c modifiers sc
-  else
+   else
     (* Declare both syntax and interpretation *)
     add_notation_in_scope local df c modifiers sc
+  in
+  Dumpglob.dump_notation (loc,df') sc true
 
 (* Infix notations *)
 
 let inject_var x = CRef (Ident (dummy_loc, id_of_string x))
 
-let add_infix local (inf,modifiers) pr sc =
+let add_infix local ((loc,inf),modifiers) pr sc =
   check_infix_modifiers modifiers;
   (* check the precedence *)
   let metas = [inject_var "x"; inject_var "y"] in
   let c = mkAppC (pr,metas) in
   let df = "x "^(quote_notation_token inf)^" y" in
-  add_notation local c (df,modifiers) sc
+  add_notation local c ((loc,df),modifiers) sc
 
 (**********************************************************************)
 (* Delimiters and classes bound to scopes                             *)