[Agda] emacs problems

[Martin Escardo]

Try deleting the hidden .*.el file for your agda file. I once had a 
similar problem with emacs/agda that was solved by that. Martin

Ulf Norell wrote:
> 
> On Wed, Jun 17, 2009 at 12:01 AM, Andreas Buechele 
> <andreas.buechele at googlemail.com 
> <mailto: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
> 
> 
> ------------------------------------------------------------------------
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda