xplat/agda-wishlist.txt

## agda-wishlist.txt
= agda-mode

* C-c C-c should accept an expression and create a with.  (does it do this already?)  Or there should be another key combo to create a with.
* C-c C-c should work from inside complex expressions, not just when the RHS is a single hole.  Variables know where they are bound, and the RHS can be duplicated and specialized.
* A key combo to rename a variable in scope.  [should this include occurrences outside the current module?  in general that would require an IDE-style project system ...]
* Undo without reload.
* Preview for agsy and null refine.  [maybe redundant with the above]
* A key combo to suck the region into a hole.
* A key combo to expand a hole to the next higher node in the syntax tree.
! More consistent yellow highlighting during smart editing without reload.
! Don't create case splits that won't compile.  [moar detail]

= records

* Record syntax should work as a block too, not just with explicit brackets.
* Record syntax should allow pattern matching when defining a function.
* Record fields should be in scope when defining further fields.
* Individual record field definitions should be able to have where clauses.
* A record field should be definable by an inline data declaration if its type permits.

= misc syntax

* Mixfix sections: ‘_+ 3’ and ‘3 +_’ should translate to ‘\lambda x -> x + 3’ and ‘_+_ 3’ respectively.
	= agda-mode

	* C-c C-c should accept an expression and create a with. (does it do this already?) Or there should be another key combo to create a with.
	* C-c C-c should work from inside complex expressions, not just when the RHS is a single hole. Variables know where they are bound, and the RHS can be duplicated and specialized.
	* A key combo to rename a variable in scope. [should this include occurrences outside the current module? in general that would require an IDE-style project system ...]
	* Undo without reload.
	* Preview for agsy and null refine. [maybe redundant with the above]
	* A key combo to suck the region into a hole.
	* A key combo to expand a hole to the next higher node in the syntax tree.
	! More consistent yellow highlighting during smart editing without reload.
	! Don't create case splits that won't compile. [moar detail]

	= records

	* Record syntax should work as a block too, not just with explicit brackets.
	* Record syntax should allow pattern matching when defining a function.
	* Record fields should be in scope when defining further fields.
	* Individual record field definitions should be able to have where clauses.
	* A record field should be definable by an inline data declaration if its type permits.

	= misc syntax

	* Mixfix sections: ‘_+ 3’ and ‘3 +_’ should translate to ‘\lambda x -> x + 3’ and ‘_+_ 3’ respectively.