Compact index

[martinthomson]

I've tried to implement #862 here. It seems to make the index much less bulky, but I don't find that it is less usable. This uses Unicode symbols in place of words like "Section" or "Paragraph", so it's not a great default option, especially if you care about pure ASCII for text documents.

This is behind a --compact-index flag.