[Agda] Agda-mode problems in 2.3.2

[Peter Divianszky]

I'm not sure but maybe 'agda-mode compile' is needed too?

Peter

On 01/25/2013 06:28 PM, Dominic Mulligan wrote:
> Hi,
>
> I have just updated my version of Agda to 2.3.2.  However, apparently
> something has gone wrong with agda-mode as half of the functionality
> that was there prior to the update is missing.  In particular, I am
> unable to use auto (C-c C-a), display a goal and its context (C-c C-,)
> or give a term by hand to solve a goal (C-c C-space).  Issuing these
> commands inside a hole results in ... nothing, and there appears to be
> no Agda menu entry for them either (though the Agda menu has changed
> between versions, with more entries than there were before --- for
> instance I now have entries like `Information about character at point'
> that were not there prior to the update).  I can still load a file fine
> with C-c C-l, get syntax highlighting, etc.
>
> Further, Agda no longer seems to be issuing type checking errors.  When
> it encounters a type error it merely underlines the problem in red in
> the source file, but no buffers (Agda information, Agda2, etc.) contain
> an error message.
>
> What's going on?
>
> Installed Agda by:
>
> cabal update
> cabal install --global Agda
> agda-mode setup
>
> (ghc --version: 7.4.1, agda-mode
> locate: /usr/local/share/Agda-2.3.2/emacs-mode/agda2.el,
> agda --version: Agda version 2.3.2, emacs --version: GNU Emacs 23.3.1,
> Ubuntu 12.04.1 LTS 32 bit.)
>
> Thanks,
> Dominic
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>