[Agda] "Not in scope" error

[Nils Anders Danielsson]

On Thu, Jul 3, 2008 at 10:19 AM, Antoine Durand-Gasselin
<adg at cs.st-and.ac.uk> wrote:
>
> I have a problem however: I have the feeling that the emacs mode
> regularily reloads the entire file, which is time consumming on
> large files. For exemple everywhen I make-cases.

Yes, this is annoying, but requires some work to fix. I have been told
that the current UI started out as a quick hack, to get something
working. A more principled design, allowing for improvements like this
one, would be nice. However, since the current UI works reasonably
well this is not at the top of our priority lists.

I suggest that you use smaller files.

-- 
/NAD