Feature request: show types of indicated terms.

[GoogleCodeExporter]

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.

Original issue reported on code.google.com by david.wa...@gmail.com on 14 Nov 2011 at 1:56

[GoogleCodeExporter]

For 1 you can always slap a lambda on your open terms to make them closed, or 
insert a goal as you mention. Although when inserting a goal you don't have to 
remove anything, just add {! around !} it and reload. That also takes care of 2.

We don't have the technology to map source code positions to type checking 
state at the moment and I'm not sure it's worth the machinery that would be 
required.

3 wouldn't be impossible I suppose, but it would mean adding huge amounts of 
data to the emacs highlighting files, so I'm not sure it's worth it.

Original comment by ulf.nor...@gmail.com on 16 Nov 2011 at 10:09

• Changed state: Accepted
• Added labels: Emacs, Priority-Low, Type-Enhancement

[GoogleCodeExporter]

Ok, I see. Yes, that trick solves it. But reloading takes time and typing 
effort (I am lazy and impatient ;-). I still think many users would appreciate 
automatic help about types of subterms.

Original comment by david.wa...@gmail.com on 16 Nov 2011 at 10:22

[m0davis]

+1. I'm reviewing some messy code I stopped working on two months ago and wish I had this enhancement.