The docs images had been duplicated in
```
docs/img/
```
and
```
docs/app/assets/img
```
This commit fixes the gulp build to use the doc images from `docs/img` and
removes the duplocates from `docs/app/assets/img`
Closes#9655
This commit refactors how the search index is built. The docsSearch service
is now defined by a provider, which returns a different implementation of
the service depending upon whether the current browser supports WebWorkers
or now.
* **WebWorker supported**: The index is then built and stored in a new worker.
The service posts and receives messages to and from this worker to make
queries on the search index.
* **WebWorker no supported**: The index is built locally but with a 500ms
delay so that the initial page can render before the browser is blocked as
the index is built.
Also the way that the current app is identified has been modified so we can
slim down the js data files (pages-data.js) to again improve startup time.
Closes#9204Closes#9203
Bootstrap CSS was removing the margin after ul elements if they were
descendents of other ul elements. But if the ul was followed by a p
then this looked terrible.
Related to #5953
In firefox the version picker's dropdown icon from the default `select` element
is still showing. This CSS forces FF to hide the ugly default.
Closes#6878
If the type of a type-hint was not recognized, say a "Promise", then
the background color was left as white. Given that the default
foreground color is also white, this meant that such type-hints were
invisible.
Closes#6934
