[nongnu] elpa/proof-general 73571a5 03/13: Remove CCC support

[ELPA Syncer]

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

    Remove CCC support
---
 Makefile              |  2 +-
 README.md             |  4 +--
 ccc/README            | 14 ---------
 ccc/ccc.el            | 85 ---------------------------------------------------
 doc/ProofGeneral.texi |  3 +-
 generic/proof-site.el |  1 -
 6 files changed, 4 insertions(+), 105 deletions(-)

diff --git a/Makefile b/Makefile
index bda39cc..9a6edc0 100644
--- a/Makefile
+++ b/Makefile
@@ -35,7 +35,7 @@ PREFIX=$(DESTDIR)/usr
 DEST_PREFIX=$(DESTDIR)/usr
 
 # subdirectories for provers: to be compiled and installed
-PROVERS=acl2 ccc coq easycrypt hol-light isar lego pghaskell pgocaml pgshell 
phox
+PROVERS=acl2 coq easycrypt hol-light isar lego pghaskell pgocaml pgshell phox
 
 # generic lisp code: to be compiled and installed
 OTHER_ELISP=generic lib
diff --git a/README.md b/README.md
index 3ed9d29..230caee 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/) and
   [LEGO](http://www.dcs.ed.ac.uk/home/lego)
-* Experimental support of: CCC, ACL2, Hol-Light, Lambda-Clam, Shell
+* Experimental support of: ACL2, Hol-Light, Lambda-Clam, Shell
 * Obsolete instances: Demoisa, Lambda-Clam, Plastic
-* Removed instances: Twelf, HOL98
+* Removed instances: Twelf, CCC, HOL98
 
 A few example proofs are included in each prover subdirectory.
 
diff --git a/ccc/README b/ccc/README
deleted file mode 100644
index 88faf17..0000000
--- a/ccc/README
+++ /dev/null
@@ -1,14 +0,0 @@
-Proof General for the Casl Consistency Checker
-
-Author:        Christoph L�th <cxl@informatik.uni-bremen.de>
-       
-=================================================================
-
-This is a fairly straightforward instantiation of Proof General for
-the Casl Consistency Checker, CCC. 
-
-CASL is the standard algebraic specification language, and CCC is a
-tool to check consistency of CASL specifications.
-
-For more information, hasten thee browser yonder:
-  http://www.informatik.uni-bremen.de/cofi/ccc
diff --git a/ccc/ccc.el b/ccc/ccc.el
deleted file mode 100644
index 44a0d7c..0000000
--- a/ccc/ccc.el
+++ /dev/null
@@ -1,85 +0,0 @@
-;; ccc.el - Proof General for the Casl Consistency Checker
-;;
-;; Author: Christoph L�th <cxl@informatik.uni-bremen.de>
-;;
-;; This is a fairly straightforward instantiation of Proof General for
-;; the Casl Consistency Checker, CCC.
-;;
-;; CASL is the standard algebraic specification language, and CCC is a
-;; tool to check consistency of CASL specifications.
-;;
-;; For more information, hasten thee browser yonder:
-;;   http://www.informatik.uni-bremen.de/cofi/ccc
-
-(require 'proof-easy-config)            ; nice and easy does it
-(require 'proof-syntax)                        ; functions for making regexps
-
-(defvar ccc-keywords nil)
-(defvar ccc-tactics nil)
-(defvar ccc-tacticals nil)
-
-(proof-easy-config  'ccc "CASL Consistency Checker"
- proof-prog-name                "ccc" ;; must be in your path.
- proof-terminal-string             ";"
- proof-script-comment-start      "(*"
- proof-script-comment-end        "*)"
- proof-goal-command-regexp       "\\(ccc\\|holcasl\\) \".*\";"
- proof-save-command-regexp       "^qeccc"
- proof-goal-with-hole-regexp     "\\(ccc\\|holcasl\\) \"\\(\\(.*\\)\\)\""
- proof-save-with-hole-regexp     "qeccc \"\\(\\(.*\\)\\)\""
- proof-non-undoables-regexp      "undo\\|back"
- proof-goal-command              "ccc \"%s\";"
- proof-save-command              "qeccc \"%s\";"
- proof-kill-goal-command         "abort ();"
- proof-showproof-command         "prt()"
- proof-undo-n-times-cmd          "undo_steps %s;"
- proof-auto-multiple-files       nil
- proof-shell-cd-cmd              "cd \"%s\""
- proof-shell-interrupt-regexp    "Interrupt"
- proof-shell-start-goals-regexp  "^No subgoals\\|^[0-9]* subgoals\\|^Wts:"
- proof-shell-end-goals-regexp    "val it"
- proof-shell-quit-cmd            "quit();"
- proof-assistant-home-page       
"http://www.informatik.uni-bremen.de/cofi/tools/ccc";
- proof-shell-annotated-prompt-regexp  "^\\(val it = () : 
unit\n\\)?\\(CCC\\|^HOL-CASL\\)> " ;; "^\\(val it = () : unit\n\\)?ML>? "
- proof-shell-error-regexp        "\\*\\*\\*\\|^.*Error:\\|^uncaught exception 
\\|^Exception- "
- proof-shell-proof-completed-regexp "^Consistency proof successfully finished."
- proof-shell-eager-annotation-start "^\\[opening \\|^###\\|^Reading" ;;; ???
-
- ;;
- ;; Some basic fontlocking and syntax table entries, as taken from the
- ;; hol98 instance (it's all SML anyway :-)
- ;;
- proof-script-syntax-table-entries
- '(?\` "\""
-   ?\$ "."
-   ?\/ "."
-   ?\\ "."
-   ?+  "."
-   ?-  "."
-   ?=  "."
-   ?%  "."
-   ?<  "."
-   ?>  "."
-   ?\& "."
-   ?.  "w"
-   ?_  "w"
-   ?\' "w"
-   ?\| "."
-   ?\[ "(]"
-   ?\] ")["
-   ?\* ". 23"
-   ?\( "()1"
-   ?\) ")(4")
-
- ccc-keywords  '("use" "ap" "holcasl" "ccc" "load_lib" "qeccc")
- ccc-tactics   '("compose" "compose'" "prove" "prove_free_type")
- ccc-tacticals '("Repeat" "Orelse" "Then" "ThenList" "OrelseList")
- proof-script-font-lock-keywords
- (list
-  (cons (proof-ids-to-regexp ccc-keywords) 'font-lock-keyword-face)
-  (cons (proof-ids-to-regexp ccc-tactics) 'font-lock-keyword-face)
-  ; (cons (proof-ids-to-regexp hol98-rules) 'font-lock-keyword-face)
-  (cons (proof-ids-to-regexp ccc-tacticals) 'proof-tacticals-name-face))
-
-
-)
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 17dab48..143ad20 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -209,7 +209,7 @@ other documentation, system downloads, etc.
 @cindex news
 
 The old code for the support of the following systems have been
-removed: Twelf, Hol98.
+removed: Twelf, CCC, HOL98.
 
 @node News for Version 4.4
 @unnumberedsec News for Version 4.4
@@ -524,7 +524,6 @@ script file for your proof assistant, for example:
 @item       ACL2          @tab @file{.acl2}   @tab @code{acl2-mode}
 @item       Plastic       @tab @file{.lf}     @tab @code{plastic-mode}
 @item       Lambda-CLAM   @tab @file{.lcm}    @tab @code{lclam-mode}
-@item       CCC           @tab @file{.ccc}    @tab @code{ccc-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 6e295ee..a66f41f 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -52,7 +52,6 @@
       ;; Obscure instances or conflict with other Emacs modes.
 
       ;; (lego "LEGO" "l")
-      ;; (ccc    "CASL Consistency Checker" "ccc")
 
       ;; (hol-light "HOL Light" "ml") ; [for testing]