diff options
Diffstat (limited to 'tools/coqdoc/index.mli')
| -rw-r--r-- | tools/coqdoc/index.mli | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 56a3cd11..517ec97a 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -6,13 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: index.mli 11576 2008-11-10 19:13:15Z msozeau $ i*) +(*i $Id$ i*) open Cdglobals type loc = int -type entry_type = +type entry_type = | Library | Module | Definition @@ -33,7 +33,7 @@ type entry_type = val type_name : entry_type -> string -type index_entry = +type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type | Mod of coq_module * string @@ -44,28 +44,32 @@ val find_string : coq_module -> string -> index_entry val add_module : coq_module -> unit -type module_kind = Local | Coqlib | Unknown +type module_kind = Local | External of coq_module | Unknown val find_module : coq_module -> module_kind -(*s Scan identifiers introductions from a file *) +val init_coqlib_library : unit -> unit -val scan_file : string -> coq_module -> unit +val add_external_library : 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 *) -type 'a index = { +type 'a index = { idx_name : string; idx_entries : (char * (string * 'a) list) list; idx_size : int } val current_library : string ref -val all_entries : unit -> +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 |