search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Feature request: show types of indicated terms. #516

Open UlfNorell opened 10 years ago

UlfNorell commented 10 years ago

From david.wa...@gmail.com on November 14, 2011 14:56:42

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: http://code.google.com/p/agda/issues/detail?id=516

UlfNorell commented 10 years ago

From ulf.nor...@gmail.com on November 16, 2011 02:09:51

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.

Status: Accepted
Labels: Type-Enhancement Priority-Low Emacs

UlfNorell commented 10 years ago

From david.wa...@gmail.com on November 16, 2011 02:22:33

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.