Re: [isabelle] Remaining reasons for Proof General

Am 12.11.2013 16:22, schrieb Makarius:
> On Tue, 12 Nov 2013, Joachim Breitner wrote:
>> Ideally most of the issues that we discussed in this thread about
>> symbols are actually independent from whether we edit Isabelle
>> theories or love letters (\he gives ♡ ;-)), so that we can use
>> upstream resources when solving them.
> This is an important observation.  The new Isabelle/jEdit manual describes
> the situation as follows:
>   \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
>   could delegate the problem to produce Isabelle symbols in their
>   Unicode rendering to the underlying operating system and its
>   \emph{input methods}.  Regular jEdit also provides various ways to
>   work with \emph{abbreviations} to produce certain non-ASCII
>   characters.  Since none of these standard input methods work
>   satisfactorily for the mathematical characters required for
>   Isabelle, various specific Isabelle/jEdit mechanisms are provided.

As a matter of fact: The Linux' XCompose input method [1] works fairly
well with Isabelle/jEdit. For example, I use my right windows key as
compose key, allowing me to use Compose + / + \ to enter ∧ in any text.
Same for Compose + g + a for α ... and many more.

Using this in Isabelle/jEdit yields the result I'd expected, i.e. no
visual difference to using jEdits abbreviations here.

Hence, in theory, a sophisticated user could have different levels of
input abbreviations (very often used ones: jEdit, not so often: Compose,
seldomly: explicit completion), where the first ones can even share the
same codes (f.ex. < + = for ≤ and Compose + < + = for ⇐ )

- René

[1] I probably am using the wrong nomenclature here...

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift

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