[ProofPower] PP and XML

[Gregg Reynolds]

(sorry, sent the first try from the wrong account)

Roger Bishop Jones wrote:
> >
> > 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
> > "�" .  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.

Hi Roger,

Sounds interesting.  But if you use xpp to edit the texts, why the XML
mapping?  Do you do some kind of transformation on it?

> >
> > 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.

This would be the easiest quick fix.  A little perl script called as a
view filter would do the trick, no?
> >
> > I am interested to know what your emacs setup is for editing
> > fancy character sets.

Take a look at the leim/quail subdir in the emacs tree.  Naturally it's
not under the lisp directory but beside it.  On my windows machine, it's
c:\emacs-21.3\leim\quail; on freebsd, it's
/usr/local/share/emacs/21.3/leim/quail.  From there it should be pretty
self-evident.  Just copy one of the quail files to your private elisp
dir (~/elisp for me), rename, and edit.  To get non-ascii stuff you can
cut and paste characters from e.g. greek.el.  I don't know how to get
the right glyphs by any other method.  I do know that nxml-mode, aside
from being a very powerful XML editing mode, allows you to insert
unicode chars by name or number, so you might be able to hack some code
from there.

For characters not found in the quail files, I use a nice little unicode
editor called Babelpad for which you can google.  It's got a handy
unicode char lookup facility.  So for example, to get Z chars, I create
a dummy text file with babelpad containing the chars I want.  Then I
open the file in emacs and cut and paste the chars into my quail input
method file.  Works like a charm, although of course you need the right
font.

Don't forget to set the appropriate coding system for your files.  See
the online emacs help.  Selecting an input method is quite easy:  ctl-x
ctl\ for a prompt.

Since cygwin provides me with a near-complete posix environment and I
have nt-emacs, I've not yet taken the trouble to figure out how to do
the same thing on a unix platform, but I imagine it isn't too terribly hard.

Here's a snippet from my zbar.el quail input mode file:

(require 'quail)

(quail-define-package
 "zbar" "Z^" "Z" nil
 "Z-bar Grammar Definition Language
Post-fix selectors:
  `  - Z¯ ops
  $  - set ops
  ~  - logical ops
  /  - Greek characters
Post-fixers only needed for ambiguities."
 nil t t t t nil nil nil nil nil t)
)

(quail-define-rules
  ("<|`" ?⦉) ;; left binding bracket  (no font support yet?)
  ("<|`" ?⦊) ;; right binding bracket (no font support yet?)
...
  ("A~" ?∀) ;; universal quantification (forall)
  ("E~" ?∃) ;; existential quantification (thereis)
...
 ("in$" ?∈) ;; membership
 ("!in$" ?∉)
...
  ("a/" ?α) ;; alpha
  ("b/" ?β) ;; beta
  ("g/" ?γ) ;; gamma
...)

I like the postfix input method, so I've chosen different postfix
discriminators to select characters from different repertoires.  I can
type symbolic formulae quite easily and rapidly this way.

This email is utf-8 encoded, so with the right font you should see the
symbols with the possible exception of the binding brackets; most fonts
don't support  them yet.  Code2000 does, though.
http://home.att.net/~jameskass/

It's pretty simple on Windows, because font handling in nt-emacs is
nicely integrated with the Windows system.  I've had less luck on Unix
since I've never managed to wrap my head entirely around the font
management architecture of emacs+X11.  If you can figure that out let me
know.

Hope it helps,

gregg