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

[be5invis]

No description provided.

[swr1bm86]

@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 microsoft/vscode#22885 I think, and another way is to show the result on status bar which is already implemented #106, but I haven't released this feature yet since I got some problem with vsce.

[swr1bm86]

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

[czhang03]

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

[swr1bm86]

@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]

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

[czhang03]

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

[swr1bm86]

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

[swr1bm86]

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]

I think so.

[ndmitchell]

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.

[swr1bm86]

@ndmitchell I will address issue ASAP :)

[swr1bm86]

• Add option to turn off stupid output channel.
  - [ ] Using thumb icons.
  - [ ] Add a preview HTML page to display errors. I can't remember what exactly in my mind three weeks ago.

[ndmitchell]

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

[be5invis]

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

[swr1bm86]

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

[swr1bm86]

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]

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.

[swr1bm86]

@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.