HTML Navigation options to publisher file

[Rob Beezer]

I've converted three more string parameters to publisher file entries. I think
there may be only one more left in my sights as part of this tedious project.
(Brad M calls it "chopping wood".)

Subsection 29.1.7: HTML Navigation
https://pretextbook.org/doc/guide/html/html-publisher-options.html#html-navigation

Not on -announce because

* I'm not sure anybody is using these much.

* The "tree" navigation logic is mostly personal self-indulgence.

* One, and maybe two, are really about style, or at least UI construction.

* Maybe not best to advertise them now.

So please be my eyes on this one, as usual. And not trying to open old wounds,
we can migrate some of this to styling/JS/CSS as appropriate/timely, it is all
ancient history.

Rob