[Agda] help with math symbols

[Dominique Devriese]

Serge,

What output do you get if you run the command "agda-mode locate" in a
shell (outside of emacs)?

Thanks
Dominique

2012/7/30 Serge D. Mechveliani <mechvel at botik.ru>:
> (1) With empty  ~/.emacs,  emacs  loads without error.
>
> But according to README of Agda-2.3.0.1, I set  ~/.emacs  as
>
> (load-file (let ((coding-system-for-read 'utf-8))
>                 (shell-command-to-string "agda-mode locate")))
>
> And now, emacs loads with a certain error:
>                                            > emacs --debug-init
> reports
> ---------------------------------------------------------------------
> Debugger entered--Lisp error: (file-error "Cannot open load file"
> "/home/mechvel/haskell/agda/lib-0.6/src/Data/stdin:  is not a tty
> /home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el")
>   load("/home/mechvel/haskell/agda/lib-0.6/src/Data/stdin: is not a tty
> \n/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el" nil nil t)
>   load-file("stdin: is not a tty
> \n/home/mechvel/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el")
>   eval-buffer(#<buffer  *load*> nil "/home/mechvel/.emacs" nil t)  ;
> Reading at buffer position 114
>  load-with-code-conversion("/home/mechvel/.emacs" "/home/mechvel/.emacs" t t)
>  load("~/.emacs" t t)
>  #[nil "
> ---------------------------------------------------------------------
>
> a) The directory  ~/haskell/agda/lib-0.6/src/Data/
>                                                    (~ = /home/mechvel)
>    contains many files but does not contain  stdin.
>
> b) ~/.cabal/share/Agda-2.3.0.1/emacs-mode/agda2.el    does exist.
> c) The  putStrLn "Hello!"  program complies and runs correctly.
>
> d) With this,  emacs  still shows correctly specific math symbols
>    in the  .adga  files,
> but I cannot correctly _input_ these math symbols. For example,
> my program
>           open import Nat
>           ...
>           f : \bn
>           f = zero
> does not compile, the compiler takes  \bn  as lambda.
>
> Please, how to fix the setting?
>
>
> (3) http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Docs.UnicodeInput
> writes
> --------------------------------------------------
> How can I write Unicode characters using Emacs?
> The Agda Emacs mode turns on a special input method [..]
> This input method is highly customisable
>
> (via   M-x customize-group agda-input  ).
>
> By default you can insert a number of symbols by typing their
> TeX/LaTeX names. For instance, if you type \forall then Б┬─ gets inserted
> Some characters have key bindings which have not been taken from LaTeX
> (typing \bn results in Б└∙ being inserted, for instance)
> [..]
> --------------------------------------------------
>
> The error of (1) still keeps emacs working, with many respects.
> So, I tried in  emacs,  in the menu dialogue:
>
>   >  Alt-x
>   e> M-x
>   >  customize group
>   e> Customize group (default emacs):
>   >  agda-input
>   e> Customize group (default emacs): agda-input  no match
>
> -- it somehow fails to customize.
>
> Thank you in advance for advice,
>
> ------
> Sergei
> mechvel at botik.ru
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda