[Agda] include directories and agda-mode "warping" between files

WILSON F.A.J. frank.wilson at durham.ac.uk
Tue Jul 15 12:39:27 CEST 2008


I've found that when I change the location of the agda core library [1]
it seems to mess-up warping between files. (By warping, I mean when you 
click on say, proj_1 you get taken to the definition of proj_1 in the
core library, which is located wherever you put it). 
I'm specifying the library path in the included dirs section of the
agda emacs customization page. The compiler is quite happy with this
but whatever handles the warping isnt. Whenever I click on an anchor
I see a message complaining that old library location doesnt exist 
in the minibar.

I've tried purging my working directory of all agdai and agda.el files
but this doesnt seem to work. When they get regenerated whatever is handling
the warping (the agda.el?) is still pointing to the old library location.

Does anyone know of a work around for this?

Frank 

[1] http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Libraries.StandardLibrary

-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080715/8319cf59/attachment.html


More information about the Agda mailing list