From 7b88d786d16c54fe8ad2d0802a1551bfc9265b9e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 14 Jul 2017 23:19:05 +0200
Subject: 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.
---
tools/coqdoc/output.ml | 34 +++++++++++++++-------------------
1 file changed, 15 insertions(+), 19 deletions(-)
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 5c0d2a39b0..d043c4a584 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -693,25 +693,21 @@ module Html = struct
printf "%s" (translate s)
let ident s loc =
- if is_keyword s then begin
- printf "%s" (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 "%s" (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 "%s" (translate s)
+ else if is_keyword s then
+ printf "%s" (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 "☐"
--
cgit v1.2.3