search

banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link

Show the panel when open an agda file #61

Closed jonaprieto closed 6 years ago

jonaprieto commented 6 years ago

It would be nice to have the panel docking as soon as we open an Agda file, With some message like "Agda-mode loaded" or whatever. My point is the following. I have a file which takes to compile almost one minute. Since I just opened the file and then I typed C-C C-L to type-check the file, I don't know whether it's working or not. So, I sometimes got nervous because I don't know what's happening. When I got the panel, I see something at least.

banacorn commented 6 years ago

Do you want an Agda file to be loaded right after it is opened, or do you just want to see those type-checking messages running like in Emacs?

jonaprieto commented 6 years ago

Do you want an Agda file to be loaded right after it is opened No. That is not a good idea.

This request is just concerned with the first time you open the file.

The current behavior: You open the file, there is nothing in the panel docking because the file is not type-checked yet. Then, the user may want to type-check the file and wait to see the result. That's is how it works now and it's fine.

Now, my request is based on the following.

Imagine that you agda file has tons of code. You opened the file for the first time and you run the command to type-check it. At this point, you have to wait of course. But the user doesn't know if agda is effectively working or not because since it's the first time and the panel docking has not been opened yet. So since the agda file takes considerable time type-checking, the user starts feeling desperate (xD) and start typing C-C C-L to see if something happen and so on.

The thing is we can avoid this just showing the panel as soon as the user opens an agda file. The panel can contain a message like: "Agda-Mode waiting to type-check" or whatever. If the user decide to type-check, they will know what's happening because of the panel is there and we have the loading (type-checking animation) or also the verbose panel, I don't know, something to see the progress.

image

I might be badly expressing this. Sorry.

banacorn commented 6 years ago

I see!!