[Agda] problem with refine

[Dan Licata]

Hi everyone,

I'm having a problem with the 'refine' feature of the emacs mode.  It
may be the same issue as

http://code.google.com/p/agda/issues/detail?id=130&sort=type

but I'm seeing slightly different behavior:

1) When refining a hole containing a name defined in the same file as
the hole, the full path to the name gets inserted, which isn't a valid
way to refer to that name at that point.

2) bound variables are fine, as are names imported from a separate file

Here's an example:

  open import lib.Prelude
  -- contains
  --   data Unit : Set where
  --     <> : Unit
  
  module misc.RefineBug where
  
    data U : Set where
      * : U
  
    test0 : U 
    test0 = {! * !}    -- BAD: refines to misc.RefineBug.*
  
    test1 : U -> U
    test1 u = {! u  !} -- GOOD: refines to u
  
    test2 : Unit
    test2 = {! <> !}   -- GOOD: refines to <> because it's coming from another file


Are there any workarounds until this gets fixed? I was going to show off
Agda's emacs mode to some people, but not without refine... 


Another question: is there a way to set what unicode symbols are used
for forall and -> and \ ?  I have a bunch of code that already uses
\rightarrow.


Thanks!
-Dan