Commit 69337bce authored by Herbert Valerio Riedel's avatar Herbert Valerio Riedel 🕺
Browse files

Try to fix \index-ed `||` getting LaTeX confused

Turns out that special care needs to be taken when escaping `|`s in
`\index{}`. See also
http://tex.stackexchange.com/questions/176931/how-to-escape-character-in-index
parent 607cd9eb
......@@ -40,7 +40,7 @@ more readable.
\label{prelude-bool}
\indextycon{Bool}
\indextt{False}\indextt{True}
\index{""|""|@@{\tt {\char'174}{\char'174}}}
\index{\vert\vert@@{\tt {\char'174}{\char'174}}}
\index{&&@@{\tt \&\&}}
\indextt{not}
\indextt{otherwise}
......
......@@ -1464,7 +1464,7 @@ edence & operators & operators & operators \\ \hline\hline
\indextt{elem}
\indextt{notElem}
\index{&&@@{\tt \&\&}}
\index{""|""|@@{\tt {\char'174}{\char'174}}}
\index{\vert\vert@@{\tt {\char'174}{\char'174}}}
\indextt{>>}
\indextt{>>=}
\index{$@@{\tt {\char'044}}}
......
% Formatting for double-sided
\documentclass[twoside,10pt]{book}
\usepackage[T1]{fontenc}
\usepackage{times}
\usepackage{makeidx}
\usepackage{graphicx}
......
......@@ -114,10 +114,10 @@ sub printIndexEntries { # also re-sets $indexentries, specialentries
#
# there are a few "raw" chars that need fiddling, too...
#
$raw =~ s/\|/""\|/g;
$raw =~ s/!/""!/g;
$raw =~ s/\@/""\@\@/g;
$raw =~ s/\\/\\\\/g;
$raw =~ s/\|/\\vert/g;
print "\\index\{$raw\@\@$processed\}%\n";
} else {
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment