From b37bf74fc2d6309a5ae3dc6b55e8488409976775 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 29 Feb 2000 06:19:39 +0000
Subject: New projects directory.

---
 html/projects/thybrowse.html | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 html/projects/thybrowse.html

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

diff --git a/html/projects/thybrowse.html b/html/projects/thybrowse.html
new file mode 100644
index 00000000..bb081fc0
--- /dev/null
+++ b/html/projects/thybrowse.html
@@ -0,0 +1,32 @@
+<h2>A Generic Theory Browser</h2>
+<p>
+Proof General has very limited mechanisms for helping the user find
+theorems and definitions during a proof.  It has notion of displaying
+a "current context" for a proof, and configuration with a proof
+engine command for searching for theorems.  It would be useful to
+extend these facilities with a <i>theory browser</i> for investigating
+the theories currently defined in a running proof assistant.  This
+involves designing a small protocol to communicate with the proof
+assistant and a generic way of displaying theories which have
+different aspects from system to system.  A way which would
+fit in well with Emacs would be to use a <tt>dired</tt>-like
+buffer.
+</p>
+<p>
+An alternative version of this project would be to write a standalone
+theory browser which uses an extension of the forthcoming Proof
+General standardized protocol for interaction (see white paper <a
+href="/home/da/drafts/#white">here</a>).  This could be implemented in
+Java, or in a functional language, Perl, C or C++, so long as a nice
+toolkit is chosen (Qt or GTK).
+</p>
+<p>
+<b>Skills:</b>
+Interface programming skills.
+Basic understanding of what theories are for several different proof
+assistants.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+
-- 
cgit v1.2.3