The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

On 03/01/2016 12:05 PM, Soegtrop, Michael wrote:
> 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?

This weekend, I've tried XIM (The X Input Method).
I guess that is the oldest input method for X.

Here are my notes what I needed to do to get what I needed.

  
https://github.com/matej-kosik/coq/tree/v8.5__Show_Tree__BLANK__propositional_logic__1#configuring-xim-the-x-input-method

Then I was able to type the UNICODE glyphs I needed
(in coqtop running in my X terminal
 in CoqIDE
 in Emacs
 and just about anywhere where I bothered to test ... ⊤ ⊥ ¬ ∧ ∨ → ↔ ℙ)

There are much more fancier alternatives but this one (XIM) worked for me 
well.