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 things anyway.


	Makarius





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