I have to disagree to that one needs syntax highlighting and autofilling to be productive in Agda. I have written a fair amount of agda code in Acme, which has

I have to disagree to that one needs syntax highlighting and autofilling to be productive in Agda. I have written a fair amount of agda code in Acme, which has neither. Rather I find these bells and whistles distracting — and prefer giving my complete attention to the task at hand. I think that writing agda code interactively in Emacs is fine, but it is certainly not the only way to write good agda code. In fact writing without the interactive support encourages better code structure. One is more likely to factor a complicated line into several help terms (using 'where', for example), which makes the code more readable.