[nongnu] elpa/proof-general e27b1ef 08/13: Remove Lambda-Clam support

[ELPA Syncer]

branch: elpa/proof-general
commit e27b1efa04412e277ac7a155752c3333d7d9d57b
Author: Stefan Monnier <monnier@iro.umontreal.ca>
Commit: Stefan Monnier <monnier@iro.umontreal.ca>

    Remove Lambda-Clam support
---
 Makefile                   |   2 +-
 README.md                  |   6 +-
 doc/ProofGeneral.texi      |   3 +-
 generic/proof-site.el      |   1 -
 obsolete/lclam/README      |  15 ----
 obsolete/lclam/example.lcm |  34 --------
 obsolete/lclam/lclam.el    | 209 ---------------------------------------------
 7 files changed, 5 insertions(+), 265 deletions(-)

diff --git a/Makefile b/Makefile
index 2669510..039884e 100644
--- a/Makefile
+++ b/Makefile
@@ -58,7 +58,7 @@ ELISP_EXTRAS=
 EXTRA_DIRS = images
 
 DOC_FILES=AUTHORS BUGS COMPATIBILITY CHANGES COPYING INSTALL README REGISTER 
doc/*.pdf
-DOC_EXAMPLES=isar/*.thy lclam/*.lcm pgshell/*.pgsh phox/*.phx
+DOC_EXAMPLES=isar/*.thy pgshell/*.pgsh phox/*.phx
 DOC_SUBDIRS=${DOC_EXAMPLES} */README* */CHANGES */BUGS 
 
 BATCHEMACS=${EMACS} --batch --no-site-file -q 
diff --git a/README.md b/README.md
index c4950ae..c26f752 100644
--- a/README.md
+++ b/README.md
@@ -140,9 +140,9 @@ instances are no longer maintained nor available in the 
MELPA package:
 * Legacy support of
   [Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/)
   
-* Experimental support of: Lambda-Clam, Shell
-* Obsolete instances: Demoisa, Lambda-Clam
-* Removed instances: Twelf, CCC, Hol-Light, ACL2, Plastic, HOL98,
+* Experimental support of: Shell
+* Obsolete instances: Demoisa
+* Removed instances: Twelf, CCC, Hol-Light, ACL2, Plastic, Lambda-Clam, HOL98,
   [LEGO](http://www.dcs.ed.ac.uk/home/lego)
 
 A few example proofs are included in each prover subdirectory.
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 7411fe7..e7dfa44 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -207,7 +207,7 @@ other documentation, system downloads, etc.
 @cindex news
 
 The old code for the support of the following systems have been
-removed: Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, HOL98.
+removed: Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, Lambda-Clam, HOL98.
 
 @node News for Version 4.4
 @unnumberedsec News for Version 4.4
@@ -516,7 +516,6 @@ script file for your proof assistant, for example:
 @item       Coq           @tab @file{.v}      @tab @code{coq-mode}
 @item       Isabelle      @tab @file{.thy}    @tab @code{isar-mode}
 @item       Phox          @tab @file{.phx}    @tab @code{phox-mode}
-@item       Lambda-CLAM   @tab @file{.lcm}    @tab @code{lclam-mode}
 @item       PG-Shell      @tab @file{.pgsh}   @tab @code{pgshell-mode}
 @item       EasyCrypt     @tab @file{.ec}     @tab @code{easycrypt-mode}
 @end multitable
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 3141310..4a111b7 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -57,7 +57,6 @@
 
       ;; Incomplete/obsolete:
 
-      ;; (lclam "Lambda-CLAM" "lcm")     ; obsolete
       ;; (demoisa "Isabelle Demo" "ML")  ; obsolete
       )
     "Default value for `proof-assistant-table', which see.")
