Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisation (add_glob* et dump_*)

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

3 files changed, 17 insertions, 16 deletions

diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index ab23f2210..e4d464236 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -238,7 +238,9 @@ let firstchar =
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
      '\'' '0'-'9']
-let ident = firstchar identchar*
+let id = firstchar identchar*
+let pfx_id = (id '.')*
+let ident = id | pfx_id id
 
 let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
 let end_hide = "(*" space* "end" space+ "hide" space* "*)"
@@ -405,10 +407,11 @@ and module_refs = parse
       { module_refs lexbuf }
   | ident  
       { let id =  lexeme lexbuf in
-	  (try
-	      add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
-	    with
-		Not_found -> ()
+	  (Printf.eprintf "DEBUG: id = %s\n" id; 
+	   try
+	     add_mod !current_library (lexeme_start lexbuf) (Hashtbl.find modules id) id
+	   with
+	       Not_found -> ()
 	  ); 
 	module_refs lexbuf }
   | eof    
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 0522bbac0..a75b7196d 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -417,17 +417,14 @@ module Html = struct
   let stop_verbatim () = printf "</pre>\n"
 
   let module_ref m s = 
-    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    (*i
     match find_module m with
-    | Local ->
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib when !externals ->
-	let m = Filename.concat !coqlib m in
-	printf "<a href=\"%s.html\">" m; raw_ident s; printf "</a>"
-    | Coqlib | Unknown ->
-	raw_ident s
-    i*)
+      | Local ->
+	  printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
+      | Coqlib when !externals ->
+	  let m = Filename.concat !coqlib m in
+	    printf "<a class=\"modref\" href=\"%s.html\">" m; raw_ident s; printf "</a>"
+      | Coqlib | Unknown ->
+	  raw_ident s
 
   let ident_ref m fid s = 
     match find_module m with
@@ -446,6 +443,7 @@ module Html = struct
       printf "</span>"
     end else 
       begin
+	Printf.eprintf "DEBUG: looking for (%s, %d)\n" !current_module loc;
 	try
 	  (match Index.find !current_module loc with
 	     | Def (fullid,_) -> 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index d78aabbf9..b2fa915b6 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -639,7 +639,7 @@ and notation_bol = parse
 
 and notation = parse
   | nl { Output.line_break(); notation_bol lexbuf }
-  | '"' { Output.char '"'; false }
+  | '"' { Output.char '"'}
   | token
       { let s = lexeme lexbuf in
 	  Output.symbol s; notation lexbuf }