[Agda] command line type checker vs interactive

[Andrés Sicard-Ramírez]

On 31 December 2015 at 09:30, Sergei Meshveliani <mechvel at botik.ru> wrote:
> Year or two ago, similar settings worked.
> But this year, it says only  "Another command is currently in progress".

Which is the output of

  $ type agda

?

After loading (C-c C-l) the file

postulate
  Foo : Set


which is the content in the Emacs buffers *Messages* and *agda2*?

-- 
Andrés