diff options
Diffstat (limited to 'html/projects/pgml.html')
| -rw-r--r-- | html/projects/pgml.html | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/html/projects/pgml.html b/html/projects/pgml.html index 52b3d3f1..46cdd960 100644 --- a/html/projects/pgml.html +++ b/html/projects/pgml.html @@ -3,14 +3,16 @@ PGML is the proposed logical markup language for future versions of Proof General. The basic version legitimizes the present markup scheme which is used by Proof General (based on 8-bit characters). -Ideas for PGML are described in the white paper -<a href="/home/da/drafts/#white">here</a>, but no complete description or -DTD is given there. This project is to specify PGML using XML or SGML, -and develop some tools for using it. Various tools are desirable, -including: (1) a display tool which displays PGML inside Emacs, or -converts it to HTML for display by a web browser; (2) a filter or -revised version of LEGO which converts its 8-bit markup into PGML, for -testing purposes. +The ideas for PGML are described in the white paper +<a href="/home/da/drafts/#white">here</a>, and an experimental +DTD is given there. This project is to refine the specification +of PGML, and develop some tools for using it. Various tools are desirable, +including: (1) translation tools which convert PGML to various other +formats, such as HTML and LaTeX. (2) a display tool which displays PGML +inside Emacs, or converts it to HTML for display by a web browser; +(3) a filter or revised version of LEGO which converts its 8-bit markup +into PGML, for testing purposes. We need the last tool for other +proof assistants too. </p> <p> <b>Skills:</b> |