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
\<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