[no subject]

[Gavin D. Smith]

branch: old/qt-info
commit 33a22a18726fa65fdca432cb92a131c20f62873e
Author: Gavin Smith <gavinsmith0123@gmail.com>
AuthorDate: Wed Apr 10 16:27:45 2019 +0100

    Reduce ambiguity of "index".
    
    (config) <INDEX_NAME>: Rename to TOP_NAME.
    <INDEX_ID>: Rename to TOP_ID.
    (init_index_page, init_top_page): Rename.
    
    This tries to leave the word "index" used for the indices of the
    manual only.
---
 ChangeLog  | 11 ++++++++
 js/info.js | 94 +++++++++++++++++++++++++++++++-------------------------------
 2 files changed, 58 insertions(+), 47 deletions(-)

diff --git a/ChangeLog b/ChangeLog
index 06f2b348a2..9ddb0783de 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -1,3 +1,14 @@
+2019-04-09  Gavin Smith  <gavinsmith0123@gmail.com>
+
+       Reduce ambiguity of "index".
+
+       (config) <INDEX_NAME>: Rename to TOP_NAME.
+       <INDEX_ID>: Rename to TOP_ID.
+       (init_index_page, init_top_page): Rename.
+
+       This tries to leave the word "index" used for the indices of the 
+       manual only.
+
 2019-04-09  Gavin Smith  <gavinsmith0123@gmail.com>
 
        * js/info.js (web_channel_override) <input>: Only override for 
