diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqdoc/index.mll | 31 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 2 |
2 files changed, 21 insertions, 12 deletions
diff --git a/tools/coqdoc/index.mll b/tools/coqdoc/index.mll index 2e2804cf2..290c77fcb 100644 --- a/tools/coqdoc/index.mll +++ b/tools/coqdoc/index.mll @@ -129,15 +129,6 @@ let find_module m = else Unknown -let ref_module loc s = - try - 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_library (loc+i+1) (Hashtbl.find modules id) id - with Not_found -> - () - (* Building indexes *) type 'a index = { @@ -251,8 +242,8 @@ rule traverse = parse | "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 } + | "Require" (space+ ("Export"|"Import"))? + { module_refs lexbuf; traverse lexbuf } | "End" space+ { end_ident lexbuf; traverse lexbuf } | begin_hide @@ -379,6 +370,24 @@ and module_ident = parse | _ { () } +(*s parse module names *) + +and module_refs = parse + | space+ + { 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 -> () + ); + module_refs lexbuf } + | eof + { () } + | _ + { () } + { let read_glob f = diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 3e171a2c5..5a5f1e7bf 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -37,7 +37,7 @@ let is_keyword = "Hypothesis"; "Hypotheses"; "Immediate"; "Implicit"; "Import"; "Inductive"; "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac"; - "Module"; "Module Type"; "Declare Module"; + "Module"; "Module Type"; "Declare Module"; "Include"; "Mutual"; "Parameter"; "Parameters"; "Print"; "Proof"; "Qed"; "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem"; |