From f1e36dc74e323fa869ff955a633ce55a62fe621f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 16 Jul 2000 15:18:32 +0000
Subject: Modified, now white paper contains DTDs (soon)

---
 html/projects/pgml.html | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

(limited to 'html/projects/pgml.html')

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> 
-- 
cgit v1.2.3