doc-src/fixbookmarks.pl

Added support for making constants final, that is, ensuring that no
definition can be given later (useful for constants whose behaviour is
fixed axiomatically rather than definitionally).

s/\\([a-zA-Z]+)\s*/$1/g;
s/\$//g;
s/^BOOKMARK/\\BOOKMARK/g;