idvi: Specials to Control Generated HTML

When building a per-page html file, variable names which appear in the template html file are expanded. Some standard ones are the variables page and title. It would be nice to be able to pass values from the document to the template html file, such as a string to be used to represent the current page number or a section title to be placed in the browser title bar.
  1. Handle specials of the form idvi:name=value in idvi.dvi.DVITokenizer.

  2. Ignore the above tokens altogether in the class idvi.display.Parser, or add a call to DVITokenizer telling it to not generate the token.

  3. Give each page its own list of variables, kept in the idvi.split.PageInfo class. Variables accumulate over the course of a document, but only the values up to the current page are used for any given page.

    This lets us use pageString or sectionTitle variables in a natural way.

  4. Look around line 400 of the file idvi.split.Splitter.java to see how merge per-page variables with the rest.