diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-14 23:19:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-07-15 11:40:25 +0200 |
| commit | 7b88d786d16c54fe8ad2d0802a1551bfc9265b9e (patch) | |
| tree | eac687184adf40091652e0b747cea34e706c914d /tools/coqdoc | |
| parent | e3eb17a728d7b6874e67462e8a83fac436441872 (diff) | |
Fixing #5648 (too early decision of tagging ident as keyword in html coqdoc).
Fix proposed by the reporter, Vincent Laporte.
Note that for LaTeX output, the selection of a keyword was already
done after checking if the ident is recognized as a Coq ident by
coqtop.
Incidentally, being now explicit on an wildcard-catching of exceptions.
Diffstat (limited to 'tools/coqdoc')
| -rw-r--r-- | tools/coqdoc/output.ml | 34 |
1 files changed, 15 insertions, 19 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 5c0d2a39b..d043c4a58 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -693,25 +693,21 @@ module Html = struct printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) let ident s loc = - if is_keyword s then begin - printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s) - end else begin - try - match loc with - | None -> raise Not_found - | Some loc -> - reference (translate s) (Index.find (get_module false) loc) - with Not_found -> - if is_tactic s then - printf "<span class=\"id\" title=\"tactic\">%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) - with _ -> Tokens.output_tagged_ident_string s - else - Tokens.output_tagged_ident_string s - end + try + match loc with + | None -> raise Not_found + | Some loc -> + reference (translate s) (Index.find (get_module false) loc) + with Not_found -> + if is_tactic s then + printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s) + 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) + with Not_found -> Tokens.output_tagged_ident_string s + else + Tokens.output_tagged_ident_string s let proofbox () = printf "<font size=-2>☐</font>" |