aboutsummaryrefslogtreecommitdiff
path: root/html/projects/mm.html
diff options
context:
space:
mode:
Diffstat (limited to 'html/projects/mm.html')
-rw-r--r--html/projects/mm.html26
1 files changed, 26 insertions, 0 deletions
diff --git a/html/projects/mm.html b/html/projects/mm.html
new file mode 100644
index 00000000..c0946f65
--- /dev/null
+++ b/html/projects/mm.html
@@ -0,0 +1,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>
+