## Lines starting with '## ' will be removed from the log message.

## File(s) to commit:
## tools/coqdoc/index.mll
## tools/coqdoc/output.ml
## tools/coqdoc/pretty.mll
Various improvements to coqdoc:
- (Hopefully) better handling of brackets and notations like \in
(debugger with Stéphane Lescuyer).
- More indexed tactics and commands.
- Fix bug(?) in parsing of "[[" comments.
- Better interpolation of module and library names.


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

3 files changed, 36 insertions, 29 deletions

diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll
index b41c19ac3..f83b1212e 100644
--- a/tools/coqdoc/index.mll
+++ b/tools/coqdoc/index.mll
@@ -70,12 +70,14 @@ let add_def loc ty sp id =
     
 let add_ref m loc m' sp id ty = 
   if Hashtbl.mem reftable (m, loc) then ()
-  else
-    Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty))
+  else Hashtbl.add reftable (m, loc) (Ref (m', full_ident sp id, ty));
+  let idx = if id = "<>" then m' else id in
+    if Hashtbl.mem deftable idx then ()
+    else Hashtbl.add deftable idx (Ref (m', full_ident sp id, ty))  
     
 let add_mod m loc m' id = 
   Hashtbl.add reftable (m, loc) (Mod (m', id));
-  Hashtbl.add deftable id (Mod (m', id))
+  Hashtbl.add deftable m (Mod (m', id))
     
 let find m l = Hashtbl.find reftable (m, l)
   
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2d547af79..34c993296 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -32,7 +32,7 @@ let build_table l =
 
 let is_keyword = 
   build_table
-    [ "AddPath"; "Axiom"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
+    [ "AddPath"; "Axiom"; "Abort"; "Chapter"; "Check"; "Coercion"; "CoFixpoint";
       "CoInductive"; "Corollary"; "Defined"; "Definition"; "End"; "Eval"; "Example"; 
       "Export"; "Fact"; "Fix"; "Fixpoint"; "Global"; "Grammar"; "Goal"; "Hint";
       "Hypothesis"; "Hypotheses"; 
@@ -42,27 +42,31 @@ let is_keyword =
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; 
-      "Set"; "Types"; "Unset"; "Variable"; "Variables"; "Context";
+      "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; 
       "Boxed"; "Unboxed"; "Inline";
       "Arguments"; "Add"; "Strict";
       "Typeclasses"; "Instance"; "Class"; "Instantiation";
+      "subgoal";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
-      "Program Instance";
+      "Program Instance"; "Equations"; "Equations_nocomp";
       (*i (* coq terms *) *)
       "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "dest"; "fun"; 
-      "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"
+      "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
+      (* Ltac *)
+      "before"; "after"
        ]
 
 let is_tactic = 
   build_table
-    [ "intro"; "intros"; "apply"; "rewrite"; "setoid_rewrite";
-      "destruct"; "induction"; "elim"; "dependent"; 
-      "generalize"; "clear"; "rename"; "move"; "set"; "assert";
-      "cut"; "assumption"; "exact"; "split"; "try"; "discriminate";
+    [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "injection";
+      "elimtype"; "progress"; "setoid_rewrite";
+      "destruct"; "destruction"; "destruct_call"; "induction"; "elim"; "dependent"; 
+      "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "clear"; "rename"; "move"; "set"; "assert";
+      "cut"; "assumption"; "exact"; "split"; "subst"; "try"; "discriminate";
       "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index fc40a97c5..d38a09bd6 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -190,17 +190,24 @@ let pfx_id = (id '.')*
 let identifier = 
   id | pfx_id id
 
-let symbolchar_no_brackets =
-  ['!' '$' '%' '&' '*' '+' ',' '@' '^' '#'
-   '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~'
-   '{' '}' '(' ')'] |
+let symbolchar_symbol_no_brackets =
+  ['!' '$' '%' '&' '*' '+' ',' '^' '#'
+      '\\' '/' '-' '<' '>' '|' ':' '?' '=' '~' ] |
   (* utf-8 symbols *) 
   '\226' ['\134'-'\143' '\152'-'\155' '\164'-'\165' '\168'-'\171'] _
+let symbolchar_no_brackets = symbolchar_symbol_no_brackets | 
+    [ '@' '{' '}' '(' ')' 'A'-'Z' 'a'-'z' '_']
 let symbolchar = symbolchar_no_brackets | '[' | ']'
-let token_no_brackets = symbolchar_no_brackets+
-let token = symbolchar+ | '[' [^ '[' ']' ':']* ']'
+let token_no_brackets = symbolchar_symbol_no_brackets symbolchar_no_brackets*
+let token = symbolchar_symbol_no_brackets symbolchar* | '[' [^ '[' ']' ':']* ']'
 let printing_token = (token | id)+
 
+(* tokens with balanced brackets *)
+let token_brackets =
+  ( token_no_brackets ('[' token_no_brackets? ']')* 
+  | token_no_brackets? ('[' token_no_brackets? ']')+ )
+  token_no_brackets?
+
 let thm_token = 
   "Theorem" 
   | "Lemma" 
@@ -226,6 +233,7 @@ let def_token =
   | "Scheme"
   | "Inductive"
   | "CoInductive"
+  | "Equations"
 
 let decl_token = 
   "Hypothesis" 
@@ -313,12 +321,6 @@ let gallina_kw_to_hide =
   | "Declare" space+ ("Left" | "Right") space+ "Step" 
 
 
-(* tokens with balanced brackets *)
-let token_brackets =
-  ( symbolchar_no_brackets+ ('[' symbolchar_no_brackets* ']')* 
-  | symbolchar_no_brackets* ('[' symbolchar_no_brackets* ']')+ )
-  symbolchar_no_brackets*
-
 let section = "*" | "**" | "***" | "****"
 
 let item_space = "    "
@@ -525,16 +527,15 @@ and doc_bol = parse
 and doc = parse
   | nl
       { Output.char '\n'; doc_bol lexbuf }
-  | "["
-      { brackets := 1; 
-	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
-	doc lexbuf }
-  | "[[" nl space*
+  | "[[" nl
       { formatted := true; Output.line_break (); Output.start_inline_coq ();
-	Output.indentation (fst (count_spaces (lexeme lexbuf))); 
 	let eol = body_bol lexbuf in 
 	  Output.end_inline_coq (); formatted := false;
 	  if eol then doc_bol lexbuf else doc lexbuf}
+  | "["
+      { brackets := 1; 
+	Output.start_inline_coq (); escaped_coq lexbuf; Output.end_inline_coq ();
+	doc lexbuf }
   | '*'* "*)" space* nl
       { true }
   | '*'* "*)"