Unicode input in find/replace

[barrettj12]

At the moment, Unicode input doesn't work in find/replace. While this would be nice to have (if possible), it's not essential.

The real problem is that \ still starts Unicode input mode, so it is impossible to type a \ in the find bar. If you type \ twice, it will enter a backslash somewhere in the Agda file, not in the find bar. This makes it very hard to do regex searches.

Somehow this problem doesn't exist for file search (although you still can't use Unicode input there).

[banacorn]

Thank you for reporting this. I've been able to reproduce the problem.

The condition for triggering the Unicode input mode when typing \, could depend on this context thing. We need to find the correct context so that \ won't trigger anything in the find/replace box.

[barrettj12]

If possible, it would actually be quite useful to have Unicode input in find/replace. You would have to ensure that the resulting character ends up in the find/replace bar, rather than the document. Not sure how possible/feasible this is.