Re: modernizing html output

[Gavin Smith]

On Tue, Jan 01, 2019 at 05:46:11PM -0800, Per Bothner wrote:
> On 1/1/19 1:49 PM, Gavin Smith wrote:
> >Thanks for working on this.  What else needs to be changed so that the
> >output is valid for HTML 5?
> 
> It's worth clarifying that all of the changes in my patch produce valid HTML 
> 4:
> Using 'id' attributes on arbitrary elements is part of HTML 4, and I believe
> it has been supported by all non-toy browsers for 20 years.
> 
> So the only reason for not unconditionally changing things according to my 
> patch
> is if we are concerned about third-party css stylesheets or JavaScript (such 
> as
> texinfo-js) depending on the "old" html output and hence breaking if we make
> these changes unconditionally.  I also suggest we should make these changes
> at least the default (and possibly unconditionally) in a future texinfo 
> release.

I've tested the JS interface with the old (<a name>) and new (id) HTML 
output and it appears the same for both, from what I can tell.  I found 
a couple of reference to 'name' attributes in the code, but they may not 
matter, as I suspect they are not referring to elements that are 
actually present in the HTML files.  The patch below changes them to 
'id'.  I do not have a good understanding of this code, though.

Are there any JavaScript enthusiasts/experts out there who want to look
through info.js and see what work if any should be done in the future on it?


diff --git a/js/info.js b/js/info.js
index 10a2b1d..0175d35 100644
--- a/js/info.js
+++ b/js/info.js
@@ -1170,7 +1170,7 @@
       if (linkid === config.INDEX_ID)
         {
           hide_grand_child_nodes (ul);
-          res = elem.querySelector ("a[name=\"" + linkid + "\"]");
+          res = elem.querySelector ("a[id=\"" + linkid + "\"]");
         }
       else
         {
@@ -1229,7 +1229,7 @@
           var header = document.createElement ("header");
           var a = document.createElement ("a");
           a.setAttribute ("href", config.INDEX_NAME);
-          a.setAttribute ("name", config.INDEX_ID);
+          a.setAttribute ("id", config.INDEX_ID);
           header.appendChild (a);
           var div = document.createElement ("div");
           a.appendChild (div);