diff options
author | Felix Mulder <felix.mulder@gmail.com> | 2016-03-24 19:57:50 +0100 |
---|---|---|
committer | Felix Mulder <felix.mulder@gmail.com> | 2016-03-30 11:21:20 +0200 |
commit | 7822041205586ce909729a97f7bbcac8b871dffb (patch) | |
tree | 76902587640e1a53acff354d585f476358192571 /src/scaladoc | |
parent | ecc89449eebda0f6464e1dcc1e61bbdc46bdab3f (diff) | |
download | scala-7822041205586ce909729a97f7bbcac8b871dffb.tar.gz scala-7822041205586ce909729a97f7bbcac8b871dffb.tar.bz2 scala-7822041205586ce909729a97f7bbcac8b871dffb.zip |
Add search history for Scaladoc
Diffstat (limited to 'src/scaladoc')
-rw-r--r-- | src/scaladoc/scala/tools/nsc/doc/html/resource/lib/index.js | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/scaladoc/scala/tools/nsc/doc/html/resource/lib/index.js b/src/scaladoc/scala/tools/nsc/doc/html/resource/lib/index.js index 55224eae52..41936799b2 100644 --- a/src/scaladoc/scala/tools/nsc/doc/html/resource/lib/index.js +++ b/src/scaladoc/scala/tools/nsc/doc/html/resource/lib/index.js @@ -21,6 +21,20 @@ var Index = {}; } })(Index); +/** Find query string from URL */ +var QueryString = function(key) { + if (QueryString.map === undefined) { // only calc once + QueryString.map = {}; + var keyVals = window.location.search.split("?").pop().split("&"); + keyVals.forEach(function(elem) { + var pair = elem.split("="); + if (pair.length == 2) QueryString.map[pair[0]] = pair[1]; + }); + } + + return QueryString.map[key]; +}; + $(document).ready(function() { // Clicking #doc-title returns the user to the root package $("#doc-title").click(function() { document.location = toRoot + "index.html" }); @@ -39,6 +53,11 @@ $(document).ready(function() { else $("#textfilter > .input > .clear").hide(); }); + + if (QueryString("search") !== undefined) { + $("#index-input").val(QueryString("search")); + searchAll(); + } }); /* Handles all key presses while scrolling around with keyboard shortcuts in search results */ @@ -510,6 +529,11 @@ function searchAll() { return; } + // Replace ?search=X with current search string if not hosted locally on Chrome + try { + window.history.replaceState({}, "", "?search=" + searchStr); + } catch(e) {} + $("div#results-content > span.search-text").remove(); var memberResults = document.getElementById("member-results"); |