blob: c0946f6562d3eafbf7616046e2745f7ac61d0c26 (
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>Mulitple modes for Emacs</h2>
<p>
Emacs has a mechanism for customizing the editing behaviour of buffers
based on their <i>major mode</i>. A buffer can only have one major
mode, but in literate styles of programming and proving we want to mix
program text with documentation in a single file. A way of
multiplexing major modes is needed, so that different regions of a
buffer can be edited in different modes. One approach may be to use
"views" onto untangled buffers, although it isn't clear how search and
replace, etc, should behave in this case.
</p><p>
The <a href="http://mmm-mode.sourceforge.net/">MMM mode</a> Emacs
add-on allows multiple-modes in a similar way, and was originally
designed for the situation where you have a script embedded in an HTML
page.
This project
might try applying MMM mode for Proof General
with Coq and Isabelle/Isar, as a feasibility demonstration.
</p><p>
<b>Skills:</b>
A passion for Emacs and Emacs Lisp.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
|
