Re: Variable pitch mode line

[Po Lu]

Lars Ingebrigtsen <larsi@gnus.org> writes:

>> I also don't understand how an HTML-based Info reader will handle (for
>> example) I-search through an entire manual without rendering it all in
>> one go.

> We don't have to render the HTML to search in it -- parsing the HTML is
> enough (and is quick), and then we can just search in the DOM and then
> render the node we find the match in.  It's just a small matter of
> programming.

It seems a bit scary to me.  For example, how would I quickly find "see
Optimize Options", if that was generated by a pxref, where the "see" and
"Optimize Options" are in different nodes?

Thanks.