[Agda] help with math symbols

[Serge D. Mechveliani]

On Wed, Aug 08, 2012 at 10:36:04AM +0200, Nils Anders Danielsson wrote:
> On 2012-08-04 10:17, Serge D. Mechveliani wrote:
>> Guillaume Brunerie <guillaume.brunerie at gmail.com> asks
>> (on 03 Aug 2012)
>>
>>> And what's the output of
>>>
>>> sh -c "agda-mode locate"
>>
>>
>> The same:
>> /home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el
>>
>> -- without Newline in the end.
>
> Interesting. Can you please run the following commands in Emacs (for
> instance by using M-:) and post the output here?
>
> (shell-command-to-string "echo $SHELL")
> (shell-command-to-string "echo $Agda_datadir")
> (shell-command-to-string "which agda-mode")


People,
thanks for your help attempts with the  emacs mode  for Agda.
My problem with it was that in

 (load-file (let ((coding-system-for-read 'utf-8))
                        (shell-command-to-string "agda-mode locate")))

in  .emacs,  the call  (shell-command-to-string "agda-mode locate")
evaluated to the path 
            /home/mechvel/stdin
instead of  /home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el

and, I think, in that the Agda people are distant from my computer.

Now, our Unix specialist  traced the system calls from running  emacs,
looked into my settings, and has done the following improvements.

(1) Removed the line of  `mesg y'  from  ~/.cshrc
    (I work under  tcshell).
    I do not know the meaning of this command. It was used to support 
    the `talk' facility, which is obfuscated now.

(2) Put the line   `setenv SHELL /bin/sh'
    to  ~/.login

And now,  (shell-command-to-string "agda-mode locate")  evaluates to
the needed path when  emacs  starts.

He said that each (1) or (2) fixes the problem.
He said something of this sort:
a) when  emacs  was run, the command  `mesg y'  was re-applied, and
   this has reset some path to  /home/mechvel/stdin.
b) when an user of  tcshell  sets  emacs mode for Agda,  one needs to 
   think of the effect of the command  `mesg y'  in  ~/.cshrc.

Regards,

------
Sergei