diff --git a/js/info.js b/js/info.js
index 6ca994aca9..8ec20fca33 100644
--- a/js/info.js
+++ b/js/info.js
@@ -27,14 +27,14 @@
       environment before loading this script.  */
   var config = {
     EXT: ".html",
-    INDEX_NAME: "index.html",
-    INDEX_ID: "index",
+    TOP_NAME: "index.html",
+    TOP_ID: "index",
     MAIN_ANCHORS: ["Top", "SEC_Contents"],
     WARNING_TIMEOUT: 3000,
     SCREEN_MIN_WIDTH: 700,
     hooks: {
       /** Define a function called after 'DOMContentLoaded' event in
-          the INDEX_NAME context.
+          the TOP_NAME context.
           @type {function (): void}*/
       on_main_load: null,
       /** Define a function called after 'DOMContentLoaded' event in
@@ -262,9 +262,9 @@
           var current = state.current;
           var link = linkid_split (state.current);
 
-          /* Handle inner 'config.INDEX_NAME' anchors specially.  */
-          if (link.pageid === config.INDEX_ID)
-            current = config.INDEX_ID;
+          /* Handle inner 'config.TOP_NAME' anchors specially.  */
+          if (link.pageid === config.TOP_ID)
+            current = config.TOP_ID;
 
           var ids = state.loaded_nodes[current];
           linkid = ids[action.direction];
@@ -399,7 +399,7 @@
   /** Initialize the index page of the manual which manages the state of the
       application.  */
   function
-  init_index_page ()
+  init_top_page ()
   {
     /*--------------------------.
     | Component for help page.  |
@@ -733,14 +733,14 @@
     function
     Pages (index_div)
     {
-      index_div.setAttribute ("id", config.INDEX_ID);
-      index_div.setAttribute ("node", config.INDEX_ID);
+      index_div.setAttribute ("id", config.TOP_ID);
+      index_div.setAttribute ("node", config.TOP_ID);
       index_div.setAttribute ("hidden", "true");
       this.element = document.createElement ("div");
       this.element.setAttribute ("id", "sub-pages");
       this.element.appendChild (index_div);
       /** @type {string[]} Currently created divs.  */
-      this.ids = [config.INDEX_ID];
+      this.ids = [config.TOP_ID];
       /** @type {string} */
       this.prev_id = null;
       /** @type {HTMLElement} */
@@ -796,11 +796,11 @@
           && state.search.status === "ready")
         {
           this.prev_search = state.search;
-          if (state.search.current_pageid === config.INDEX_ID)
+          if (state.search.current_pageid === config.TOP_ID)
             {
               window.setTimeout (function () {
                 store.dispatch ({ type: "search-query" });
-                var res = search (document.getElementById (config.INDEX_ID),
+                var res = search (document.getElementById (config.TOP_ID),
                                   state.search.regexp);
                 store.dispatch ({ type: "search-result", found: res });
               }, 0);
@@ -822,8 +822,8 @@
       /* Update highlight of current page.  */
       if (!state.highlight)
         {
-          if (state.current === config.INDEX_ID)
-            remove_highlight (document.getElementById (config.INDEX_ID));
+          if (state.current === config.TOP_ID)
+            remove_highlight (document.getElementById (config.TOP_ID));
           else
             {
               var link = linkid_split (state.current);
@@ -884,7 +884,7 @@
 
       /* Create iframe if necessary unless the div is refering to the Index
          page.  */
-      if ((pageid === config.INDEX_ID) && visible)
+      if ((pageid === config.TOP_ID) && visible)
         {
           div.removeAttribute ("hidden");
           /* Unlike iframes, Elements are unlikely to be scrollable (CSSOM
@@ -960,7 +960,7 @@
             {
               /* Fallback to changing only the hash part which is safer.  */
               visible_url = window.location.pathname;
-              if (linkid !== config.INDEX_ID)
+              if (linkid !== config.TOP_ID)
                 visible_url += ("#" + linkid);
               method.call (window.history, linkid, null, visible_url);
             }
@@ -975,7 +975,7 @@
     function
     post_message (pageid, msg)
     {
-      if (pageid === config.INDEX_ID)
+      if (pageid === config.TOP_ID)
         window.postMessage (msg, "*");
       else
         {
@@ -1000,7 +1000,7 @@
     | Event handlers for the top-level context.  |
     `-------------------------------------------*/
 
-    /* Initialize the top level 'config.INDEX_NAME' DOM.  */
+    /* Initialize the top level 'config.TOP_NAME' DOM.  */
     function
     on_load ()
     {
@@ -1034,7 +1034,7 @@
             {
               var link = linkid_split (state.current);
               var elem = document.getElementById (link.pageid);
-              if (link.pageid !== config.INDEX_ID)
+              if (link.pageid !== config.TOP_ID)
                 elem.querySelector ("iframe").focus ();
               else
                 {
@@ -1062,9 +1062,9 @@
 
       /* Retrieve NEXT link and local menu.  */
       var links = {};
-      links[config.INDEX_ID] = navigation_links (document);
+      links[config.TOP_ID] = navigation_links (document);
       store.dispatch (actions.cache_links (links));
-      store.dispatch ({ type: "iframe-ready", id: config.INDEX_ID });
+      store.dispatch ({ type: "iframe-ready", id: config.TOP_ID });
       store.dispatch ({
         type: "echo",
         msg: "Welcome to Texinfo documentation viewer 6.1, type '?' for help."
@@ -1183,7 +1183,7 @@
       }
 
       var ul = elem.querySelector ("ul");
-      if (linkid === config.INDEX_ID)
+      if (linkid === config.TOP_ID)
         {
           hide_grand_child_nodes (ul);
           res = document.getElementById(linkid);
@@ -1211,7 +1211,7 @@
     function
     create_link_dict (nav)
     {
-      var prev_id = config.INDEX_ID;
+      var prev_id = config.TOP_ID;
       var links = {};
 
       function
@@ -1229,7 +1229,7 @@
 
       depth_first_walk (nav, add_link, Node.ELEMENT_NODE);
       /* Add a reference to the first and last node of the manual.  */
-      links["*TOP*"] = config.INDEX_ID;
+      links["*TOP*"] = config.TOP_ID;
       links["*END*"] = prev_id;
       return links;
     }
@@ -1244,8 +1244,8 @@
         {
           var header = document.createElement ("header");
           var a = document.createElement ("a");
-          a.setAttribute ("href", config.INDEX_NAME);
-          a.setAttribute ("id", config.INDEX_ID);
+          a.setAttribute ("href", config.TOP_NAME);
+          a.setAttribute ("id", config.TOP_ID);
           header.appendChild (a);
           var div = document.createElement ("div");
           a.appendChild (div);
@@ -1275,7 +1275,7 @@
                          window.location.href.replace (/[/][^/]*$/, "/"));
       document.head.appendChild (base);
 
-      scan_toc (toc_div, config.INDEX_NAME);
+      scan_toc (toc_div, config.TOP_NAME);
 
       /* Get 'backward' and 'forward' link attributes.  */
       var dict = create_link_dict (toc_div.querySelector ("nav.contents ul"));
@@ -1299,7 +1299,7 @@
 
           /* Remove the hash part for the main page.  */
           var pageid = linkid_split (data.selected).pageid;
-          var selected = (pageid === config.INDEX_ID) ? pageid : data.selected;
+          var selected = (pageid === config.TOP_ID) ? pageid : data.selected;
           /* Highlight the current LINKID in the table of content.  */
           var elem = scan_toc (toc_div, selected);
           if (elem)
@@ -1431,7 +1431,7 @@
                   }
                 else if (!absolute_url_p (href))
                   {
-                    var linkid = href_hash (href) || config.INDEX_ID;
+                    var linkid = href_hash (href) || config.TOP_ID;
                     store.dispatch (actions.set_current_url (linkid));
                     event.preventDefault ();
                     event.stopPropagation ();
@@ -1609,16 +1609,16 @@
   }
 
   /** Return a relative URL corresponding to HREF, which refers to an anchor
-      of 'config.INDEX_NAME'.  HREF must be a USVString representing an
+      of 'config.TOP_NAME'.  HREF must be a USVString representing an
       absolute or relative URL.  For example "foo/bar.html" will return
-      "config.INDEX_NAME#bar".
+      "config.TOP_NAME#bar".
 
       @arg {string} href.*/
   function
   with_sidebar_query (href)
   {
-    if (basename (href) === config.INDEX_NAME)
-      return config.INDEX_NAME;
+    if (basename (href) === config.TOP_NAME)
+      return config.TOP_NAME;
     else
       {
         /* XXX: Do not use the URL API for IE portability.  */
@@ -1630,7 +1630,7 @@
            instead of directly to the page. */
         if (url.hash && new_hash !== url.hash)
           new_hash += ("." + url.hash.slice (1));
-        return config.INDEX_NAME + new_hash;
+        return config.TOP_NAME + new_hash;
       }
   }
 
@@ -1665,8 +1665,8 @@
             link.setAttribute ("href", href$);
             if (id)
               {
-                var linkid = (href$ === config.INDEX_NAME) ?
-                    config.INDEX_ID : href_hash (href$);
+                var linkid = (href$ === config.TOP_NAME) ?
+                    config.TOP_ID : href_hash (href$);
                 link.setAttribute ("id", linkid);
               }
           }
@@ -1681,11 +1681,11 @@
   normalize_hash (hash)
   {
     var text = hash.slice (1);
-    /* Some anchor elements are present in 'config.INDEX_NAME' and we need to
+    /* Some anchor elements are present in 'config.TOP_NAME' and we need to
        handle link to them specially (i.e. not try to find their corresponding
        iframe).*/
     if (config.MAIN_ANCHORS.includes (text))
-      return config.INDEX_ID + "." + text;
+      return config.TOP_ID + "." + text;
     else
       return text;
   }
@@ -1712,8 +1712,8 @@
   function
   linkid_to_url (linkid)
   {
-    if (linkid === config.INDEX_ID)
-      return config.INDEX_NAME;
+    if (linkid === config.TOP_ID)
+      return config.TOP_NAME;
     else
       {
         var link = linkid_split (linkid);
@@ -1823,8 +1823,8 @@
         if (nav_id)
           {
             var href = basename (link.getAttribute ("href"));
-            if (href === config.INDEX_NAME)
-              res[nav_id] = config.INDEX_ID;
+            if (href === config.TOP_NAME)
+              res[nav_id] = config.TOP_ID;
             else
               res[nav_id] = href_hash (href);
           }
@@ -2019,8 +2019,8 @@
   config = Object.assign (config, user_config);
 
   var inside_iframe = top !== window;
-  var inside_index_page = window.location.pathname === config.INDEX_NAME
-      || window.location.pathname.endsWith ("/" + config.INDEX_NAME)
+  var inside_index_page = window.location.pathname === config.TOP_NAME
+      || window.location.pathname.endsWith ("/" + config.TOP_NAME)
       || window.location.pathname.endsWith ("/");
 
   if (inside_index_page)
@@ -2032,7 +2032,7 @@
         /* Dictionary associating keyword to linkids.  */
         index: {},
         /* page id of the current page.  */
-        current: config.INDEX_ID,
+        current: config.TOP_ID,
         /* dictionary associating a page id to a boolean.  */
         ready: {},
         /* Current mode for handling history.  */
@@ -2042,7 +2042,7 @@
       };
 
       store = new Store (updater, initial_state);
-      var index = init_index_page ();
+      var index = init_top_page ();
       var sidebar = init_sidebar ();
       window.addEventListener ("DOMContentLoaded", function () {
         index.on_load ();
@@ -2061,7 +2061,7 @@
     }
   else
     {
-      /* Jump to 'config.INDEX_NAME' and adapt the selected iframe.  */
+      /* Jump to 'config.TOP_NAME' and adapt the selected iframe.  */
       window.location.replace (with_sidebar_query (window.location.href));
     }