Doctor doesn't report missing src.zip file

[ayoub-benali]

Describe the bug

When the src.zip file is missing from the java home directory, textDocument/definition would yield no results for java standard library classes like java.time.LocalDate.

Running metals doctor commands shows you that everything is fine.

To Reproduce

1. Remove or rename src.zip
2. Start Metals
3. Try go to definition in java.time.LocalDate
4. Notice that nothing happens

Expected behavior

Metals doctor should show a warning with a possible fix like sudo apt-get install openjdk-8-source or equivalent.

Installation:

• Operating system: Linux
• Editor: Sublime
• Metals version: 0.10.9+213-69c1200a-SNAPSHOT

Search terms

java home, goto definiton, doctor

[tgodzik]

Thanks for reporting! We should refactor the doctor for sure and add more useful information like this.

[dos65]

I'm wondering if it would be easy to download jdk-sources if they don't exist

[tgodzik]

We would need to download the whole JDK and unpack from that. The other option is to ship our own JDK as a default, which would always have src.zip, but that would be a bit heavy.

[ayoub-benali]

Yeah I think downloading the sources would be overkill. For the moment just better error reporting would be a win.