[Agda] problem with C-c | (show context) in 2.1.3

[Ulf Norell]

On Fri, May 9, 2008 at 12:28 PM, Thorsten Altenkirch <txa at cs.nott.ac.uk>
wrote:

> Hi,
>
> I noticed that the "Context" command doesn't work in my configuration
> (aquamacs with agda-2.1.3). I get an error message in the *ghci* buffer:
>
> Prelude Interaction.GhciTop> cmd_context 0 (Range (Pn
> "/Users/txa/current/bug.agda" 111 8 19) (Pn "/Users/txa/current/bug.agda"
> 113 8 21)) ""
>
> <interactive>:1:15:
>    Couldn't match expected type `InteractionId'
>           against inferred type `Range'
>    In the second argument of `cmd_context', namely
>        `(Range
>            (Pn "/Users/txa/current/bug.agda" 111 8 19)
>            (Pn "/Users/txa/current/bug.agda" 113 8 21))'
>    In the expression:
>        cmd_context
>          0
>          (Range
>             (Pn "/Users/txa/current/bug.agda" 111 8 19)
>             (Pn "/Users/txa/current/bug.agda" 113 8 21))
>          ""
>    In the definition of `it':
>        it = cmd_context
>               0
>               (Range
>                  (Pn "/Users/txa/current/bug.agda" 111 8 19)
>                  (Pn "/Users/txa/current/bug.agda" 113 8 21))
>               ""
>
> when issuing C-C | anywhere, e.g. in goal 0 in the attached example.
>
> Anybody else has got this problem?


Have you installed the emacs-mode properly? Displaying the context should be
C-c C-e, so it might be that you are just using an old emacs-mode. The
el-files are in src/full/Interaction/emacs-mode and need to be copied to or
linked from somewhere emacs can find them. The details are in the readme
file I think.

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