diff options
| author | David Aspinall | 2000-02-29 06:19:39 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-02-29 06:19:39 +0000 |
| commit | b37bf74fc2d6309a5ae3dc6b55e8488409976775 (patch) | |
| tree | a6525ba2a439a8f87dcde7f4097690107ce09783 /html/projects/pgml.html | |
| parent | 42cc4e49a2d2b73f0765536a5265a6ad473abfe6 (diff) | |
New projects directory.
Diffstat (limited to 'html/projects/pgml.html')
| -rw-r--r-- | html/projects/pgml.html | 24 |
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> + |
