The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Pierre-Marie,

> Notwithstanding this whole discussion, I'm not sure this is the rôle of the
> editor to implement a nice input method. KISS! Plus GTK-sourceview 2.x is a
> really crappy editor, and interfering with what the user types is often 
> buggy.

I agree that we should go for what Microsoft calls an IME 
(https://en.wikipedia.org/wiki/Input_method) for typing math symbols. It 
would make more sense to type the same way when writing an email or a 
document as when typing in Coq. Not sure, though, if IMEs can be nested, e.g. 
if a Japanese IME can be used in combination with a math IME. Does this work 
on Linux?

If I understand you right, something like this exists for Linux. Could you 
give a few more pointers?

The Lean project gives me some hope that we will have something like this for 
Windows as well. If we agree on this is the way to go, I could try to use 
some contacts to push this within MS. I might also be able to come up with a 
prototype. I think there is some open source SW which can be tweaked to 
behave like a configurable IME.

Not sure what to do on Mac, though. Does it come with a configurable IME like 
Linux?

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928