diff options
Diffstat (limited to 'tools/coqdoc/index.ml')
| -rw-r--r-- | tools/coqdoc/index.ml | 44 |
1 files changed, 5 insertions, 39 deletions
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index 8170e173..4a5ff592 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Filename -open Lexing open Printf open Cdglobals @@ -36,7 +34,6 @@ type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type -let current_type : entry_type ref = ref Library let current_library = ref "" (** refers to the file being parsed *) @@ -95,9 +92,6 @@ 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 @@ -109,27 +103,6 @@ let head st = | [] -> "" | 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 *) let split_sp s = @@ -158,7 +131,7 @@ let find_external_library logicalpath = let rec aux = function | [] -> raise Not_found | (l,u)::rest -> - if String.length logicalpath > String.length l & + if String.length logicalpath > String.length l && String.sub logicalpath 0 (String.length l + 1) = l ^"." then u else aux rest @@ -208,10 +181,6 @@ let sort_entries el = let display_letter c = if c = '*' then "other" else String.make 1 c -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 -> let ln = !lib_name in @@ -304,9 +273,9 @@ let type_of_string = function | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix" | "ex" | "scheme" -> Definition | "prf" | "thm" -> Lemma - | "ind" | "coind" -> Inductive + | "ind" | "variant" | "coind" -> Inductive | "constr" -> Constructor - | "rec" | "corec" -> Record + | "indrec" | "rec" | "corec" -> Record | "proj" -> Projection | "class" -> Class | "meth" -> Method @@ -319,7 +288,7 @@ let type_of_string = function | "mod" | "modtype" -> Module | "tac" -> TacticDefinition | "sec" -> Section - | s -> raise (Invalid_argument ("type_of_string:" ^ s)) + | s -> invalid_arg ("type_of_string:" ^ s) let ill_formed_glob_file f = eprintf "Warning: ill-formed file %s (links will not be available)\n" f @@ -370,9 +339,6 @@ let read_glob vfile f = done) with _ -> ()) | _ -> - try Scanf.sscanf s "not %d %s %s" - (fun loc sp id -> add_def loc loc (type_of_string "not") sp id) - with Scanf.Scan_failure _ -> try Scanf.sscanf s "%s %d:%d %s %s" (fun ty loc1 loc2 sp id -> add_def loc1 loc2 (type_of_string ty) sp id) |