Small improvements to `workspace/symbol`#5443

Merged

Duhemm merged 7 commits intoscala:masterfrom

dotty-staging:ide-workspace-symbols

Nov 30, 2018

Commits on Nov 20, 2018

Commits on Nov 29, 2018

Commits on Nov 30, 2018

Fix outdated doc
Duhemm
committed