@@ -92,6 +92,13 @@ function getSearchElement() {
9292
9393 var titleBeforeSearch = document . title ;
9494
95+ function clearInputTimeout ( ) {
96+ if ( searchTimeout !== null ) {
97+ clearTimeout ( searchTimeout ) ;
98+ searchTimeout = null ;
99+ }
100+ }
101+
95102 function getPageId ( ) {
96103 var id = document . location . href . split ( "#" ) [ 1 ] ;
97104 if ( id ) {
@@ -345,10 +352,7 @@ function getSearchElement() {
345352 if ( hasClass ( help , "hidden" ) === false ) {
346353 displayHelp ( false , ev , help ) ;
347354 } else if ( hasClass ( search , "hidden" ) === false ) {
348- if ( searchTimeout !== null ) {
349- clearTimeout ( searchTimeout ) ;
350- searchTimeout = null ;
351- }
355+ clearInputTimeout ( ) ;
352356 ev . preventDefault ( ) ;
353357 hideSearchResults ( search ) ;
354358 document . title = titleBeforeSearch ;
@@ -1805,7 +1809,7 @@ function getSearchElement() {
18051809
18061810 function startSearch ( ) {
18071811 var callback = function ( ) {
1808- clearTimeout ( searchTimeout ) ;
1812+ clearInputTimeout ( ) ;
18091813 if ( search_input . value . length === 0 ) {
18101814 if ( browserSupportsHistoryApi ( ) ) {
18111815 history . replaceState ( "" , window . currentCrate + " - Rust" , "?search=" ) ;
@@ -1819,10 +1823,7 @@ function getSearchElement() {
18191823 search_input . oninput = callback ;
18201824 document . getElementsByClassName ( "search-form" ) [ 0 ] . onsubmit = function ( e ) {
18211825 e . preventDefault ( ) ;
1822- if ( searchTimeout !== null ) {
1823- clearTimeout ( searchTimeout ) ;
1824- searchTimeout = null ;
1825- }
1826+ clearInputTimeout ( ) ;
18261827 search ( ) ;
18271828 } ;
18281829 search_input . onchange = function ( e ) {
@@ -1831,10 +1832,7 @@ function getSearchElement() {
18311832 return ;
18321833 }
18331834 // Do NOT e.preventDefault() here. It will prevent pasting.
1834- if ( searchTimeout !== null ) {
1835- clearTimeout ( searchTimeout ) ;
1836- searchTimeout = null ;
1837- }
1835+ clearInputTimeout ( ) ;
18381836 // zero-timeout necessary here because at the time of event handler execution the
18391837 // pasted content is not in the input field yet. Shouldn’t make any difference for
18401838 // change, though.
0 commit comments