diff options
author | 2004-05-07 00:09:01 +0000 | |
---|---|---|
committer | 2004-05-07 00:09:01 +0000 | |
commit | f295d390fb43cad5caecd38786ca0bb18fb01836 (patch) | |
tree | 0a89c2cbfaff5574876f3ac945638f512a6dac6e /coq | |
parent | dd662549c9f16f16b0ea7f4a93440556863a60c7 (diff) |
Updated.
Diffstat (limited to 'coq')
-rw-r--r-- | coq/TODO-TMP | 61 |
1 files changed, 61 insertions, 0 deletions
diff --git a/coq/TODO-TMP b/coq/TODO-TMP index 25a227b2..15fb4aa7 100644 --- a/coq/TODO-TMP +++ b/coq/TODO-TMP @@ -19,3 +19,64 @@ a -- TAB here loops forever +================================================================= + + +;; coq-mmm.el Configure MMM mode for Coq (for LaTeX/coqdoc) +;; +;; Copyright (C) 2004 David Aspinall +;; Authors: David Aspinall <David.Aspinall@ed.ac.uk> +;; Licence: GPL +;; +;; $Id$ +;; +;; Presently, we deal with several cases of (** text *). +;; +;; TODO: +;; -- complete this +;; + +(require 'mmm-auto) + +(defconst coq-start-latex-regexp + (concat + "\\(" + (proof-ids-to-regexp + ;; Perhaps section is too much? The fontification is nice but + ;; section headers are a bit short to use LaTeX mode in. + (list "text" "header" ".*section")) + ;; Next one is nice but hammers font lock a bit too much + ;; if there are lots of -- {* short comments *} + ;; "\\|\-\-" ;; NB: doesn't work with \\<--\\> + "\\)[ \t]+{\\*")) + +(defconst coq-start-sml-regexp + (concat + "\\(" + (proof-ids-to-regexp (list "ML" "ML_command" "ML_setup" + "typed_print_translation")) + "\\)[ \t]+{\\*")) + + +(mmm-add-group + 'coq + `((coq-latex + :submode LaTeX-mode + :face mmm-comment-submode-face + :front ,coq-start-latex-regexp + :back "\\*}" + :insert ((?t coqtext nil @ "text {*" @ " " _ " " @ "*}" @)) + :save-matches 1) + + (coq-sml + :submode sml-mode + :face mmm-code-submode-face + :front ,coq-start-sml-regexp + :back "\\*}" + :insert ((?M coqml nil @ "ML_setup {*" @ " " _ " " @ "*}" @)) + :save-matches 1))) + + +(provide 'coq-mmm) + +;;; coq-mmm.el ends here |