The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 03/01/2016 02:50 AM, Pierre-Marie Pédrot wrote:
> On 01/03/2016 10:25, Enrico Tassi wrote:
>> If a brave one really wants to add to CoqIDE handy utf8 input mode, I'd
>> suggest copying the one we had in Matita:
> 
> 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.

Indeed, I use IBus for east-asian scripts and it works nicely there. I 
haven't used it to input symbols, but it's a cool idea!

Quick sampling from Github gives the following tokens as a few examples of 
Unicode being used in Proof Scripts:

  Γ Π Φ Ψ φ ← → ↦ ↾ ⇓ ∅ ∈ ∉ ∖ ∧ ∨ ∩ ∪ ≅ ≡ ≢ ≤ ≥ ≫ ≼ ⊂ ⊄ ⊆ ⊈ ⊑ ⊗ ⊣ ⊤ ⊥ ⋃ ⋅ ■ □ 
▷ ● ◯ ★ ✓ ⟨ ⟩ ⟶ ⟾

Is there a way for me (from Emacs) to query IBus, so I can help users input 
these characters? Otherwise, does IBus have a good story about 
discoverability?

Clément

Attachment: signature.asc
Description: OpenPGP digital signature