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 [email protected] http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
