[Agda] "Problem encountered. The *ghci* buffer perhaps can explain why"

[Nils Anders Danielsson]

On 2010-07-10 12:24, Robert Rothenberg wrote:
> I'm having trouble with Agda, installed from Ubuntu packages. "File
> mode specification error. The *ghci* buffer perhaps can explain why".
> In the buffer,
>
>    <interactive>:1:0: Not in scope: `ioTCM'
>
>    <interactive>:1:48: Not in scope: `cmd_write_highlighting_info'
>    Prelude>  ioTCM "/home/rr/src/Agda/Kripke.agda" Nothing ( cmd_goals
> "/home/rr/src/Agda/Kripke.agda" )
>
>    <interactive>:1:0: Not in scope: `ioTCM'
>
>    <interactive>:1:48: Not in scope: `cmd_goals'
>    Prelude>

Can you show the rest of the buffer contents as well?

--
/NAD