Ask user whether to index a big file

[samlhuillier]

Given that we index the contents of the editor each time the user changes file, and this can introduce lots of lag for big files, we should ask the user whether they want us to index a file (if we detect that it is big) before doing it.

This could just be a modal that pops up and asks: Should we index this file now? Should we index the first 100 chunks? Etc.