Merge commit 'upstream/8.0pl3+8.1beta' into 8.1

1 files changed, 141 insertions, 56 deletions

diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index ec89da2f..9b5716ff 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: index.mll 8617 2006-03-08 10:47:12Z notin $ i*)
+(*i $Id: index.mll 8863 2006-05-26 10:33:21Z notin $ i*)
 
 {
 
@@ -34,11 +34,14 @@ type index_entry =
   | Ref of coq_module * string
   | Mod of coq_module * string
 
-let table = Hashtbl.create 97
+let current_type = ref Library
+let current_library = ref ""
+  (** referes to the file being parsed *)
 
-let current_module = ref ""
+let table = Hashtbl.create 97
+  (** [table] is used to store references and definitions *)
 
-let add_def loc ty id = Hashtbl.add table (!current_module, loc) (Def (id, ty))
+let add_def loc ty id = Hashtbl.add table (!current_library, loc) (Def (id, ty))
 
 let add_ref m loc m' id = Hashtbl.add table (m, loc) (Ref (m', id))
 
@@ -46,7 +49,55 @@ let add_mod m loc m' id = Hashtbl.add table (m, loc) (Mod (m', id))
 
 let find m l = Hashtbl.find table (m, l)
 
-let current_type = ref Library
+
+(*s Manipulating path prefixes *) 
+
+type stack = string list 
+
+let rec string_of_stack st =
+  match st with
+    | [] -> ""
+    | x::[] -> x
+    | x::tl -> (string_of_stack tl) ^ "." ^ x
+
+let empty_stack = []
+
+let module_stack = ref empty_stack
+let section_stack = ref empty_stack
+
+let init_stack () =
+  module_stack := empty_stack; section_stack := empty_stack
+
+let push st p = st := p::!st
+let pop st = 
+  match !st with 
+    | [] -> ()
+    | _::tl -> st := tl
+	
+let head st =
+  match st with
+    | [] -> ""
+    | x::_ -> x
+
+let begin_module m = push module_stack m
+let begin_section s = push section_stack s
+
+let end_block id =
+  (** determines if it ends a module or a section and pops the stack *)
+  if ((String.compare (head !module_stack) id ) == 0) then
+    pop module_stack
+  else if ((String.compare (head !section_stack) id) == 0) then
+    pop section_stack
+  else
+    ()
+
+let make_fullid id = 
+  (** prepends the current module path to an id *)
+  let path = string_of_stack !module_stack in
+    if String.length path > 0 then
+      path ^ "." ^ id
+    else 
+      id
 
 (* Coq modules *)
 
@@ -83,7 +134,7 @@ let ref_module loc s =
     let n = String.length s in
     let i = String.rindex s ' ' in 
     let id = String.sub s (i+1) (n-i-1) in
-    add_mod !current_module (loc+i+1) (Hashtbl.find modules id) id
+      add_mod !current_library (loc+i+1) (Hashtbl.find modules id) id
   with Not_found -> 
     ()
 
@@ -104,25 +155,25 @@ let compare_entries (s1,_) (s2,_) = Alpha.compare_string s1 s2
 
 let sort_entries el =
   let t = Hashtbl.create 97 in
