Re: [isabelle] HOLCF

On Wed, 27 Jun 2012, Christian Sternagel wrote:

Concerning usage of HOLCF in jEdit (I guess, this is for Makarius): could a translation from $ to the unicode cdot be added to the default "translation table", since typing "<space> c d o t" and then moving back in order to remove the space is slightly odd.

This is specific to HOLCF. Any global modification of the input method is apt to cause annoyances in other situations, where $ or \<cdot> are used differently / independently.

Until some better configuration for Isabelle/jEdit input methods becomes available, you can add the following line to your $ISABELLE_HOME_USER/etc/symbols file:

  \<cdot>                 code: 0x0022c5  abbrev: $

Note that etc/symbols allows to change the "code" assignment as well, but this should be done with great care, or not at all, to avoid chaos in the communication with other users.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.