Make sure that hyperref creates the proper links to the documentation indexes.

3 files changed, 32 insertions, 49 deletions

diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 01ad0f70fa..907b30b3e0 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -134,24 +134,17 @@ Options A and B of the licence are {\em not} elected.}
 \bibliography{biblio}
 \cutname{biblio.html}
 
-\printindex
-\cutname{general-index.html}
-
-\printindex[tactic]
-\cutname{tactic-index.html}
-
-\printindex[command]
-\cutname{command-index.html}
-
-\printindex[option]
-\cutname{option-index.html}
-
-\printindex[error]
-\cutname{error-index.html}
+\printrefmanindex{default}{Global Index}{general-index.html}
+\printrefmanindex{tactic}{Tactics Index}{tactic-index.html}
+\printrefmanindex{command}{Vernacular Commands Index}{command-index.html}
+\printrefmanindex{option}{Vernacular Options Index}{option-index.html}
+\printrefmanindex{error}{Index of Error Messages}{error-index.html}
 
 %BEGIN LATEX
-\listoffigures
+\cleardoublepage
+\phantomsection
 \addcontentsline{toc}{chapter}{\listfigurename}
+\listoffigures
 %END LATEX
 
 \end{document}
diff --git a/doc/refman/headers.hva b/doc/refman/headers.hva
index df4aec272f..9714a29beb 100644
--- a/doc/refman/headers.hva
+++ b/doc/refman/headers.hva
@@ -8,23 +8,19 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \usepackage{index}
 \makeindex
-\newindex{tactic}{tacidx}{tacind}{%
-\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index}
 
-\newindex{command}{comidx}{comind}{%
-\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
-Vernacular Commands Index}
 
-\newindex{option}{optidx}{optind}{%
-\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}%
-Vernacular Options Index}
+\newindex{tactic}{tacidx}{tacind}{Tactics Index}
+\newindex{command}{comidx}{comind}{Vernacular Commands Index}
+\newindex{option}{optidx}{optind}{Vernacular Options Index}
+\newindex{error}{erridx}{errind}{Index of Error Messages}
+\renewindex{default}{idx}{ind}{Global Index}
 
-\newindex{error}{erridx}{errind}{%
-\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
-
-\renewindex{default}{idx}{ind}{%
-\protect\addcontentsline{toc}{chapter}{Global Index}%
-Global Index}
+\newcommand{\printrefmanindex}[3]{%
+\addcontentsline{toc}{chapter}{#2}%
+\printindex[#1]%
+\cutname{#3}%
+}
 
 \newcommand{\tacindex}[1]{%
 \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
diff --git a/doc/refman/headers.sty b/doc/refman/headers.sty
index ef28588e3c..fb39f687d7 100644
--- a/doc/refman/headers.sty
+++ b/doc/refman/headers.sty
@@ -30,27 +30,21 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \usepackage{index}
 \makeindex
-\newindex{tactic}{tacidx}{tacind}{%
-\protect\setheaders{Tactics Index}%
-\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index}
 
-\newindex{command}{comidx}{comind}{%
-\protect\setheaders{Vernacular Commands Index}%
-\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
-Vernacular Commands Index}
-
-\newindex{option}{optidx}{optind}{%
-\protect\setheaders{Vernacular Options Index}%
-\protect\addcontentsline{toc}{chapter}{Vernacular Options Index}%
-Vernacular Options Index}
-
-\newindex{error}{erridx}{errind}{%
-\protect\setheaders{Index of Error Messages}%
-\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
-
-\renewindex{default}{idx}{ind}{%
-\protect\addcontentsline{toc}{chapter}{Global Index}%
-\protect\setheaders{Global Index}Global Index}
+\newindex{tactic}{tacidx}{tacind}{Tactics Index}
+\newindex{command}{comidx}{comind}{Vernacular Commands Index}
+\newindex{option}{optidx}{optind}{Vernacular Options Index}
+\newindex{error}{erridx}{errind}{Index of Error Messages}
+\renewindex{default}{idx}{ind}{Global Index}
+
+\newcommand{\printrefmanindex}[3]{%
+\cleardoublepage%
+\phantomsection%
+\setheaders{#2}%
+\addcontentsline{toc}{chapter}{#2}%
+\printindex[#1]%
+\cutname{#3}%
+}
 
 \newcommand{\tacindex}[1]{%
 \index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}