diff --git a/doc/src/sgml/stylesheet-html-common.xsl b/doc/src/sgml/stylesheet-html-common.xsl
index bb6429ef7c..8e5d9912d5 100644
--- a/doc/src/sgml/stylesheet-html-common.xsl
+++ b/doc/src/sgml/stylesheet-html-common.xsl
@@ -309,4 +309,137 @@ set toc,title
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ 6
+
+
+
+
+
+
+
+
+
+ clear: both
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+ #
+
+
+
+
+
+ id_link
+
+ #
+
+
+
+
+
+
+
+ Ids are required in order to provide the public
+ HTML documentation with stable URLs for <
+
+ > element content; id missing at:
+
+ /
+
+
+ [@
+
+ = '
+
+ ']
+
+
+
+
+
+
+
+
+
diff --git a/doc/src/sgml/stylesheet.css b/doc/src/sgml/stylesheet.css
index cc14efa1ca..15bcc95d41 100644
--- a/doc/src/sgml/stylesheet.css
+++ b/doc/src/sgml/stylesheet.css
@@ -169,3 +169,13 @@ acronym { font-style: inherit; }
width: 75%;
}
}
+
+/* Links to ids of headers and definition terms */
+a.id_link {
+ color: inherit;
+ visibility: hidden;
+}
+
+*:hover > a.id_link {
+ visibility: visible;
+}