blob: 52b3d3f125683a0c2b16ca66dfb334465407107f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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>
|
