Save selected search tab

diff --git a/src/librustdoc/html/static/main.js b/src/librustdoc/html/static/main.js
index bccad6c89dc4fa3ada9f74606f030c7376897f29..8c260132902c2eecca6b3f3380c2b22af4a8d653 100644 (file)
--- a/src/librustdoc/html/static/main.js
+++ b/src/librustdoc/html/static/main.js
@@ -39,6 +39,13 @@
                      "associatedconstant",
                      "union"];
 
+    // On the search screen, so you remain on the last tab you opened.
+    //
+    // 0 for "Types/modules"
+    // 1 for "As parameters"
+    // 2 for "As return value"
+    var currentTab = 0;
+
     function hasClass(elem, className) {
         if (elem && className && elem.className) {
             var elemClass = elem.className;
@@ -747,7 +754,7 @@
 
             var output = '';
             if (array.length > 0) {
-                output = `<table class="search-results"${extraStyle}>`;
+                output = '<table class="search-results"' + extraStyle + '>';
                 var shown = [];
 
                 array.forEach(function(item) {
@@ -801,7 +808,7 @@
                 });
                 output += '</table>';
             } else {
-                output = `<div class="search-failed"${extraStyle}>No results :(<br/>` +
+                output = '<div class="search-failed"' + extraStyle + '>No results :(<br/>' +
                     'Try on <a href="https://duckduckgo.com/?q=' +
                     encodeURIComponent('rust ' + query.query) +
                     '">DuckDuckGo</a>?</div>';
@@ -809,6 +816,13 @@
             return output;
         }
 
+        function makeTabHeader(tabNb, text) {
+            if (currentTab === tabNb) {
+                return '<div class="selected">' + text + '</div>';
+            }
+            return '<div>' + text + '</div>';
+        }
+
         function showResults(results) {
             var output, query = getQuery();
 
@@ -816,9 +830,10 @@
             output = '<h1>Results for ' + escape(query.query) +
                 (query.type ? ' (type: ' + escape(query.type) + ')' : '') + '</h1>' +
                 '<div id="titles">' +
-                '<div class="selected">Types/modules</div>' +
-                '<div>As parameters</div>' +
-                '<div>As return value</div></div><div id="results">';
+                makeTabHeader(0, "Types/modules") +
+                makeTabHeader(1, "As parameters") +
+                makeTabHeader(2, "As return value") +
+                '</div><div id="results">';
 
             output += addTab(results['others'], query);
             output += addTab(results['in_args'], query, false);
@@ -1394,6 +1409,9 @@
 
     // In the search display, allows to switch between tabs.
     function printTab(nb) {
+        if (nb === 0 || nb === 1 || nb === 2) {
+            currentTab = nb;
+        }
         var nb_copy = nb;
         onEach(document.getElementById('titles').childNodes, function(elem) {
             if (nb_copy === 0) {