New projects added

3 files changed, 63 insertions, 9 deletions

diff --git a/html/projects.phtml b/html/projects.phtml
index 426bec3f..51320b35 100644
--- a/html/projects.phtml
+++ b/html/projects.phtml
@@ -13,15 +13,18 @@ research.  They would be ideal projects for interested students
 or researchers.
 </p>
 <p>
-For more information on a project, click on its title.
+The projects are divided into those which are specific to Proof
+General, and those which would be useful more widely and do not depend
+on Proof General.  For more information on a project, click on its
+title.
 </p>
 
+<h2>Projects involving Proof General</h2>
 <ul>
 <li><?php pgproject("coqpbp","Proof-by-pointing support for Coq") ?></li>
+<li><?php pgproject("coqfile","Multiple file handling support for Coq") ?></li>
 <li><?php pgproject("isapbp","Proof-by-pointing support for Isabelle") ?></li>
 <li><?php pgproject("outline","Integrating block-structured development and outline mode") ?></li>
-<li><?php pgproject("mm","Multiplexed Modes for Emacs") ?></li>
-<li><?php pgproject("scrgen","Script General") ?></li>
 <li><?php pgproject("thybrowse","A Generic Theory Browser") ?></li>
 <li><?php pgproject("pgml","Specification and tools for PGML") ?></li>
 <li><?php pgproject("pgip","A New Protocol for Interactive Proof in Proof General") ?></li>
@@ -29,6 +32,13 @@ For more information on a project, click on its title.
 <li><?php pgproject("test","A Test Harness and Test Suite for Proof General") ?></li>
 </ul>
 
+<h2>Projects not directly involving Proof General</h2>
+<ul>
+<li><?php pgproject("mm","Multiplexed Modes for Emacs") ?></li>
+<li><?php pgproject("scrgen","Script General") ?></li>
+<li><?php pgproject("corba", "Experiments with CORBA bindings for ML" ?></li>
+</ul>
+
 <p>
 Some projects involve Emacs Lisp.  This is the embedded programming
 language inside Emacs.  It is very easy to learn, since it is small,
@@ -54,18 +64,15 @@ If you are interested in working on any of these projects,
 feel free to discuss with the project proposer or on the 
 <?php link_root("devel#develmail","developer's mailing list") ?>.
 </p>
-<p>
-Note: the proposer of the project is just that; he or she does not
-guarantee to be available for formal supervision or intensive help
-with the project.  But it may be possible to find somebody else
-to do that.  Contact the project proposer first for more details.
-</p>
 
 <p>
 If you would like to use any of these ideas as a formal project
 proposal for students at your institution, please feel free
 but do <?php hlink("feedback.phtml","let us know ","Feedback form")?>
 if some work is begun, to help coordinate efforts.
+NB: the proposer of the project does not guarantee to be available for
+formal supervision or intensive help with the project (but it may be
+possible to find somebody else to do that).
 </p>
 
 <p>
diff --git a/html/projects/coqfile.html b/html/projects/coqfile.html
new file mode 100644
index 00000000..03836398
--- /dev/null
+++ b/html/projects/coqfile.html
@@ -0,0 +1,20 @@
+<h2>Multiple file handling support for Coq</h2>
+<p>
+Coq Proof General does not yet handle script management across file
+boundaries, as do the LEGO and Isabelle versions.  Script management
+for multiple files means that whenever a file is viewed in the editor,
+it is locked if it has been loaded into the current Coq session.  It
+may also mean that one can some file-level primitives of Coq, rather
+than loading each file manually in the interface.  This means that
+complete proof scripts will not usually need to be parsed by
+Proof General, solving one of the present problems with using
+Coq Proof General.
+</p>
+<b>Skills:</b>
+ Some understanding of Coq implementation, co-operation with
+ the Coq developers to get any Coq modifications (if any) incorporated.
+ Some Emacs Lisp knowledge. 
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
diff --git a/html/projects/corba.html b/html/projects/corba.html
new file mode 100644
index 00000000..f2143fc2
--- /dev/null
+++ b/html/projects/corba.html
@@ -0,0 +1,27 @@
+<h2>An Experimental CORBA binding for ML</h2>
+<p>
+The future version of Proof General may use CORBA as a communication
+mechanism between different components.  CORBA is also used by the
+Unix/Linux desktops KDE and GNOME, which the free implementations MICO
+and ORBIT.  We would like to be able to use ML to write applications
+and utilities in, to interface with other CORBA components on the
+desktop and network.  For this a CORBA binding for ML is needed.  This
+project involves the design and implementation of such a binding,
+using one of the open-source ML compilers such as Moscow ML, Poly/ML
+or OCaml (there may already be a project underway for the last of
+these).  
+</p>
+<p>
+A CORBA binding for Haskell would also be an interesting project.
+</p>
+</p>
+<p>
+<b>Skills:</b>
+Good ML programming skills and understanding of abstraction
+mechanisms, basic understanding of CORBA.
+</p><p>
+<b>Proposers:</b>
+<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a> and
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+
+</p>