From bf12eb93f3f6a6a824a10878878fadd59745aae0 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sat, 29 Dec 2012 10:57:43 +0100 Subject: Imported Upstream version 8.4pl1dfsg --- tools/coqdoc/index.ml | 34 +++++++++++++++----------------- tools/coqdoc/index.mli | 3 ++- tools/coqdoc/output.ml | 53 +++++++++++++++++--------------------------------- 3 files changed, 36 insertions(+), 54 deletions(-) (limited to 'tools/coqdoc') diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index d319ce72..14447b06 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -35,17 +35,18 @@ type entry_type = type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type - | Mod of coq_module * string let current_type : entry_type ref = ref Library let current_library = ref "" (** refers to the file being parsed *) -(** [deftable] stores only definitions and is used to interpolate idents - inside comments, which are not globalized otherwise. *) - +(** [deftable] stores only definitions and is used to build the index *) let deftable = Hashtbl.create 97 +(** [byidtable] is used to interpolate idents inside comments, which are not + globalized otherwise. *) +let byidtable = Hashtbl.create 97 + (** [reftable] stores references and definitions *) let reftable = Hashtbl.create 97 @@ -59,25 +60,25 @@ let full_ident sp id = else "" let add_def loc1 loc2 ty sp id = + let fullid = full_ident sp id in + let def = Def (fullid, ty) in for loc = loc1 to loc2 do - Hashtbl.add reftable (!current_library, loc) (Def (full_ident sp id, ty)) + Hashtbl.add reftable (!current_library, loc) def done; - Hashtbl.add deftable id (Def (full_ident sp id, ty)) + Hashtbl.add deftable !current_library (fullid, ty); + Hashtbl.add byidtable id (!current_library, fullid, ty) let add_ref m loc m' sp id ty = + let fullid = full_ident sp id in 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', fullid, 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 m (Mod (m', id)) + if Hashtbl.mem byidtable idx then () + else Hashtbl.add byidtable idx (m', fullid, ty) let find m l = Hashtbl.find reftable (m, l) -let find_string m s = Hashtbl.find deftable s +let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) (*s Manipulating path prefixes *) @@ -289,10 +290,7 @@ let all_entries () = let l = try Hashtbl.find bt t with Not_found -> [] in 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 + let classify m (s,t) = (add_g s m t; add_bt t s m) in Hashtbl.iter classify deftable; Hashtbl.iter (fun id m -> add_g id m Library; add_bt Library id m) modules; { idx_name = "global"; diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 8c658a90..0f62a086 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -34,10 +34,11 @@ val type_name : entry_type -> string type index_entry = | Def of string * entry_type | Ref of coq_module * string * entry_type - | Mod of coq_module * string +(* Find what symbol coqtop said is located at loc in the source file *) val find : coq_module -> loc -> index_entry +(* Find what data is referred to by some string in some coq module *) val find_string : coq_module -> string -> index_entry val add_module : coq_module -> unit diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index cd33528a..0dc86bc8 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -126,9 +126,12 @@ let initialize_texmacs () = let token_tree_texmacs = ref (initialize_texmacs ()) +let token_tree_latex = ref Tokens.empty_ttree +let token_tree_html = ref Tokens.empty_ttree + let initialize_tex_html () = let if_utf8 = if !Cdglobals.utf8 then fun x -> Some x else fun _ -> None in - List.fold_right (fun (s,l,l') (tt,tt') -> + let (tree_latex, tree_html) = List.fold_right (fun (s,l,l') (tt,tt') -> (Tokens.ttree_add tt s l, match l' with None -> tt' | Some l' -> Tokens.ttree_add tt' s l')) [ "*" , "\\ensuremath{\\times}", if_utf8 "×"; @@ -151,10 +154,9 @@ let initialize_tex_html () = "Π", "\\ensuremath{\\Pi}", if_utf8 "Π"; "λ", "\\ensuremath{\\lambda}", if_utf8 "λ"; (* "fun", "\\ensuremath{\\lambda}" ? *) - ] (Tokens.empty_ttree,Tokens.empty_ttree) - -let token_tree_latex = ref (fst (initialize_tex_html ())) -let token_tree_html = ref (snd (initialize_tex_html ())) + ] (Tokens.empty_ttree,Tokens.empty_ttree) in + token_tree_latex := tree_latex; + token_tree_html := tree_html let add_printing_token s (t1,t2) = (match t1 with None -> () | Some t1 -> @@ -325,9 +327,6 @@ module Latex = struct let space = 0.5 *. (float n) in printf "\\coqdocindent{%2.2fem}\n" space - let module_ref m s = - printf "\\coqdocmodule{%s}{%s}" m (escaped s) - let ident_ref m fid typ s = let id = if fid <> "" then (m ^ "." ^ fid) else m in match find_module m with @@ -356,12 +355,8 @@ module Latex = struct let reference s = function | Def (fullid,typ) -> defref (get_module false) fullid typ s - | Mod (m,s') when s = s' -> - module_ref m s | Ref (m,fullid,typ) -> ident_ref m fullid typ s - | Mod _ -> - printf "\\coqdocvar{%s}" (escaped s) (*s The sublexer buffers symbol characters and attached uninterpreted ident and try to apply special translation such as, @@ -389,6 +384,7 @@ module Latex = struct last_was_in := false let initialize () = + initialize_tex_html (); Tokens.token_tree := token_tree_latex; Tokens.outfun := output_sublexer_string @@ -534,10 +530,7 @@ module Html = struct end let trailer () = - if !index && (get_module false) <> "Index" then - printf "\n\n
\n
Index" !index_name; - if !header_trailer then - if !footer_file_spec then + if !header_trailer && !footer_file_spec then let cin = Pervasives.open_in !footer_file in try while true do @@ -545,12 +538,14 @@ module Html = struct printf "%s\n" s done with End_of_file -> Pervasives.close_in cin - else - begin - printf "
This page has been generated by "; - printf "coqdoc\n" Coq_config.wwwcoq; - printf "
\n\n\n\n\n" - end + else + begin + if !index && (get_module false) <> "Index" then + printf "\n\n
\n
Index" !index_name; + printf "
This page has been generated by "; + printf "coqdoc\n" Coq_config.wwwcoq; + printf "
\n\n\n\n\n" + end let start_module () = let ln = !lib_name in @@ -620,15 +615,6 @@ module Html = struct | Some n -> n | None -> addr) - let module_ref m s = - match find_module m with - | Local -> - printf "%s" m s - | External m when !externals -> - printf "%s" m s - | External _ | Unknown -> - output_string s - let ident_ref m fid typ s = match find_module m with | Local -> @@ -645,12 +631,8 @@ module Html = struct | Def (fullid,ty) -> printf "" fullid; printf "%s" (type_name ty) s - | Mod (m,s') when s = s' -> - module_ref m s | Ref (m,fullid,ty) -> ident_ref m fullid (type_name ty) s - | Mod _ -> - printf "%s" s let output_sublexer_string doescape issymbchar tag s = let s = if doescape then escaped s else s in @@ -667,6 +649,7 @@ module Html = struct Tokens.output_tagged_symbol_char tag c let initialize () = + initialize_tex_html(); Tokens.token_tree := token_tree_html; Tokens.outfun := output_sublexer_string -- cgit v1.2.3