2 files changed, 11 insertions, 8 deletions
diff --git a/html/projects/pgip.html b/html/projects/pgip.html
index 22cc654b..073edd06 100644
--- a/html/projects/pgip.html
+++ b/html/projects/pgip.html
@@ -4,6 +4,7 @@ PGIP is a protocol for interactive proof to be used in the next
 version of Proof General.  It is based around the present protocol,
 but implemented with a standard collection of messages rather than
 different messages for different proof assistants.  An outline of PGIP
+and an experimental DTD
 is given in the <a href="/home/da/drafts/#white">white paper</a>.  A
 first implementation of PGIP will consist of (1) a filter (or
 modification of the output routines) for an existing proof assistant,
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>