[Ur] unurlify

[Adam Chlipala]

Gergely Buday wrote:
> what does this mean?
>
> 1492:24-1500:31: Don't know how to unurlify type in JavaScript
> Can't unurlify
> t:  source
>
> Is it not possible to use sources in client code?
>    

No, client code can certainly do many useful things with sources.  
However, in this case, you are probably using an RPC whose return type 
involves [source].  Currently such RPCs are not supported, but now I 
don't see any reason why I couldn't add support.  Was it your intention 
to return a [source] from an RPC?

(The message has to do with the encoding of RPC results in the format 
used within URLs.)