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, 5 insertions, 5 deletions

diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 3649d6a4a..517ec97a7 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -52,13 +52,9 @@ val init_coqlib_library : unit -> unit
 
 val add_external_library : string -> coq_module -> unit
 
-(*s Scan identifiers introductions from a file *)
-
-val scan_file : string -> coq_module -> unit
-
 (*s Read globalizations from a file (produced by coqc -dump-glob) *)
 
-val read_glob : string -> coq_module
+val read_glob : string -> unit
 
 (*s Indexes *)
 
@@ -69,6 +65,10 @@ type 'a index = {
 
 val current_library : string ref
 
+val display_letter : char -> string
+
+val prepare_entry : string -> entry_type -> string
+
 val all_entries : unit ->
       (coq_module * entry_type) index *
       (entry_type * coq_module index) list