From c9e9c691c353d5d4835551de8d7d1f4c0ec74b9f Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Wed, 24 May 2017 11:14:51 -0400 Subject: Remove mmm and ML4PG contribs and remove references to them in code and docs --- coq/ML4PG/doc/src/images/algorithm1.png | Bin 249326 -> 0 bytes coq/ML4PG/doc/src/images/algorithm2.png | Bin 253897 -> 0 bytes coq/ML4PG/doc/src/images/clusters1.png | Bin 117359 -> 0 bytes coq/ML4PG/doc/src/images/clusters1pg.png | Bin 138300 -> 0 bytes coq/ML4PG/doc/src/images/clusters2.png | Bin 93270 -> 0 bytes coq/ML4PG/doc/src/images/clusters2pg.png | Bin 69517 -> 0 bytes coq/ML4PG/doc/src/images/export.png | Bin 65552 -> 0 bytes coq/ML4PG/doc/src/images/fig1.png | Bin 32650 -> 0 bytes coq/ML4PG/doc/src/images/fig1pg.png | Bin 102528 -> 0 bytes coq/ML4PG/doc/src/images/fig2.png | Bin 83087 -> 0 bytes coq/ML4PG/doc/src/images/fig3.png | Bin 89061 -> 0 bytes coq/ML4PG/doc/src/images/fig4.png | Bin 129581 -> 0 bytes coq/ML4PG/doc/src/images/fig5.png | Bin 106362 -> 0 bytes coq/ML4PG/doc/src/images/frequencies.png | Bin 125515 -> 0 bytes coq/ML4PG/doc/src/images/granularity.png | Bin 122487 -> 0 bytes coq/ML4PG/doc/src/images/levels.png | Bin 261362 -> 0 bytes coq/ML4PG/doc/src/images/ml_system1.png | Bin 249326 -> 0 bytes coq/ML4PG/doc/src/images/ml_system2.png | Bin 179177 -> 0 bytes coq/coq-abbrev.el | 5 +-- coq/coq-mmm.el | 51 ------------------------------- coq/coq.el | 7 ----- 21 files changed, 1 insertion(+), 62 deletions(-) delete mode 100644 coq/ML4PG/doc/src/images/algorithm1.png delete mode 100644 coq/ML4PG/doc/src/images/algorithm2.png delete mode 100644 coq/ML4PG/doc/src/images/clusters1.png delete mode 100644 coq/ML4PG/doc/src/images/clusters1pg.png delete mode 100644 coq/ML4PG/doc/src/images/clusters2.png delete mode 100644 coq/ML4PG/doc/src/images/clusters2pg.png delete mode 100644 coq/ML4PG/doc/src/images/export.png delete mode 100644 coq/ML4PG/doc/src/images/fig1.png delete mode 100644 coq/ML4PG/doc/src/images/fig1pg.png delete mode 100644 coq/ML4PG/doc/src/images/fig2.png delete mode 100644 coq/ML4PG/doc/src/images/fig3.png delete mode 100644 coq/ML4PG/doc/src/images/fig4.png delete mode 100644 coq/ML4PG/doc/src/images/fig5.png delete mode 100644 coq/ML4PG/doc/src/images/frequencies.png delete mode 100644 coq/ML4PG/doc/src/images/granularity.png delete mode 100644 coq/ML4PG/doc/src/images/levels.png delete mode 100644 coq/ML4PG/doc/src/images/ml_system1.png delete mode 100644 coq/ML4PG/doc/src/images/ml_system2.png delete mode 100644 coq/coq-mmm.el (limited to 'coq') diff --git a/coq/ML4PG/doc/src/images/algorithm1.png b/coq/ML4PG/doc/src/images/algorithm1.png deleted file mode 100644 index 8c8f47b5..00000000 Binary files a/coq/ML4PG/doc/src/images/algorithm1.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/algorithm2.png b/coq/ML4PG/doc/src/images/algorithm2.png deleted file mode 100644 index 6b5e0835..00000000 Binary files a/coq/ML4PG/doc/src/images/algorithm2.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/clusters1.png b/coq/ML4PG/doc/src/images/clusters1.png deleted file mode 100644 index ca4ef219..00000000 Binary files a/coq/ML4PG/doc/src/images/clusters1.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/clusters1pg.png b/coq/ML4PG/doc/src/images/clusters1pg.png deleted file mode 100644 index b39d409f..00000000 Binary files a/coq/ML4PG/doc/src/images/clusters1pg.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/clusters2.png b/coq/ML4PG/doc/src/images/clusters2.png deleted file mode 100644 index f091abbe..00000000 Binary files a/coq/ML4PG/doc/src/images/clusters2.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/clusters2pg.png b/coq/ML4PG/doc/src/images/clusters2pg.png deleted file mode 100644 index 6ba6dcb4..00000000 Binary files a/coq/ML4PG/doc/src/images/clusters2pg.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/export.png b/coq/ML4PG/doc/src/images/export.png deleted file mode 100644 index de048b47..00000000 Binary files a/coq/ML4PG/doc/src/images/export.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/fig1.png b/coq/ML4PG/doc/src/images/fig1.png deleted file mode 100644 index 955fd048..00000000 Binary files a/coq/ML4PG/doc/src/images/fig1.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/fig1pg.png b/coq/ML4PG/doc/src/images/fig1pg.png deleted file mode 100644 index d4a0df9f..00000000 Binary files a/coq/ML4PG/doc/src/images/fig1pg.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/fig2.png b/coq/ML4PG/doc/src/images/fig2.png deleted file mode 100644 index ed8c399e..00000000 Binary files a/coq/ML4PG/doc/src/images/fig2.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/fig3.png b/coq/ML4PG/doc/src/images/fig3.png deleted file mode 100644 index f3741a0e..00000000 Binary files a/coq/ML4PG/doc/src/images/fig3.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/fig4.png b/coq/ML4PG/doc/src/images/fig4.png deleted file mode 100644 index 9df097bd..00000000 Binary files a/coq/ML4PG/doc/src/images/fig4.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/fig5.png b/coq/ML4PG/doc/src/images/fig5.png deleted file mode 100644 index 733a3d22..00000000 Binary files a/coq/ML4PG/doc/src/images/fig5.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/frequencies.png b/coq/ML4PG/doc/src/images/frequencies.png deleted file mode 100644 index 4f90b5fc..00000000 Binary files a/coq/ML4PG/doc/src/images/frequencies.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/granularity.png b/coq/ML4PG/doc/src/images/granularity.png deleted file mode 100644 index 385b3972..00000000 Binary files a/coq/ML4PG/doc/src/images/granularity.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/levels.png b/coq/ML4PG/doc/src/images/levels.png deleted file mode 100644 index 48e02db7..00000000 Binary files a/coq/ML4PG/doc/src/images/levels.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/ml_system1.png b/coq/ML4PG/doc/src/images/ml_system1.png deleted file mode 100644 index f11cebf1..00000000 Binary files a/coq/ML4PG/doc/src/images/ml_system1.png and /dev/null differ diff --git a/coq/ML4PG/doc/src/images/ml_system2.png b/coq/ML4PG/doc/src/images/ml_system2.png deleted file mode 100644 index 792c423d..00000000 Binary files a/coq/ML4PG/doc/src/images/ml_system2.png and /dev/null differ diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 79231ad9..3a750472 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -299,10 +299,7 @@ It was constructed with `proof-defstringset-fn'.") ["Unset Printing Unfocused" coq-unset-printing-unfocused t] ["Set Printing Wildcards" coq-set-printing-wildcards t] ["Unset Printing Wildcards" coq-unset-printing-wildcards t] - ["Set Printing Width" coq-ask-adapt-printing-width-and-show t]) - "" - ["ML4PG" (coq-activate-ml4pg) :help "Activates ML4PG: machine-learning methods for Proof General"] - )) + ["Set Printing Width" coq-ask-adapt-printing-width-and-show t]))) (setq-default coq-menu-entries (append coq-menu-common-entries diff --git a/coq/coq-mmm.el b/coq/coq-mmm.el deleted file mode 100644 index e8ff56eb..00000000 --- a/coq/coq-mmm.el +++ /dev/null @@ -1,51 +0,0 @@ -;; coq-mmm.el Configure MMM mode for CoqDoc elements -;; -;; Copyright (C) 2007 David Aspinall -;; Authors: David Aspinall -;; Licence: GPL -;; -;; $Id$ -;; -;; We only spot some simple cases of embedded LaTeX/HTML/verbatim. -;; -;; At the moment, the insertion has a bad interaction with the holes -;; code which also uses skeletons: the interesting positions used -;; for MMM markup are made into holes! - -(require 'mmm-auto) - -(mmm-add-group - 'coq - `((coq-text - :submode text-mode - :face mmm-comment-submode-face - :front "(\\*\\*[ \t]" - :back "[ ]?\\*)" - :insert ((?d coqdoc-text nil @ "(** " @ " " _ " " @ " *)" @))) - - (coq-latex - :submode LaTeX-mode - :face mmm-comment-submode-face - :front "(\\*\\*[^%\\$]*[%\\$]" - :back "[%\\$][ \t]*\\*)" - :insert ((?l coqdoc-latex nil @ "(** %" @ " " _ " " @ "% *)" @))) - - (coq-html - :submode html-mode - :face mmm-comment-submode-face - :front "(\\*\\*[^#]*#" - :back "#[ \t]*\\*)" - :insert ((?w coqdoc-html nil @ "(** #" @ " " _ " " @ "# *)" @))) - - (coq-verbatim - :submode text-mode - :face mmm-code-submode-face - :front "^[ \t]*<<" - :back ">>" - :insert ((?v coqdoc-verbatim nil @ "<<\n" @ " " _ " " @ "\n>>" @))) - )) - - -(provide 'coq-mmm) - -;;; coq-mmm.el ends here diff --git a/coq/coq.el b/coq/coq.el index 78c48170..d8a52983 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2844,13 +2844,6 @@ are non-nil at the same time, this gives priority to the former." (define-key coq-mode-map (kbd ".") 'coq-terminator-insert) ;(define-key coq-mode-map (kbd ";") 'coq-terminator-insert) ; for french keyboards -;; Activation of ML4PG functionality -(declare-function ml4pg-select-mode "ml4pg") ;; Avoids copilation warnings - -(defun coq-activate-ml4pg () - (let ((filename (concatenate 'string proof-home-directory "contrib/ML4PG/ml4pg.el"))) - (when (file-exists-p filename) (load-file filename) (ml4pg-select-mode)))) - ;;;;;;;;;;;;;; ;; This was done in coq-compile-common, but it is actually a good idea even -- cgit v1.2.3