[ProofPower] PP and XML

[Rob Arthan]

On Sunday 29 Jan 2006 8:58 am, Roger Bishop Jones wrote:
> On Saturday 28 January 2006 16:17, Rob Arthan wrote
>
>...
> I had a go with Proof General a few years back but didn't get
> anywhere worthwhile.  I was not unsuccesful in getting the
> X-symbol stuff to work satisfactorily for me, and though setting
> up Proof General for a new tool is alleged to be really simple,
> I tried and failed.
> Emacs seems to have moved on since then and I am under the
> impression that there is a standard font issued with emacs which
> has very wide coverage.

Perhaps Proof General has moved on too. No doubt David Aspinall would tell 
you.

>...
> I am upgrading my XML stuff and will consider whether the
> ProofPower XML-> HTML aspects of it can be tidied up enough to
> be made more generally available while I am on the job.
>

Great!

> I am be interested to know what you think of the idea of allowing
> %#xdddd% keywords for aribitrary unicode characters in
> ProofPower which I mentioned in an earlier post.

It sounds like a good plan. We'd need to figure out a neat way of defining the 
docsml and doctex translation schemes for these characters. Since the 
existing ProofPower character set is in the range #x0080 - #x00FF which won't 
overlap the official Unicode character assignments for any of the symbols, 
the existing encoding remapped into UTF-8 and the Unicode encoding could 
coexist, with your proposed representation giving a standard ASCII encoding 
of our scheme.

The latest version of Motif supports UTF-8, so it should be possible to switch 
xpp between the existing encoding and UTF-8.

Regards,

Rob.