What's the problem? Cut-and-pasted program examples are preferred over
attachments (if reasonably short).

When the cursor is in a goal, I can get the type of an expression by typing C-c 
C-d. I would like to have two enhancements of this feature:

1. C-c C-d sometimes work even when the cursor is not in a goal. This seems to 
be true for closed terms. But I would like to have this even for open terms. As 
it is now, agda reports "not in scope x ...", even if the cursor is in a 
position where x is known. To figure out the type, I either have to do it in my 
head, or I have to remove something, and write "?" there, reload the file, and 
then ask for the type.

2. The same as 1, but for any marked region, when the region marks a term.

3. Pop-up "bubble" with type info when I hoover the mouse over the top 
constructor of a term. for an application, it could be the space between the 
terms.


What version of Agda are you using? On what operating system (if relevant)?
Agda-2.2.10, not OS dependent, I believe.