blob: 67680b8f9d923f2dd50dfd14deb2e5aa75f434ef (
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>Integrating block-structured development and outline mode</h2>
<p>
Emacs already provides powerful outline facilities (cf. the
outl-minor-mode setup for the well-known auc-tex package).
Similarly, proof systems such as Isabelle/Isar are inherently based on
block-structured proof texts, with compositional proof checking.
</p><p>
But Proof General currently offers a mostly linear model of
incremental script management. The aim of this project is to extend that
model to a hierarchic one: e.g. sub-proofs could be suppressed in the
presentation, or even temporarily suspended (to achieve top-down
development).
</p><p>
Outline support would be useful for the large scale structure of formal
developments as well, e.g. support the basic arrangement into logical
section (cf. Coq), or even just traditional layout-based ones (cf. LaTeX).
</p>
<p>
<b>Skills:</b>
Some understanding of the workings of Emacs outline mode and Proof
General script management. Good portion of Emacs lisp knowledge.
</p><p>
<b>Proposer:</b>
<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
</p>
|
