[Agda] help with math symbols

[Dominique Devriese]

Sergei,

> Now, from the start
> (sorry, initially I confused the  emacs  report a bit):
> ~/.emacs  contains
>
>  (load-file (let ((coding-system-for-read 'utf-8))
>                  (shell-command-to-string "agda-mode locate")))
>
> Thanks to my colleage, he noticed that the expression
>                           (shell-command-to-string "agda-mode locate")
> evaluates to  "/home/mechvel/stdin".
> And it is natural to suppose that in my installation case this value
> rather should be
>        "/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el".
> Right?

Yes, that's what it should evaluate to and your solution works around
the problem but will not work well after Agda updates. The question is
why (shell-command-to-string "agda-mode locate") doesn't evaluate to
"/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el".  The
emacs function shell-command-to-string is supposed to return a string
containing the output of the shell command you pass it. But you say
that the "agda-mode locate" command yields the correct result in the
shell but not when run using shell-command-to-string.

The error messages in your previous mail suggest that the problem may
be caused by something in your shell startup files (.bashrc, .profile
etc.) that assumes that stdin is attached to a tty (an interactive
terminal), while under shell-command-to-string, emacs probably
attaches it to a pipe or something.

Dominique