-  List.iter 
-    (fun c -> Hashtbl.add t c [])
-    ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N'; 
-     'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];  
-  List.iter 
-    (fun ((s,_) as e) -> 
-       let c = Alpha.norm_char s.[0] in 
-       let l = try Hashtbl.find t c with Not_found -> [] in
-       Hashtbl.replace t c (e :: l)) 
-    el;
-  let res = ref [] in
-  Hashtbl.iter 
-    (fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
-  List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res
-    
+    List.iter 
+      (fun c -> Hashtbl.add t c [])
+      ['A'; 'B'; 'C'; 'D'; 'E'; 'F'; 'G'; 'H'; 'I'; 'J'; 'K'; 'L'; 'M'; 'N'; 
+       'O'; 'P'; 'Q'; 'R'; 'S'; 'T'; 'U'; 'V'; 'W'; 'X'; 'Y'; 'Z'; '_'];  
+    List.iter 
+      (fun ((s,_) as e) -> 
+	 let c = Alpha.norm_char s.[0] in 
+	 let l = try Hashtbl.find t c with Not_found -> [] in
+	   Hashtbl.replace t c (e :: l)) 
+      el;
+    let res = ref [] in
+      Hashtbl.iter 
+	(fun c l -> res := (c, List.sort compare_entries l) :: !res) t;
+      List.sort (fun (c1,_) (c2,_) -> Alpha.compare_char c1 c2) !res
+	
 let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
-
+  
 let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
-
+  
 let type_name = function
   | Library -> "library"
   | Module -> "module"
@@ -133,28 +184,28 @@ let type_name = function
   | Variable -> "variable"
   | Axiom -> "axiom"
   | TacticDefinition -> "tactic"
-
+      
 let all_entries () =
   let gl = ref [] in
   let add_g s m t = gl := (s,(m,t)) :: !gl in
   let bt = Hashtbl.create 11 in
   let add_bt t s m =
     let l = try Hashtbl.find bt t with Not_found -> [] in
-    Hashtbl.replace bt t ((s,m) :: l)
+      Hashtbl.replace bt t ((s,m) :: l)
   in
   let classify (m,_) e = match e with 
     | Def (s,t) -> add_g s m t; add_bt t s m
     | Ref _ | Mod _ -> ()
   in
-  Hashtbl.iter classify table;
-  Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
-  { idx_name = "global"; 
-    idx_entries = sort_entries !gl; 
-    idx_size = List.length !gl },
-  Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; 
+    Hashtbl.iter classify table;
+    Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules;
+    { idx_name = "global"; 
+      idx_entries = sort_entries !gl; 
+      idx_size = List.length !gl },
+    Hashtbl.fold (fun t e l -> (t, { idx_name = type_name t; 
 				   idx_entries = sort_entries e; 
 				   idx_size = List.length e }) :: l) bt []
-
+    
 }
 
 (*s Shortcuts for regular expressions. *)
@@ -165,15 +216,14 @@ let firstchar =
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255']
 let identchar = 
   ['$' 'A'-'Z' 'a'-'z' '_' '\192'-'\214' '\216'-'\246' '\248'-'\255' 
-   '\'' '0'-'9']
-let ident = 
-  firstchar identchar*
+     '\'' '0'-'9']
+let ident = firstchar identchar*
 
 let begin_hide = "(*" space* "begin" space+ "hide" space* "*)"
 let end_hide = "(*" space* "end" space+ "hide" space* "*)"
-
+  
 (*s Indexing entry point. *)
-
+  
 rule traverse = parse
   | "Definition" space
       { current_type := Definition; index_ident lexbuf; traverse lexbuf }
@@ -192,13 +242,15 @@ rule traverse = parse
   | "Record" space
       { current_type := Inductive; index_ident lexbuf; traverse lexbuf }
   | "Module" (space+ "Type")? space
-      { current_type := Module; index_ident lexbuf; traverse lexbuf }
+      { current_type := Module; module_ident lexbuf; traverse lexbuf }
 (*i***
   | "Variable" 's'? space
       { current_type := Variable; index_idents lexbuf; traverse lexbuf }
 ***i*)
   | "Require" (space+ ("Export"|"Import"))? space+ ident
       { ref_module (lexeme_start lexbuf) (lexeme lexbuf); traverse lexbuf }
+  | "End" space+ 
+      { end_ident lexbuf; traverse lexbuf }
   | begin_hide 
       { skip_hide lexbuf; traverse lexbuf }
   | "(*" 
@@ -216,7 +268,16 @@ and index_ident = parse
   | space+ 
       { index_ident lexbuf }
   | ident  
