[ jEdit-devel ] Unicode escape code converter plugin or macro?

[Leston B. <bu...@fi...>]

I remember that a month or so ago, someone had written a plugin (or 
macro) that would convert a Java Unicode escape code (e.g. "\u1234") 
into the Unicode character in the edit pane. But now i can't find 
anything about it anywhere, including my archived messages from this 
list and on the community.jedit.org message boards. Does anyone remember 
  where the message about this was posted? (I have run up against what i 
think is a Java bug in my own plugin, and this other plugin would 
provide an easy way to explore this bug.)

Thanks,

Leston
bu...@uc...