[Agda] emacs problems

Ulf Norell ulf.norell at gmail.com
Wed Jun 17 08:32:50 CEST 2009


On Wed, Jun 17, 2009 at 12:01 AM, Andreas Buechele <
andreas.buechele at googlemail.com> wrote:

> Hi *,
>
> I'm using emacs-23 and some strange behaviour of the Agda interface
> arise. I'm using Agda frequently and everything worked fine till yesterday.
>
> In some of my new source files the "context and goal type" feature isn't
> working. If I press "Ctrl-," the status line says "Wrote /tmp/***" and
> the ghci buffer says:
>
> ---8<---
> Prelude Agda.Interaction.GhciTop> cmd_goal_type_context
> Agda.Interaction.BasicOps.Normalised 0 (Range [Interval (Pn
> "SomeAgdaFile.agda" 2260 52 41) (Pn "SomeAgdaFile.agda" 2260 52 41)]) ""
>
> <interactive>:1:254: lexical error at character '\EOT'
> Prelude Agda.Interaction.GhciTop>


That is indeed very strange. The file is working perfectly for me (MacOsX +
Aquamacs-22). What operating system are you using?

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20090617/b6df7c99/attachment.html


More information about the Agda mailing list