diff --git a/obsolete/lclam/README b/obsolete/lclam/README
deleted file mode 100644
index 39db25c..0000000
--- a/obsolete/lclam/README
+++ /dev/null
@@ -1,15 +0,0 @@
-Lambda-CLAM Proof General
-
-Written by James Brotherston <jjb@dai.ed.ac.uk>.
-
-
-Status:                        supported
-Maintainer:            James Brotherston <jjb@dai.ed.ac.uk>
-Lambda-CLAM version:    ??
-Lambda-CLAM homepage:   http://dream.dai.ed.ac.uk/software/systems/lambda-clam/
-
-========================================
-
-$Id$
-
-
diff --git a/obsolete/lclam/example.lcm b/obsolete/lclam/example.lcm
deleted file mode 100644
index 5b27581..0000000
--- a/obsolete/lclam/example.lcm
+++ /dev/null
@@ -1,34 +0,0 @@
-/* File name:      example.lcm                            */
-/* Description:    Tutorial walkthrough from LClam manual */
-/* Author:         James Brotherston                      */
-/* Last modified:  20th August 2001                       */
-
-query_top_goal X assp.
-
-set_spypoint (induction_top normal_ind).
-set_spypoint sym_eval.
-
-silent_output on.
-
-pds_plan (induction_top normal_ind) assp.
-continue.
-continue.
-continue.
-
-add_theory_to_induction_scheme_list arithmetic.
-add_theory_to_sym_eval_list arithmetic.
-set_wave_rule_to_sym_eval.
-add_to_sym_eval_list [idty].
-set_wave_rule_to_sym_eval.
-remove_spypoint (induction_top normal_ind).
-remove_spypoint sym_eval.
-pds_plan (induction_top normal_ind) assp.
-
-step_by_step on.
-pds_plan (induction_top normal_ind) assp.
-continue.
-backtrack.
-try ind_strat.
-continue.
-plan_node (2::1::nil).
-abandon.
diff --git a/obsolete/lclam/lclam.el b/obsolete/lclam/lclam.el
deleted file mode 100644
index 0472b6a..0000000
--- a/obsolete/lclam/lclam.el
+++ /dev/null
@@ -1,209 +0,0 @@
-;; File name:      lclam.el        
-;; Description:    Proof General instance for Lambda-CLAM
-;; Author:         James Brotherston <jjb@dai.ed.ac.uk>
-;; Last modified:  23 October 2001
-;;
-;; $Id$
-
-(require 'proof)            ; load generic parts
-(require 'proof-syntax)     
-
-;;
-;; =========== User settings for Lambda-CLAM ============
-;;
-
-(defcustom lclam-prog-name ; "~/lambda-clam-teyjus/bin/lclam"
-                          "lclam"
-  "*Name of program to run Lambda-CLAM"
-  :type 'file
-  :group 'lclam)
-
-(defcustom lclam-web-page
-  "http://dream.dai.ed.ac.uk/software/systems/lambda-clam/";
-  "URL of web page for Lambda-CLAM"
-  :type 'string
-  :group 'lclam-config)
-
-
-;;
-;; =========== Configuration of generic modes ============
-;;
-
-(defun lclam-config ()
-  "Configure Proof General scripting for Lambda-CLAM."
-  (setq 
-   proof-terminal-string           "."
-   proof-script-comment-start      "/*"
-   proof-script-comment-end        "*/"
-   proof-goal-command-regexp       "^pds_plan"
-   proof-save-command-regexp       nil
-   proof-goal-with-hole-regexp     nil
-   proof-save-with-hole-regexp     nil
-   proof-non-undoables-regexp      nil
-   proof-undo-n-times-cmd          nil
-   proof-showproof-command         nil 
-   proof-goal-command              "^pds_plan %s."
-   proof-save-command              nil
-   proof-kill-goal-command         nil
-   proof-assistant-home-page       lclam-web-page
-   proof-auto-multiple-files       nil 
-   ))
-
-(defun lclam-shell-config ()
-  "Configure Proof General shell for Lambda-CLAM"
-  (setq
-   proof-shell-annotated-prompt-regexp "^lclam:" 
-   proof-shell-cd-cmd                  nil
-   proof-shell-interrupt-regexp        nil
-   proof-shell-error-regexp            nil
-   proof-shell-start-goals-regexp      nil
-   proof-shell-end-goals-regexp        nil
-   proof-shell-proof-completed-regexp  "^Plan Succeeded"
-   proof-shell-init-cmd                nil
-   proof-shell-quit-cmd                "halt."
-   proof-shell-eager-annotation-start  nil
-    ))
-
-;;
-;; =========== Defining the derived modes ================
-;;
-
-(define-derived-mode lclam-proofscript-mode proof-mode
-  "Lambda-CLAM script" nil
-  (lclam-config)
-  (proof-config-done))
-
-(define-derived-mode lclam-shell-mode proof-shell-mode
-  "Lambda-CLAM shell" nil
-  (lclam-shell-config)
-  (proof-shell-config-done))
-
-(define-derived-mode lclam-response-mode proof-response-mode
-  "Lambda-CLAM response" nil
-  (proof-response-config-done))
-
-(define-derived-mode lclam-goals-mode proof-goals-mode
-  "Lambda-CLAM goals" nil
-  (proof-goals-config-done))
-
-;; Automatic selection of theory file or proof script mode
-;; .lcm -> proof script mode
-;; .def -> theory file mode
-
-(defun lclam-mode ()
-(interactive)
-(cond
-    ((proof-string-match "\\.def$" (buffer-file-name))
-    (thy-mode))
-    (t
-    (lclam-proofscript-mode)))
-)
-
-;; Hook which configures settings to get the proof shell running 
-
-(add-hook 'proof-pre-shell-start-hook 'lclam-pre-shell-start)
-
-(defun lclam-pre-shell-start ()
-  (setq proof-prog-name         lclam-prog-name)
-  (setq proof-mode-for-shell    'lclam-shell-mode)
-  (setq proof-mode-for-response 'lclam-response-mode)
-  (setq proof-mode-for-goals    'lclam-goals-mode)
-  (setq proof-shell-process-connection-type t))
-
-
-;;
-;; ============ Extra bits and pieces - JB ============
-;;
-
-;; Open .def files in theory mode from now on
-
-(setq auto-mode-alist
-      (cons '("\\.def$" . thy-mode) auto-mode-alist))
-
-;; Remove redundant toolbar buttons
-
-(eval-after-load "pg-custom"
-'(progn
-  (setq lclam-toolbar-entries
-       (remassoc 'state lclam-toolbar-entries))
-  (setq lclam-toolbar-entries
-       (remassoc 'context lclam-toolbar-entries))
-  (setq lclam-toolbar-entries
-       (remassoc 'undo lclam-toolbar-entries))
-  (setq lclam-toolbar-entries
-       (remassoc 'retract lclam-toolbar-entries))
-  (setq lclam-toolbar-entries
-       (remassoc 'qed lclam-toolbar-entries))))
-
-;;
-;; ============ Theory file mode ==============
-;;
-
-(define-derived-mode thy-mode fundamental-mode "Lambda-CLAM theory file mode"
-  (thy-add-menus))
-
-(defvar thy-mode-map nil)
-
-(defun thy-add-menus ()
-  "Add Lambda-CLAM menu to current menu bar."  
-  (require 'proof-script)    
-  (require 'proof-x-symbol)
-  (easy-menu-define thy-mode-pg-menu
-                    thy-mode-map
-                    "PG Menu for Lambda-CLAM Proof General"
-                    (cons proof-general-name
-                          (append
-                           (list
-                           ;; A couple from the toolbar that make sense here
-                           ;; (also in proof-universal-keys)
-                            ["Issue command" proof-minibuffer-cmd t]
-                            ["Interrupt prover" proof-interrupt-process t])
-                          (list proof-buffer-menu)
-                           (list proof-help-menu))))
-
-  (easy-menu-define thy-mode-lclam-menu
-                    thy-mode-map
-                    "Menu for Lambda-CLAM Proof General, theory file mode."
-                    (cons "Theory"
-                          (list
-                           ["Next section" thy-goto-next-section t]
-                           ["Prev section" thy-goto-prev-section t]
-                           ["Insert template" thy-insert-template t]
-; da: commented out this, function is incomplete
-;                           ["Include definitions" match-and-assert-defs
-;                            :active (proof-locked-region-empty-p)]
-                           ["Process theory" process-thy-file
-                            :active (proof-locked-region-empty-p)]
-; da: commented out this, there's no retract function provided
-;                           ["Retract theory" isa-retract-thy-file
-;                            :active (proof-locked-region-full-p)]
-                           ["Next error" proof-next-error t]
-                           ["Switch to script" thy-find-other-file t])))
-
-  (easy-menu-add thy-mode-pg-menu thy-mode-map)
-  (easy-menu-add thy-mode-lclam-menu thy-mode-map)
-)
-
-(defun process-thy-file (file)
-  "Process the theory file FILE.  If interactive, use buffer-file-name."
-  (interactive (list buffer-file-name))
-  (save-some-buffers)
-  (update-thy-only file nil nil))
-
-(defun update-thy-only (file try wait)
-  "Process the theory file FILE."
-  ;; First make sure we're in the right directory to take care of
-  ;; relative "files" paths inside theory file.
-  (proof-cd-sync)
-  (proof-shell-invisible-command
-   (proof-format-filename
-    ;; %r parameter means relative (don't expand) path
-    (format "use_thy \"%s%%r\"." (if try "try_" ""))
-    (file-name-nondirectory file))
-   wait))
-
-;(defun match-and-assert-defs
-;  "Interactively process and assert definitions in theory file"
-;)
-
-(provide 'lclam)