-      { add_def (lexeme_start lexbuf) !current_type (lexeme lexbuf) }
+      { let fullid = 
+	  let id = lexeme lexbuf in
+	    match !current_type with
+	      | Definition
+	      | Inductive
+	      | Constructor 
+	      | Lemma -> make_fullid id
+	      | _ -> id 
+	in 
+	  add_def (lexeme_start lexbuf) !current_type fullid }
   | eof    
       { () }
   | _      
@@ -234,12 +295,12 @@ and index_idents = parse
       { () }
   | _
       { skip_until_point lexbuf }
-
+      
 (*s Index identifiers in an inductive definition (types and constructors). *)
-
+      
 and inductive = parse
   | '|' | ":=" space* '|'? 
-      { current_type := Constructor; index_ident lexbuf; inductive lexbuf }
+	{ current_type := Constructor; index_ident lexbuf; inductive lexbuf }
   | "with" space
       { current_type := Inductive; index_ident lexbuf; inductive lexbuf }
   | '.'    
@@ -248,9 +309,9 @@ and inductive = parse
       { () }
   | _      
       { inductive lexbuf }
-
+      
 (*s Index identifiers in a Fixpoint declaration. *)
-
+      
 and fixpoint = parse
   | "with" space
       { index_ident lexbuf; fixpoint lexbuf }
@@ -260,9 +321,9 @@ and fixpoint = parse
       { () }
   | _      
       { fixpoint lexbuf }
-
+      
 (*s Skip a possibly nested comment. *)
-
+      
 and comment = parse
   | "*)" { () }
   | "(*" { comment lexbuf; comment lexbuf }
@@ -271,25 +332,48 @@ and comment = parse
   | _    { comment lexbuf }
 
 (*s Skip a constant string. *)
-
+      
 and string = parse
   | '"'  { () }
   | eof  { eprintf " *** Unterminated string while indexing" }
   | _    { string lexbuf }
 
 (*s Skip everything until the next dot. *)
-
+      
 and skip_until_point = parse
   | '.'  { () }
   | eof  { () }
   | _    { skip_until_point lexbuf }
-
+      
 (*s Skip everything until [(* end hide *)] *)
 
 and skip_hide = parse
   | eof | end_hide { () }
   | _ { skip_hide lexbuf }
 
+and end_ident = parse
+  | space+ 
+      { end_ident lexbuf }
+  | ident  
+      { let id = lexeme lexbuf in end_block id }
+  | eof    
+      { () }
+  | _      
+      { () }
+
+and module_ident = parse
+  | space+
+      { module_ident lexbuf }
+  | ident space* ":="
+      { () }
+  | ident
+      { let id = lexeme lexbuf in
+	  begin_module id; add_def (lexeme_start lexbuf) !current_type id }
+  | eof
+      { () }
+  | _
+      { () }
+
 {
   
   let read_glob f = 
@@ -306,10 +390,11 @@ and skip_hide = parse
 	    | 'R' ->
 		(try
 		   let i = String.index s ' ' in
+		   let j = String.index_from s (i+1) ' ' in 
 		   let loc = int_of_string (String.sub s 1 (i - 1)) in
-		   let sp = String.sub s (i + 1) (n - i - 1) in
-		   let m',id = split_sp sp in
-		   add_ref !cur_mod loc m' id
+		   let lib_dp = String.sub s (i + 1) (j - i - 1) in
+		   let full_id = String.sub s (j + 1) (n - j - 1) in
+		     add_ref !cur_mod loc lib_dp full_id
 		 with Not_found -> 
 		   ())
 	    | _ -> ()
@@ -317,11 +402,11 @@ and skip_hide = parse
       done
     with End_of_file -> 
       close_in c
-
+	
   let scan_file f m = 
-    current_module := m;
+    init_stack (); current_library := m;
     let c = open_in f in
     let lb = from_channel c in
-    traverse lb;
-    close_in c
+      traverse lb;
+      close_in c
 }