On 13 Aug 2012, at 10:59, Roger Bishop Jones wrote:

> On Monday 13 Aug 2012 13:12, Rob Arthan wrote:
> 
>> Jon is using Anthony Hall's Z Word Tools, which actually
>> go quite a long way to bridging this gap. Z Word Tools
>> allows you to prepare a Z specification inside a Word
>> document and project out the Z in a format suitable for
>> processing by other tools such as Fuzz or CZT.  Anthony
>> and I have talked about adding ProofPower as a list of
>> targets, but it got deferred pending some work I was
>> doing on getting ProofPower to support UTF-8. I have a
>> prototype converter from a UTF-8 format to the
>> ProofPower formats, but it would require a bit of
>> handcranking to get it to convert CZT input into
>> ProofPower input. I don't know how much work would be
>> involved in getting Z Word Tools to output something
>> that ProofPower can eat (e.g., my UTF-8 format).
> 
> That's all very interesting, and it would be good to get 
> ProofPower into a less eccentric position on document 
> formats.
> 
I agree.

> I have myself recently found myself using utf8 in LaTeX 
> documents (when I wanted to get some Greek in), and may find 
> myself wanting to prepare documents which have both Greek 
> and ProofPower as a result of furthering my modelling of 
> aspects of Aristotle's Organon and Metaphysics.
> 
> I see from reading a little about this in either or both of 
> emacs and PERL that the support of arbitary encodings rather 
> than specifically of one or more of the UTF variants seems to 
> be thought desirable (and is realised I think in emacs).
> From this point of view one might consider making the 
> ProofPower encoding "respectable" by doing whatever is 
> needed for it to be supported by such generic software.

Surely just accepting and outputting UTF-8 will achieve that, won't it?

> It might then be possible to convert between ProofPower's 
> encoding and others using some standard generic utility 
> (perhaps emacs does this).
> [On further grubbing around I think the "generic" facilities 
> support a fixed, if perhaps long, list of encodings.
> I haven't found anything which appears to work from a soft 
> definition of an encoding.]
> 
> Somewhere in this maze I think there are ways of telling 
> that the greek alphabet does consist of alphabetic 
> characters and hence perhaps should be admitted in 
> ProofPower identifiers.

That is somewhat orthogonal to how I would plan to do the ProofPower side of 
this in the first instance.

> When you speak of "my UTF8 format", presumably you are 
> talking about the mapping between the ProofPower extended 
> characters and the unicode character codes (which wouldn't 
> be specific to UTF8).

Yes.

> 
> Incidentally, my hacks for making HTML from ProofPower 
> sources, though they once translated into image references, 
> were switched a while back to use unicode entities (not UTF 
> but ascii things like &#xxxx;) so I do have a mapping 
> between the two (though incomplete).
> Not good enough to be of any help to you, but I would fall 
> in line with whatever mapping you have come up with if I 
> ever find myself augmenting or fixing it.

When I got some time. I will tidy up the little prototype converter I wrote and 
make it available for you to have a look at.

Regards,

Rob.


_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to