Completion improvement

[zjhmale]

• Note for contribution to add item kind for :repl-completions command. Also, need to eliminate some speed overhead.

Currently, it will only suggest bare strings for auto-completion without any extra information e.g. item kind which mentioned above.

{"responseType":"return","msg":[[["locMessage"],""]]}
{"responseType":"return","msg":[[["show","showArg","showCon","showLitChar","showLitString","showParens","showPrec"],""]]}
{"responseType":"return","msg":[[["show"],""]]}
{"responseType":"return","msg":[[["show","showArg","showCon","showLitChar","showLitString","showParens","showPrec"],""]]}
{"responseType":"return","msg":[[["Unknown","UnknownImplicit"],""]]}
{"responseType":"return","msg":[[["show","showArg","showCon","showLitChar","showLitString","showParens","showPrec"],""]]}

• Support auto-completion for all words in the open editor like javascript here.

For the second point, there is no external tools to analysis Idris source file currently, so a naive but straight forward way is to extract all the lexer identifier and add to the completion result list.

[czhang03]

also, the completion failed when previous file load ends with an error.

[zjhmale]

Hi, @chantisnake Can you give me more details?

1. What is the suggestMode you are playing with?
2. Are you working with a standalone Idris file or an iPKG based project?
3. Which version of this extension do you currently hold?

Thanks in advance!

[czhang03]

Sorry, I thought this is an known issue, therefore did not provide any details.

My suggestionMode is repl.
My computer is running Windows 10 build 15063.138
Working in standalone project
The extension version is 0.9.0, vscode version is 1.11.2

The behavior is, let's say I wrote a function and did not save (do the type check on file) then the completion for that function will not show up

let's say I save (do type check on file), but I did not finish the function.
Therefore causing an error:

Then I will not get any completion at all, until I do the next type check.

This is quite annoying...

[czhang03]

I think one of the way to solve the previous problem is that when you did the type check, keep the previous successful type check file in a temp location, if the current type check failed, use the previous successful type checked file to provide completion.

I don't know lots of javascript, therefore I will write Pseudocode:

process = start_process( type_check(current_file) )

if process.failed() && exists(last_success_file):
   start_process( type_check(last_success_file) )

elif process.success() :
   last_success_file = current_file

This is no where near a good solution, but it works. Although the performance issue is an headache.

Let's just hope a "real script analyzer" will come for idris soon

[zjhmale]

@chantisnake You solution seems doable, I will create a separator issue to track this, Thanks!

[zjhmale]

@chantisnake On a second thought, cache previous file may not work as expected because if you want to type check a file in a project, you also need other related modules which means you have to cache the whole project which can be type checked before, so maybe a more straightforward way is to cache the previous completion items I believe.

[czhang03]

It is reasonable, I believe.

Thank your for fixing it.

[zjhmale]

Hi, @chantisnake I believe I have already addressed the issue you mentioned before, it can provide cached completion items when type checking failed. But for the first case that you add a function without saving the file, it is impossible to auto completion the name for it because Idris process can only interpolate the function into the module context unless you successfully type check and load the file. BTW, I will release a new version which contains this fix ASAP this week :)

[czhang03]

Thank you so much!

[zjhmale]

@chantisnake No worries :)