[ProofPower] PP and XML

[Roger Bishop Jones]

On Tuesday 24 January 2006 15:30, Gregg Reynolds wrote:

> As it stands now, sieve et al. do a pretty good job, and are
> generic enough to support all kinds of LP stuff.  You could
> probably do interesting XMLish things with sieve as it stands.
>  An obvious enhancement would be to replace =FOO expressions
> with <FOO...> tags of some sort, and to require a </FOO...>
> endtag.

My system involves a translation between ProofPower documents 
with sieve directives and XML documents using XML elements 
instead of the directives.
The formal text is the same in the XML document except that:
the non ascii characters are given as named entities (the name in 
HTML4 if its in there) or as UNICODE characters in the form 
"&#xdddd;" .  These files are ascii, which is a subset of utf-8, 
but you still get all the UNICODE characters this way.

The XML document is the master in the cvs repository, but I 
translate to ProofPower document and use xpp to edit the formal 
text or to work with ProofPower.
This means that the formal text is not cluttered with XML markup, 
and using XML markup for the surrounding document structure is 
not onerous.

One way to adapt ProofPower to unicode would be:

1.	Introduce %#xdddd% as a way of representing arbitrary unicode 
characters.
2,	Write a translator between pp .doc format and utf-8.
3.	Integrate the translator into various bits of software such as
        xpp, docsml, pp.

This would minimise the upheaval to ProofPower.
Of course, this is not the same as getting ProofPower to work 
nicely with XML, but the latter may only need a translation 
between sieve directives and XML markup.

Then you need a nice editor (though for applications involving 
only the existing character set xpp would still be OK).
I'd prefer to use emacs if I knew how to get it to do the right 
thing.

Roger Jones






> On the other hand, I don't think it's wise to be too religious
> about XML.

I'm not religious about XML (or anything else) but I am using it.

I am interested to know what your emacs setup is for editing 
fancy character sets.
I tried to get it to work for me but never succeeded, so I 
continue to use xpp for ProofPower even though I use emacs for 
everything else.