Coqdoc: Exporting location and unique id for binding variables.

This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.

In particular, this fixes #7697.

5 files changed, 12 insertions, 5 deletions

diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index dbc930f5ec..2c2bd98541 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -230,6 +230,10 @@ tr.infrulemiddle hr {
     color: rgb(40%,0%,40%);
 }
 
+.id[title="binder"] {
+    color: rgb(40%,0%,40%);
+}
+
 .id[type="definition"] { 
     color: rgb(0%,40%,0%);
 }
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index f49f9f0066..aa9c414761 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -72,6 +72,7 @@
 \newcommand{\coqdocinductive}[1]{\coqdocind{#1}}
 \newcommand{\coqdocdefinition}[1]{\coqdoccst{#1}}
 \newcommand{\coqdocvariable}[1]{\coqdocvar{#1}}
+\newcommand{\coqdocbinder}[1]{\coqdocvar{#1}}
 \newcommand{\coqdocconstructor}[1]{\coqdocconstr{#1}}
 \newcommand{\coqdoclemma}[1]{\coqdoccst{#1}}
 \newcommand{\coqdocclass}[1]{\coqdocind{#1}}
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 4cc82726f1..723918525d 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -31,6 +31,7 @@ type entry_type =
   | Abbreviation
   | Notation
   | Section
+  | Binder
 
 type index_entry =
   | Def of string * entry_type
@@ -177,6 +178,7 @@ let type_name = function
   | Abbreviation -> "abbreviation"
   | Notation -> "notation"
   | Section -> "section"
+  | Binder -> "binder"
 
 let prepare_entry s = function
   | Notation ->
@@ -268,6 +270,7 @@ let type_of_string = function
   | "mod" | "modtype" -> Module
   | "tac" -> TacticDefinition
   | "sec" -> Section
+  | "binder" -> Binder
   | s -> invalid_arg ("type_of_string:" ^ s)
 
 let ill_formed_glob_file f =
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 3426fdd3d3..7a3d401fd7 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -30,6 +30,7 @@ type entry_type =
   | Abbreviation
   | Notation
   | Section
+  | Binder
 
 val type_name : entry_type -> string
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index dd1b65d294..04725aa26f 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -337,11 +337,8 @@ module Latex = struct
     let id = if fid <> "" then (m ^ "." ^ fid) else m in
     match find_module m with
       | Local ->
-          if typ = Variable then
-            printf "\\coqdoc%s{%s}" (type_name typ) s
-          else
-            (printf "\\coqref{"; label_ident id;
-             printf "}{\\coqdoc%s{%s}}" (type_name typ) s)
+          printf "\\coqref{"; label_ident id;
+          printf "}{\\coqdoc%s{%s}}" (type_name typ) s
       | External m when !externals ->
           printf "\\coqexternalref{"; label_ident fid;
           printf "}{%s}{\\coqdoc%s{%s}}" (escaped m) (type_name typ) s
@@ -615,6 +612,7 @@ module Html = struct
       else match s.[i] with
       | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1)
       | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1)
+      | '-' | ':' -> loop esc (i-1) (* should be safe in HTML5 attribute name syntax *)
       | _ ->
         (* This name contains complex characters:
            this is probably a notation string, we simply hash it. *)