diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/librustdoc/html/static/main.js | 28 |
1 files changed, 23 insertions, 5 deletions
diff --git a/src/librustdoc/html/static/main.js b/src/librustdoc/html/static/main.js index bccad6c89dc..8c260132902 100644 --- 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) { |
