Re: Should @shortcontents come before @contents with CONTENTS_OUTPUT_LOCATION=after_top?

[Gavin Smith]

On Sun, Mar 12, 2023 at 11:49:38AM +0100, Patrice Dumas wrote:
> On Sat, Mar 11, 2023 at 12:01:18PM +0100, Arsen Arsenović wrote:
> > Hi,
> > 
> > Currently, CONTENTS_OUTPUT_LOCATION=after_top outputs contents first,
> > then shortcontents, as is written in HTML.pm:4113.  Some manuals, such
> > as that of GCC, place @shortcontents first, in order to let the user
> > browse a briefer high-level overview before jumping into the (quite
> > large) table of contents.
> 
> I think that the best would be, after having decided on a default, to
> have the alternative order specified in CONTENTS_OUTPUT_LOCATION.  So,
> for example if it is shortcontents first and contents next in the
> default case, there would be both CONTENTS_OUTPUT_LOCATION=after_top
> and CONTENTS_OUTPUT_LOCATION=after_top_short_last to be able to specify
> that.

I agree with Arsen that the shortcontents should come first.  I don't
care if other options are added too to swap the orders.

> 
> > Do you think this rationale makes sense, and should we output
> > @shortcontents first with after_top?
> 
> If we do it with after_top, it should be the same with the other similar
> possibilities for CONTENTS_OUTPUT_LOCATION.  So, both with after_title
> and separate_element the defaut order should be the same.

Good point.