search

zjhmale / vscode-idris

Idris for Visual Studio Code
https://marketplace.visualstudio.com/items?itemName=zjhmale.Idris
BSD 3-Clause "New" or "Revised" License
106 stars 21 forks source link

Is it really necessary to pop up the output panel when typechecking a file? #109

Closed be5invis closed 7 years ago

zjhmale commented 7 years ago

@be5invis Yes, I also considered switching to a new way to display the type checking result, one possible way is to show problem panel when the type checking process failed, but it is still pending https://github.com/Microsoft/vscode/issues/22885 I think, and another way is to show the result on status bar which is already implemented https://github.com/zjhmale/vscode-idris/issues/106, but I haven't released this feature yet since I got some problem with vsce.

zjhmale commented 7 years ago

What do you have in mind is the best way to show the type checking result?

czhang03 commented 7 years ago

I would give a +1 to the problem panel (and I did)

zjhmale commented 7 years ago

@chantisnake problem panel is supposed to be the best solution here indeed, but we still have to wait it appears in the next release of VSCode.

be5invis commented 7 years ago

maybe a :+1: :-1: icon like this? https://marketplace.visualstudio.com/items?itemName=roscaj.dafny-vscode

czhang03 commented 7 years ago

I think @be5invis idea is generally valid for now. Idris atom uses a method like this (a notification in the status bar)

zjhmale commented 7 years ago

@be5invis @chantisnake OK, thanks for the reference, I will remove the stupid output channel and use the thumb icons.

zjhmale commented 7 years ago

So it is also no need to display the type checking errors in output channel right? cause we can check all the warnings and errors in problem panel.

czhang03 commented 7 years ago

I think so.

ndmitchell commented 7 years ago

I found the forced switch to output to be exceptionally annoying since I was quickly doing other stuff in another terminal window. I would definitely like this to be eliminated.

zjhmale commented 7 years ago

@ndmitchell I will address issue ASAP :)

zjhmale commented 7 years ago
ndmitchell commented 7 years ago

Note that the thing that broke my flow was forced switching to the output channel - actually having the output channel wasn't problematic.

be5invis commented 7 years ago

@zjhmale @ndmitchell Add an option for that, "showOutputWhenTypechecking"

zjhmale commented 7 years ago

@be5invis Thanks, adding an option is on the todo list already.

zjhmale commented 7 years ago

Hi @ndmitchell @be5invis @chantisnake Sorry for the huge delay, I was busy with something else these days, the showOutputWhenTypechecking option is already added and default to false, the new release will be tonight or tomorrow, Cheers!

pandemonium commented 7 years ago

When showOutputWhenTypechecking is false, saving the file or activating the idris.typecheck command does not actually type-check the file. This is a bug but since there is a discussion about it here I thought I'd mention it.

zjhmale commented 7 years ago

@pandemonium Thanks, I will address it. There is also a bug of Github that I just got the notification of your comment with a huge delay.