Remove mmm and ML4PG contribs and remove references to them in code and docs

3 files changed, 0 insertions, 83 deletions

diff --git a/etc/coq/coqdoc-egs.v b/etc/coq/coqdoc-egs.v
deleted file mode 100644
index d79d44e5..00000000
--- a/etc/coq/coqdoc-egs.v
+++ /dev/null
@@ -1,26 +0,0 @@
-(* Some tests/examples of coqdoc regions in Coq files, 
-   used with MMM configuration (ProofGeneral -> Options -> Multiple Modes. *)
-
-
-(** This is a coqdoc plain text region.
-
-    After editing/changing regions in mmm mode, use C-x % C-b to reparse
-*)
-
-
-(** %This is a special case of a \LaTeX{} region recognised by MMM.
-\begin{quote}
-Emacs will be in \texttt{LaTeX} mode when editing this region.
-\end{quote}
- % *)
-
-
-(** #Similarly, this is an HTML region, edited in HTML mode # *)
-
-
-(* Finally, here is some *)
-<<
-verbatim text
->>
-(* in text mode *)
-
diff --git a/etc/isar/MMMtests.thy b/etc/isar/MMMtests.thy
deleted file mode 100644
index 994a8ee0..00000000
--- a/etc/isar/MMMtests.thy
+++ /dev/null
@@ -1,40 +0,0 @@
-(* Testing samples for MMM *)
-
-header {* This is edited in LaTeX mode *}
-
-theory MMMtests imports Main begin
-
-text {*
-  This is a test of MMM support.
-  This region is edited in \LaTeX{} mode.
-*}
-
-subsection {* and this one. *}
-
-
-ML {*
-  (* Whereas this region is edited in SML mode.  For that to work, you
-  need to have installed SML mode in your Emacs, otherwise MMM mode
-  won't bother.  See Stefan Monnier's page at
-  http://www.iro.umontreal.ca/~monnier/elisp/. *)
-  
-  fun foo [] = 0
-    | foo (x::xs) = x * foo xs
-*}
-
-ML_val {* (* and this one *) *}
-
-ML_command {* (* and this one *) *}
-
-print_translation {* [] (* and even this one *) *}
-
-text {* 
-  You can enter the text for a MMM region conveniently 
-  using the dedicated insertion commands. For example, I inserted
-  this region by typing \texttt{C-c \% t}  --- see the MMM menu or
-  \texttt{C-c \% h}  for a list of commands.  
-
-  Notice that font locking for different modes tends to interact
-  badly with mode switches between lines.  Best stick to
-  separate lines as in these examples.
-*}
diff --git a/etc/mmm-install b/etc/mmm-install
deleted file mode 100644
index 41042d23..00000000
--- a/etc/mmm-install
+++ /dev/null
@@ -1,17 +0,0 @@
-#!/bin/sh
-#
-# Install from mmm-mode into PG by copying relevant files
-# Run from inside mmm-mode distrib
-#
-# $Id$
-#
-NOTICES="AUTHORS COPYING FAQ INSTALL NEWS README TODO"
-DOCS="mmm.texinfo version.texi"
-ELISP=*.el
-MMMDIR=~/PG/mmm
-
-rm -f $MMMDIR/*
-cp -p $NOTICES $DOCS $ELISP $MMMDIR
-
-
-