aboutsummaryrefslogtreecommitdiffhomepage
path: root/html/projects/scrgen.html
blob: d65b477f5dc5d458755b5671aeb73ca3a9ae6c3d (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
25
26
<h2>Script General</h2>
<p>
Proof General is based around a core system of script management
for proof scripts.  But the idea of script management is not
restricted to proof assistants, it makes sense for many interactive
scripting languages.  It deserves to be better known and used.
A worthwhile project would be to rewrite the core script management
features of Proof General so that they could work for arbitrary
interactive scripting languages, and instantiate to Proof General as
well as languages such as ML, Haskell, LISP, Scheme, Python, and
even Emacs Lisp itself.
</p>
<p>
An alternative version of this project is to implement a 
generic basis for script management which does <i>not</i> depend on 
Emacs, but uses a similar protocol to communicate with other
text editors or display widgets.  This could be implemented in
SML, OCaml, Java, C++, or any other suitable language.
<p>
<b>Skills:</b>
Proficient Emacs Lisp (or other programming language), 
knowledge of scripting languages desirable.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>