diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /tools/coqdoc | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'tools/coqdoc')
-rw-r--r-- | tools/coqdoc/index.ml | 16 | ||||
-rw-r--r-- | tools/coqdoc/index.mli | 2 | ||||
-rw-r--r-- | tools/coqdoc/output.ml | 6 |
3 files changed, 14 insertions, 10 deletions
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index df493fdf..724d3838 100644 --- a/tools/coqdoc/index.ml +++ b/tools/coqdoc/index.ml @@ -77,7 +77,7 @@ let add_ref m loc m' sp id ty = let find m l = Hashtbl.find reftable (m, l) -let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) +let find_string s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t) (* Coq modules *) @@ -185,7 +185,8 @@ let type_name = function let prepare_entry s = function | Notation -> (* We decode the encoding done in Dumpglob.cook_notation of coqtop *) - (* Encoded notations have the form section:sc:x_'++'_x where: *) + (* Encoded notations have the form section:entry:sc:x_'++'_x *) + (* where: *) (* - the section, if any, ends with a "." *) (* - the scope can be empty *) (* - tokens are separated with "_" *) @@ -202,10 +203,12 @@ let prepare_entry s = function let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in let h = try String.index_from s 0 ':' with _ -> err () in let i = try String.index_from s (h+1) ':' with _ -> err () in - let sc = String.sub s (h+1) (i-h-1) in - let ntn = Bytes.make (String.length s - i) ' ' in + let m = try String.index_from s (i+1) ':' with _ -> err () in + let entry = String.sub s (h+1) (i-h-1) in + let sc = String.sub s (i+1) (m-i-1) in + let ntn = Bytes.make (String.length s - m) ' ' in let k = ref 0 in - let j = ref (i+1) in + let j = ref (m+1) in let quoted = ref false in let l = String.length s - 1 in while !j <= l do @@ -227,7 +230,8 @@ let prepare_entry s = function incr j done; let ntn = Bytes.sub_string ntn 0 !k in - if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" + let ntn = if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" in + if entry = "" then ntn else entry ^ ":" ^ ntn | _ -> s diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 5cd30138..7c9aad67 100644 --- a/tools/coqdoc/index.mli +++ b/tools/coqdoc/index.mli @@ -41,7 +41,7 @@ type index_entry = 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 find_string : string -> index_entry val add_module : coq_module -> unit diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index d2522700..750698a1 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -76,7 +76,7 @@ let is_tactic = [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection"; "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct"; - "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto"; + "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "info_auto"; "info_eauto"; "quote"; "eexact"; "autorewrite"; "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality"; "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega"; @@ -431,7 +431,7 @@ module Latex = struct else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then try - let tag = Index.find_string (get_module false) s in + let tag = Index.find_string s in reference (translate s) tag with _ -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s @@ -706,7 +706,7 @@ module Html = struct else if is_keyword s then printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then - try reference (translate s) (Index.find_string (get_module false) s) + try reference (translate s) (Index.find_string s) with Not_found -> Tokens.output_tagged_ident_string s else Tokens.output_tagged_ident_string s |