aboutsummaryrefslogtreecommitdiff
path: root/html/projects/pgml.html
diff options
context:
space:
mode:
authorDavid Aspinall2000-02-29 06:19:39 +0000
committerDavid Aspinall2000-02-29 06:19:39 +0000
commitb37bf74fc2d6309a5ae3dc6b55e8488409976775 (patch)
treea6525ba2a439a8f87dcde7f4097690107ce09783 /html/projects/pgml.html
parent42cc4e49a2d2b73f0765536a5265a6ad473abfe6 (diff)
New projects directory.
Diffstat (limited to 'html/projects/pgml.html')
-rw-r--r--html/projects/pgml.html24
1 files changed, 24 insertions, 0 deletions
diff --git a/html/projects/pgml.html b/html/projects/pgml.html
new file mode 100644
index 00000000..52b3d3f1
--- /dev/null
+++ b/html/projects/pgml.html
@@ -0,0 +1,24 @@
+<h2>Specification and tools for PGML</h2>
+<p>
+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.
+</p>
+<p>
+<b>Skills:</b>
+Understanding of markup languages and tools for using and specifying them.
+Interest in representation of mathematical content.
+Necessary programming skills.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+