[Agda] Agda2 emacs mode - yellow highlighting

[Andrew Pitts]

I have a question about how to use the Agda2 emacs mode more effectively in the case that one’s Agda code goes yellow because of overzealous use of implicit arguments. 

If I select a piece of yellow-highlighted code, is there a command to replace the region with code in which all implicit arguments are made made visible as holes?

For example, in 

f : {A : Set}{a : A} → A
f {A} {a} = a
g : (A : Set) → A → A
g A a = f 

the last “f” will be highlighted in yellow and I would like a key stroke that causes the code to become

f : {A : Set}{a : A} → A
f {A} {a} = a
g : (A : Set) → A → A
g A a = f {?} {?}

Supplementary question: there is a global command in Agda2

C-c C-x C-h (Toggle display of hidden arguments)

Can someone give me an example of what it is supposed to do? (I naively thought it might display all the hidden arguments.)

Andy Pitts