Modified, now white paper contains DTDs (soon)

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>