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 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. 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. 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). 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. Roger _______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com