xplat · May 18, 2011 20:51 · wjzz · Jun 7, 2011
diff --git a/agda-wishlist.txt b/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.