public static class HTMLPane.ChoiceGroup
A document may be displayed piecemeal; nominally each piece
corresponds to a tab in the view, but other organizations
will also be used. Pieces appear in
the document as the children of single DIV. This DIV has the
attribute choicegroup, with a name as its value. Each child of the
choicegroup DIV is itself a DIV and has attribute 'choice'
whose value is the name to display on the tab.
<div choicegroup='c1'><div choice='tab first'>
... contents of first tab ...
... contents of second tab ...
The choicegroup names must be unique across the document;
that is, no two DIVs can have the same choicegroup value.
Similarly, the names of choiceGroups within each choicegroup must be unique.
A ChoiceGroup relates to one <div choicegroup ...> in the document.
Its choices field has one entry for each choice in the group.
In IndexGofer/StyleEdit.java, the document is displayed in an HTMLPane
just below a JPanel managed by a JTabbedPane. The JTabbedPane has dummy
contents. As a tab is clicked, the corresponding choice in the HTML
pane is made visible.