Re: [isabelle] Remaining reasons for Proof General
For completeness here are my own remaining reasons for Proof General,
which are really the last bits.
* Use of ispell to spell-check the "text" parts of theories (the
latex-oid formal source).
I think jEdit VoxSpell will do the job after some fine-tuning. In
particular the token language needs to be taken into account to
distinguish informal from formal text.
* Reformatting of plain ASCII or "text" parts with fill-paragraph.
It should be reasonably easy to reshape the jEdit action
format-paragraph to work more like the old Emacs operation. It
especially needs to distinuish a given margin for informal text vs.
the overall "wrap margin" of the source file.
From the above you can guess how I've edited the new Isabelle/jEdit manual
some weeks ago: using Proof General in offline mode.
Hopefully that was the last time that such oddities happened. Once that
the Isabelle document preparation system is integrated into
Isabelle/jEdit, there will be little reasons to look back on ancient
This archive was generated by a fusion of
Pipermail (Mailman edition) and