diff options
Diffstat (limited to 'html/projects/outline.html')
| -rw-r--r-- | html/projects/outline.html | 26 |
1 files changed, 26 insertions, 0 deletions
diff --git a/html/projects/outline.html b/html/projects/outline.html new file mode 100644 index 00000000..67680b8f --- /dev/null +++ b/html/projects/outline.html @@ -0,0 +1,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> + |