Re: [isabelle] Remaining reasons for Proof General



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.


I’m not sure if this is actually the case, though, as I cannot tell which editing features are provided by jEdit by default, which are provided by jEdit but instrumented and configured using the Isabelle plugin, and which are genuine Isabelle plugin features.

The new manual should give some impression what is jEdit and what is Isabelle/jEdit. It is the first go on such a manual, though, and many fine points might be missing or difficult to understand.


	Makarius


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