[nongnu] elpa/proof-general 0a295cd 07/13: Remove Plastic support

[ELPA Syncer]

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

    Remove Plastic support
---
 Makefile                           |   2 +-
 README.md                          |   4 +-
 doc/PG-adapting.texi               |   2 +-
 doc/ProofGeneral.texi              |   3 +-
 generic/proof-config.el            |   2 +-
 generic/proof-site.el              |   1 -
 obsolete/plastic/README            |  12 -
 obsolete/plastic/plastic-syntax.el | 119 -------
 obsolete/plastic/plastic.el        | 665 -------------------------------------
 obsolete/plastic/test.lf           |  64 ----
 proof-general.el                   |   2 +-
 11 files changed, 7 insertions(+), 869 deletions(-)

diff --git a/Makefile b/Makefile
index 66a77d9..2669510 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 plastic/*.lf
+DOC_EXAMPLES=isar/*.thy lclam/*.lcm 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 66f2d17..c4950ae 100644
--- a/README.md
+++ b/README.md
@@ -141,8 +141,8 @@ instances are no longer maintained nor available in the 
MELPA package:
   [Isabelle](https://www.cl.cam.ac.uk/research/hvg/Isabelle/)
   
 * Experimental support of: Lambda-Clam, Shell
-* Obsolete instances: Demoisa, Lambda-Clam, Plastic
-* Removed instances: Twelf, CCC, Hol-Light, ACL2, HOL98,
+* Obsolete instances: Demoisa, Lambda-Clam
+* Removed instances: Twelf, CCC, Hol-Light, ACL2, Plastic, HOL98,
   [LEGO](http://www.dcs.ed.ac.uk/home/lego)
 
 A few example proofs are included in each prover subdirectory.
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 3f1374e..d89c180 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -1636,7 +1636,7 @@ stripped of carriage returns before being sent.
 Example uses:
 Lego used this hook for setting the pretty printer width if
 the window width has changed;
-Plastic uses it to remove literate-style markup from @samp{string}.
+Plastic used it to remove literate-style markup from @samp{string}.
 
 See also @samp{@code{proof-script-preprocess}} which can munge text when
 it is added to the queue of commands.
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 869fa87..7411fe7 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, HOL98.
+removed: Twelf, CCC, Lego, Hol-Light, ACL2, Plastic, 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       Plastic       @tab @file{.lf}     @tab @code{plastic-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}
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 3106d4e..2f4be4a 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -1662,7 +1662,7 @@ stripped of carriage returns before being sent.
 Example uses:
 Lego used this hook for setting the pretty printer width if
 the window width has changed;
-Plastic uses it to remove literate-style markup from `string'.
+Plastic used it to remove literate-style markup from `string'.
 
 See also `proof-script-preprocess' which can munge text when
 it is added to the queue of commands."
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 7286628..3141310 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -57,7 +57,6 @@
 
       ;; Incomplete/obsolete:
 
-      ;; (plastic "Plastic" "lf")        ; obsolete
       ;; (lclam "Lambda-CLAM" "lcm")     ; obsolete
       ;; (demoisa "Isabelle Demo" "ML")  ; obsolete
       )
diff --git a/obsolete/plastic/README b/obsolete/plastic/README
deleted file mode 100644
index 881f5b5..0000000
--- a/obsolete/plastic/README
+++ /dev/null
@@ -1,12 +0,0 @@
-Plastic Proof General
-
-Written by Paul Callaghan
-
-Status:                  under development together with Plastic
-Maintainer:      Paul Callaghan
-Plastic homepage: http://www.dur.ac.uk/CARG/plastic.html
-
-========================================
-
-$Id$
-
diff --git a/obsolete/plastic/plastic-syntax.el 
b/obsolete/plastic/plastic-syntax.el
deleted file mode 100644
index c259a3b..0000000
--- a/obsolete/plastic/plastic-syntax.el
+++ /dev/null
@@ -1,119 +0,0 @@
-;; plastic-syntax.el - Syntax of Plastic
-;; Author: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
-;; Maintainer: <author>
-;; plastic-syntax.el,v 6.0 2001/09/03 12:11:56 da Exp
-
-;; adapted from the following, by Paul Callaghan
-;; ;; lego-syntax.el Syntax of LEGO
-;; ;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
-;; ;; Author: Thomas Kleymann and Dilip Sequeira
-;; ;; Maintainer: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
-;; ;; lego-syntax.el,v 2.10 1998/11/06 16:18:55 tms Exp
-
-
-(require 'proof-syntax)
-
-;; ----- keywords for font-lock.
-
-(defconst plastic-keywords-goal '("$?Goal"))
-
-(defconst plastic-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen"))
-
-(defconst plastic-commands
-  (append plastic-keywords-goal plastic-keywords-save
-         '("allE" "allI" "andE" "andI" "Assumption" "Claim" "Coercion"
-           "Cut" "Discharge" "DischargeKeep"
-           "echo" "exE" "exI" "Expand" "ExpAll"
-           "ExportState" "Equiv" "For" "Freeze" "Hnf" "Immed"
-           "impE" "impI" "Induction" "Inductive"
-           "Invert" "Init" "intros" "Intros" "Module" "Next"
-           "Normal" "notE" "notI" "orE" "orIL" "orIR" "qnify" "Qnify"
-           "Qrepl" "Record" "Refine" "Repeat" "Return" "ReturnAll"
-           "Try" "Unfreeze"))
-  "Subset of Plastic keywords and tacticals which are terminated by a \?;")
-
-(defconst plastic-keywords
-  (append plastic-commands
-         '("Constructors" "Double" "ElimOver" "Fields" "Import" "Inversion"
-           "NoReductions" "Parameters" "Relation" "Theorems")))
-
-(defconst plastic-tacticals '("Then" "Else" "Try" "Repeat" "For"))
-
-;; ----- regular expressions for font-lock
-(defconst plastic-error-regexp "^\\(FAIL\\)"
-  "A regular expression indicating that the Plastic process has identified an 
error.")
-
-(defvar plastic-id proof-id)
-
-(defvar plastic-ids (concat plastic-id "\\(\\s *,\\s *" plastic-id "\\)*")
-  "*For font-lock, we treat \",\" separated identifiers as one identifier
-  and refontify commata using \\{plastic-fixup-change}.")
-
-(defconst plastic-arg-list-regexp "\\s *\\(\\[[^]]+\\]\\s *\\)*"
-  "Regular expression maching a list of arguments.")
-
-(defun plastic-decl-defn-regexp (char)
-    (concat "\\[\\s *\\(" plastic-ids "\\)" plastic-arg-list-regexp char))
-; Examples
-;              ^        ^^^^        ^^^^^^^^^^^^^^^^^^^^^^^  ^^^^
-;              [        sort                                 =
-;              [        sort        [n:nat]                  =
-;              [        sort        [abbrev=...][n:nat]      =
-
-(defconst plastic-definiendum-alternative-regexp
-  (concat "\\(" plastic-id "\\)" plastic-arg-list-regexp "\\s * ==")
-  "Regular expression where the first match identifies the definiendum.")
-
-(defvar plastic-font-lock-terms
-  (list
-
-   ; lambda binders
-     (list (plastic-decl-defn-regexp "[:|?]") 1
-          'proof-declaration-name-face)
-
-     ; let binders
-     (list plastic-definiendum-alternative-regexp 1 
'font-lock-function-name-face)
-     (list (plastic-decl-defn-regexp "=") 1 'font-lock-function-name-face)
-
-     ; Pi and Sigma binders
-     (list (concat "[{<]\\s *\\(" plastic-ids "\\)") 1
-          'proof-declaration-name-face)
-
-     ;; Kinds
-     (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
-                  plastic-id ")\\)?") 'font-lock-type-face))
-  "*Font-lock table for Plastic terms.")
-
-;; Instead of "[^:]+", it may be better to use "plastic-id". Furthermore,
-;; it might be safer to append "\\s-*:".
-(defconst plastic-goal-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp plastic-keywords-goal) 
"\\)\\s-+\\([^:]+\\)")
-  "Regular expression which matches an entry in `plastic-keywords-goal'
-  and the name of the goal.")
-
-(defconst plastic-save-with-hole-regexp
-  (concat "\\(" (proof-ids-to-regexp plastic-keywords-save) 
"\\)\\s-+\\([^;]+\\)")
-  "Regular expression which matches an entry in
-  `plastic-keywords-save' and the name of the goal.")
-
-(defvar plastic-font-lock-keywords-1
-   (append
-    plastic-font-lock-terms
-    (list
-     (cons (proof-ids-to-regexp plastic-keywords) 'font-lock-keyword-face)
-     (cons (proof-ids-to-regexp plastic-tacticals) 'proof-tacticals-name-face)
-     (list plastic-goal-with-hole-regexp 2 'font-lock-function-name-face)
-     (list plastic-save-with-hole-regexp 2 'font-lock-function-name-face))))
-
-(defun plastic-init-syntax-table ()
-  "Set appropriate values for syntax table in current buffer."
-
-  (modify-syntax-entry ?_ "_")
-  (modify-syntax-entry ?\' "_")
-  (modify-syntax-entry ?\| ".")
-  (modify-syntax-entry ?\* ". 23")
-  (modify-syntax-entry ?\( "()1")
-  (modify-syntax-entry ?\) ")(4"))
-
-
-(provide 'plastic-syntax)
diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el
deleted file mode 100644
index 39f6c01..0000000
--- a/obsolete/plastic/plastic.el
+++ /dev/null
@@ -1,665 +0,0 @@
-;; plastic.el  - Major mode for Plastic proof assistant
-;;
-;; Portions © Copyright 2018  Free Software Foundation, Inc.
-;;
-;; Author: Paul Callaghan <P.C.Callaghan@durham.ac.uk>
-;;
-;; $Id$
-
-;; NOTES:
-;;     remember to prefix all potential cmds with plastic-lit-string
-;;     alternative is to fix the filtering
-
-
-(require 'proof)
-
-(require 'cl-lib)                       ;cl-member-if
-(eval-when-compile
-  (require 'span)
-  (require 'proof-syntax)
-  (require 'outline))
-(defvar plastic-keymap)                 ;FIXME: Not defined anywhere!
-
-(require 'plastic-syntax)
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;; User Configuration ;;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-;; I believe this is standard for Linux under RedHat -tms
-(defcustom plastic-tags "TO BE DONE"
-  "*The directory of the TAGS table for the Plastic library"
-  :type 'file
-  :group 'plastic)
-
-(defcustom plastic-test-all-name "need_a_global_lib"
-  "*The name of the LEGO module which inherits all other modules of the
-  library."
-  :type 'string
-  :group 'plastic)
-
-(eval-and-compile
-(defvar plastic-lit-string
-  ">"
-  "*Prefix of literate lines. Set to empty string to get non-literate mode"))
-
-(defcustom plastic-help-menu-list
-  '(["The PLASTIC Reference Card" (browse-url plastic-www-refcard) t]
-    ["The PLASTIC library (WWW)" (browse-url plastic-library-www-page)  t])
-  "List of menu items, as defined in `easy-menu-define' for Plastic
-  specific help."
-  :type '(repeat sexp)
-  :group 'plastic)
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;; Configuration of Generic Proof Package ;;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;; Users should not need to change this.
-
-(defvar plastic-shell-handle-output
-  (lambda (cmd string) 
-    (when (proof-string-match "^Module" cmd)
-      ;; prevent output and just give a minibuffer message
-      (setq proof-shell-last-output-kind 'systemspecific)
-      (message "Imports done!")))
-  "Acknowledge end of processing import declarations.")
-
-(defconst plastic-process-config
-  (concat plastic-lit-string
-         " &S ECHO No PrettyPrinting configuration implemented;\n")
-  "Command to enable pretty printing of the Plastic process.
-   Proof-General annotations triggered by a cmd-line opt
-  ")
-
-(defconst plastic-pretty-set-width "&S ECHO no PrettyWidth ;\n"
-  "Command to adjust the linewidth for pretty printing of the Plastic
-  process.")
-
-(defconst plastic-interrupt-regexp "Interrupt.."
-  "Regexp corresponding to an interrupt")
-
-
-;; ----- web documentation
-
-(defcustom plastic-www-home-page "http://www.dur.ac.uk/CARG/plastic.html";
-  "Plastic home page URL."
-  :type 'string
-  :group 'plastic)
-
-(defcustom plastic-www-latest-release
-  (concat plastic-www-home-page "/current")
-  "The WWW address for the latest Plastic release."
-  :type 'string
-  :group 'plastic)
-
-(defcustom plastic-www-refcard
-  plastic-www-home-page
-  "URL for the Plastic reference card."
-  :type 'string
-  :group 'plastic)
-
-(defcustom plastic-library-www-page
-  (concat plastic-www-home-page "/library")
-  "The HTML documentation of the Plastic library."
-  :type 'string
-  :group 'plastic)
-
-
-
-;; ----- plastic-shell configuration options
-
-(defcustom plastic-base
-  "/usr/local/plastic"
-  ;; da: was
-  ;; "PLASTIC_BASE:TO_BE_CUSTOMISED"
-  "*base dir of plastic distribution"
-  :type 'string
-  :group 'plastic)
-
-(defvar plastic-prog-name
-  (concat plastic-base "/bin/plastic")
-  "*Name of program to run as plastic.")
-
-(defun plastic-set-default-env-vars ()
-  "defaults for the expected lib vars."
-  (cond
-    ((not (getenv "PLASTIC_LIB"))
-               (setenv "PLASTIC_LIB" (concat plastic-base "/lib"))
-               (setenv "PLASTIC_TEST" (concat plastic-base "/test"))
-       )))
-
-(defvar plastic-shell-cd
-  (concat plastic-lit-string " &S ECHO no cd ;\n")
-  "*Command of the inferior process to change the directory.")
-
-(defvar plastic-shell-proof-completed-regexp "\\*\\*\\* QED \\*\\*\\*"
-  "*Regular expression indicating that the proof has been completed.")
-
-(defvar plastic-save-command-regexp
-  (concat "^" (proof-ids-to-regexp plastic-keywords-save)))
-(defvar plastic-goal-command-regexp
-  (concat "^" (proof-ids-to-regexp plastic-keywords-goal)))
-
-(defvar plastic-kill-goal-command
-  (concat plastic-lit-string " &S ECHO KillRef not applicable;"))
-(defvar plastic-forget-id-command
-  (concat plastic-lit-string " &S Forget "))
-
-(defvar plastic-undoable-commands-regexp
-  (proof-ids-to-regexp '("Refine" "Intros" "intros" "Normal" "Claim" "Immed"))
-  "Undoable list")
-
-;; "Dnf" "Refine" "Intros" "intros" "Next" "Normal"
-;;   "Qrepl" "Claim" "For" "Repeat" "Succeed" "Fail" "Try" "Assumption"
-;;   "UTac" "Qnify" "qnify" "andE" "andI" "exE" "exI" "orIL" "orIR" "orE" 
"ImpI"
-;;   "impE" "notI" "notE" "allI" "allE" "Expand" "Induction" "Immed"
-;;   "Invert"
-
-;; ----- outline
-
-(defvar plastic-goal-regexp "\\?\\([0-9]+\\)")
-
-(defvar plastic-outline-regexp
-  (concat "[[*]\\|"
-         (proof-ids-to-regexp
-          '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" 
"Inductive"
-     "Unfreeze"))))
-
-(defvar plastic-outline-heading-end-regexp ";\\|\\*)")
-
-(defvar plastic-shell-outline-regexp plastic-goal-regexp)
-(defvar plastic-shell-outline-heading-end-regexp plastic-goal-regexp)
-
-(defvar plastic-error-occurred
-       nil
-       "flag for whether undo is required for try or minibuffer cmds")
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Derived modes - they're here 'cos they define keymaps 'n stuff ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(define-derived-mode plastic-shell-mode proof-shell-mode
-   "plastic-shell"
-   ;; With nil argument for docstring, Emacs makes up a nice one.
-   nil
-   (plastic-shell-mode-config))
-
-(define-derived-mode plastic-mode proof-mode
-   "Plastic script"
-     "Major mode for Plastic proof scripts.
-
-\\{plastic-mode-map}"
-   (plastic-mode-config)
-   (easy-menu-change (list proof-general-name) (car proof-help-menu)
-                    (append (cdr proof-help-menu) plastic-help-menu-list)))
-
-(eval-and-compile
-  (define-derived-mode plastic-response-mode proof-response-mode
-    "PlasticResp" nil
-    (setq font-lock-keywords plastic-font-lock-terms)
-    (plastic-init-syntax-table)
-    (proof-response-config-done)))
-
-(define-derived-mode plastic-goals-mode proof-goals-mode
-  "PlasticGoals" "Plastic Goal State"
-  (plastic-goals-mode-config))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Code that's plastic specific                                      ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun plastic-count-undos (span)
-  "This is how to work out what the undo commands are.
-Given is the first SPAN which needs to be undone."
-  (let ((ct 0) string i
-       (tl (length proof-terminal-string)))
-    (while span
-      (setq string (span-property span 'cmd))
-      (plastic-preprocessing)                  ;; dynamic scope, on string
-      (cond ((eq (span-property span 'type) 'vanilla)
-            (if (or (proof-string-match plastic-undoable-commands-regexp 
string)
-                    (and (proof-string-match "Equiv" string)
-                         (not (proof-string-match "Equiv\\s +[TV]Reg" 
string))))
-                (setq ct (+ 1 ct))))
-           ((eq (span-property span 'type) 'pbp)
-            (setq i 0)
-            (while (< i (length string))
-              (if (string-equal (substring string i (+ i tl)) 
proof-terminal-string)
-                  (cl-incf ct))
-              (setq i (+ 1 i)))))
-      (setq span (next-span span 'type)))
-    (list (concat plastic-lit-string 
-                 " &S Undo x" (int-to-string ct) proof-terminal-string))))
-
-(defun plastic-goal-command-p (span)
-  "Decide whether argument is a goal or not"                   ;; NEED CHG.
-  (proof-string-match plastic-goal-command-regexp
-                     (or (span-property span 'cmd) "")))
-
-(defun plastic-find-and-forget (span)
-       ;; count the number of spans to undo.
-       ;; all spans are equal...
-    ;; (NB the 'x' before the id is required so xNN looks like an id,
-    ;;  so that Undo can be implemented via the tmp_cmd route.)
-  (let (string (spans 0))
-    (while span
-      ;; FIXME da: should probably ignore comments/proverproc here?
-      (setq string (span-property span 'cmd))
-      (plastic-preprocessing)          ;; dynamic scope, on string
-
-      (cond
-        ((null string) nil)
-        ((or (string-match "^\\s-*import" string)
-             (string-match "^\\s-*test" string)
-             (string-match "^\\s-*\\$" string)
-             (string-match "^\\s-*#" string))
-         
-         ; da: put this instead of XEmacs code
-         (message "Can't Undo imports yet!  You must exit Plastic for this!")
-       ;    (popup-dialog-box
-       ;       (list (concat "Can't Undo imports yet\n"
-       ;                          "You have to exit Plastic for this\n")
-       ;             ["ok, I'll do this" (lambda () t) t]))
-           (cl-return)  ;FIXME: No enclosing block?!
-          )    ;; warn the user that undo of imports not yet working.
-        (t (cl-incf spans))
-      )
-      (setq span (next-span span 'type))
-
-    )
-    (list (concat plastic-lit-string 
-                 " &S Undo x" (int-to-string spans) 
-                 proof-terminal-string))))
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Other stuff which is required to customise script management   ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun plastic-goal-hyp ()             ;; not used.
-  (cond
-   ((looking-at plastic-goal-regexp)
-    (cons 'goal (match-string 1)))
-   ((looking-at proof-shell-assumption-regexp)
-    (cons 'hyp (match-string 1)))
-   (t nil)))
-
-
-;; NEED TO REFINE THIS (may99)
-
-(defun plastic-state-preserving-p (cmd)
-  (not (proof-string-match plastic-undoable-commands-regexp cmd)))
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Commands specific to plastic                                      ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(eval-after-load "plastic" ;; da: so that plastic-lit-string can be changed
-  '(progn
-     (eval `(proof-defshortcut plastic-Intros
-                              ,(concat plastic-lit-string "Intros ")  
[(control i)]))
-     (eval `(proof-defshortcut plastic-Refine
-                              ,(concat plastic-lit-string "Refine ")  
[(control r)]))
-     (eval `(proof-defshortcut plastic-ReturnAll
-                              ,(concat plastic-lit-string "ReturnAll ") 
[(control u)]))))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Plastic shell startup and exit hooks                              ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defvar plastic-shell-current-line-width nil
-  "Current line width of the Plastic process's pretty printing module.
-  Its value will be updated whenever the corresponding screen gets
-  selected.")
-
-;; The line width needs to be adjusted if the PLASTIC process is
-;; running and is out of sync with the screen width
-
-(defun plastic-shell-adjust-line-width ()
-  "Use Plastic's pretty printing facilities to adjust output line width.
-   Checks the width in the `proof-goals-buffer'
-   ACTUALLY - still need to work with this. (pcc, may99)"
-   (and (proof-shell-live-buffer)
-       (proof-with-current-buffer-if-exists proof-goals-buffer
-       (let ((current-width
-              ;; Actually, one might sometimes
-              ;; want to get the width of the proof-response-buffer
-              ;; instead. Never mind.
-              (window-width (get-buffer-window proof-goals-buffer t))))
-
-          (if (equal current-width plastic-shell-current-line-width) ()
-            ; else
-            (setq plastic-shell-current-line-width current-width)
-            (set-buffer proof-shell-buffer)
-            (insert (format plastic-pretty-set-width (- current-width 1)))
-            )))))
-
-
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Configuring proof mode and setting up various utilities  ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun plastic-mode-config ()
-
-  (setq proof-terminal-string ";")
-  (setq proof-script-comment-start "(*")                       ;; these still 
active
-  (setq proof-script-comment-end "*)")
-
-  (setq proof-prog-name (concat plastic-prog-name ""))
-  (setenv "PROOF_GENERAL" "") ;; signal to plastic, use annotations
-
-  (setq proof-assistant-home-page plastic-www-home-page)
-
-  (setq proof-showproof-command (concat plastic-lit-string " &S PrfCtxt")
-       proof-goal-command      (concat plastic-lit-string " Claim %s;")
-       proof-save-command      (concat plastic-lit-string " Save %s;") ;; 
analogue?
-       proof-context-command   (concat plastic-lit-string " &S Ctxt 20"))
-
-  (setq proof-showproof-command  (concat plastic-lit-string " &S PrfCtxt")
-       proof-goal-command   (concat plastic-lit-string " Claim %s;")
-       proof-save-command   (concat plastic-lit-string " Save %s;") ;; 
analogue?
-       proof-context-command  (concat plastic-lit-string " &S Ctxt 20")
-          ;; show 20 things; see ^c+C...
-       proof-info-command   (concat plastic-lit-string " &S Help"))
-
-  (setq proof-goal-command-p 'plastic-goal-command-p
-       proof-count-undos-fn 'plastic-count-undos
-       proof-find-and-forget-fn 'plastic-find-and-forget
-       pg-topterm-goalhyplit-fn 'plastic-goal-hyp
-       proof-state-preserving-p 'plastic-state-preserving-p)
-
-  (setq        proof-save-command-regexp plastic-save-command-regexp
-       proof-goal-command-regexp plastic-goal-command-regexp
-       proof-save-with-hole-regexp plastic-save-with-hole-regexp
-       proof-goal-with-hole-regexp plastic-goal-with-hole-regexp
-       proof-kill-goal-command plastic-kill-goal-command
-       proof-indent-any-regexp
-       (proof-regexp-alt
-        (proof-ids-to-regexp plastic-commands)
-        "\\s(" "\\s)"))
-
-  (plastic-init-syntax-table)
-
-  ;; da: I've moved these out of proof-config-done in proof-script.el
-  (setq pbp-goal-command (concat "UNIMPLEMENTED"))
-  (setq pbp-hyp-command (concat "UNIMPLEMENTED"))
-
-;; font-lock
-
-  (set proof-script-font-lock-keywords plastic-font-lock-keywords-1)
-
-  (proof-config-done)
-
-;; outline
-
-  (make-local-variable 'outline-regexp)
-  (setq outline-regexp plastic-outline-regexp)
-
-  (make-local-variable 'outline-heading-end-regexp)
-  (setq outline-heading-end-regexp plastic-outline-heading-end-regexp)
-
-;; tags
-  (cond ((boundp 'tags-table-list)
-        (make-local-variable 'tags-table-list)
-        (setq tags-table-list (cons plastic-tags tags-table-list))))
-
-  (and (boundp 'tag-table-alist)
-       (setq tag-table-alist
-            (append '(("\\.lf$"   . plastic-tags)
-                      ("plastic"  . plastic-tags))
-                    tag-table-alist)))
-
-  (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t)
-
-;; hooks and callbacks
-
-  (add-hook 'proof-shell-insert-hook       'plastic-shell-adjust-line-width)
-  (add-hook 'proof-shell-handle-error-or-interrupt-hook 'plastic-had-error)
-  (add-hook 'proof-shell-insert-hook       'plastic-preprocessing)
-
-;; (add-hook 'proof-shell-handle-error-or-interrupt-hook
-;; (lambda()(goto-char (search-forward (regexp-quote proof-terminal-char)))))
-
-;;  (add-hook 'proof-shell-handle-delayed-output-hook 
`plastic-show-shell-buffer t)
-;; this forces display of shell-buffer after each cmd, rather than goals-buffer
-;; it is not always necessary - could always add it as a toggle option?
-
-;; set up the env.
-  (plastic-set-default-env-vars)
-  )
-
-(defun plastic-show-shell-buffer ()
-   "switch buffers."
-   (display-buffer proof-shell-buffer)
-   )
-
-
-(defun plastic-equal-module-filename (module filename)
-  "Returns `t' if MODULE is equal to the FILENAME and `nil' otherwise.
-The directory and extension is stripped of FILENAME before the test."
-  (equal module
-        (file-name-sans-extension (file-name-nondirectory filename))))
-
-(defun plastic-shell-compute-new-files-list ()
-  "Function to update `proof-included-files list'.
-Value for `proof-shell-compute-new-files-list', which see.
-
-For Plastic, we assume that module identifiers coincide with file names."
-  (let ((module (match-string 1)))
-    (cdr (cl-member-if
-         (lambda (filename) (plastic-equal-module-filename module filename))
-         proof-included-files-list))))
-
-
-
-(defun plastic-shell-mode-config ()
-  (setq proof-shell-cd-cmd plastic-shell-cd
-       proof-shell-proof-completed-regexp plastic-shell-proof-completed-regexp
-       proof-shell-error-regexp plastic-error-regexp
-       proof-shell-interrupt-regexp plastic-interrupt-regexp
-       ;; DEAD proof-shell-noise-regexp "Discharge\\.\\. "
-       proof-shell-assumption-regexp plastic-id
-       proof-shell-start-goals-regexp plastic-goal-regexp
-       pg-subterm-first-special-char ?\360
-       pg-subterm-start-char ?\372
-       pg-subterm-sep-char ?\373
-       pg-subterm-end-char ?\374
-       pg-topterm-regexp "\375"
-       proof-shell-eager-annotation-start "\376"
-       ;; FIXME da: if p-s-e-a-s is implemented, you should set
-       ;; proof-shell-eager-annotation-start-length=1 to
-       ;; avoid possibility of duplicating short messages.
-       proof-shell-eager-annotation-end "\377"
-
-       proof-shell-annotated-prompt-regexp "LF> \371"
-       proof-shell-result-start "\372 Pbp result \373"
-       proof-shell-result-end "\372 End Pbp result \373"
-       proof-shell-start-goals-regexp "\372 Start of Goals \373"
-       proof-shell-end-goals-regexp "\372 End of Goals \373"
-
-       proof-shell-init-cmd plastic-process-config
-       proof-shell-restart-cmd plastic-process-config
-       pg-subterm-anns-use-stack nil
-       proof-shell-handle-output-system-specific plastic-shell-handle-output
-       plastic-shell-current-line-width nil
-
-       proof-shell-process-file
-       (cons "Creating mark \"\\(.*\\)\" \\[\\(.*\\)\\]"
-             (lambda () (let ((match (match-string 2)))
-                             (if (equal match "") match
-                               (concat 
-                                (file-name-sans-extension match) ".lf")))))
-
-       proof-shell-retract-files-regexp "forgot back through Mark \"\\(.*\\)\""
-       ;; DEAD: proof-shell-font-lock-keywords plastic-font-lock-keywords-1
-
-       proof-shell-compute-new-files-list 
'plastic-shell-compute-new-files-list)
-
-  (plastic-init-syntax-table)
-
-  (proof-shell-config-done)
-  )
-
-(defun plastic-goals-mode-config ()
-  (setq pg-goals-change-goal "Next %s;"
-       pg-goals-error-regexp plastic-error-regexp)
-  (setq proof-goals-font-lock-keywords plastic-font-lock-terms)
-  (plastic-init-syntax-table)
-  (proof-goals-config-done))
-
-
-
-;;;;;;;;;;;;;;;;;
-;; MY new additions.
-
-(defun plastic-small-bar () (interactive) (insert 
"%------------------------------\n"))
-
-(defun plastic-large-bar () (interactive) (insert 
"%-------------------------------------------------------------------------------\n"))
-
-(defun plastic-preprocessing () ;; NB: dynamic scoping of string
-   "clear comments and remove literate marks (ie, \\n> ) - acts on var string"
-
-   (with-no-warnings
-   ;; might want to use proof-string-match here if matching is going
-   ;; to be case sensitive (see docs)
-
-   (if (= 0 (length plastic-lit-string))
-       string                          ; no-op if non-literate
-                                       ; remaining lines are the
-                                       ; Else. (what, no 'return'?)
-   (setq string (concat "\n" string " "))   ;; seed routine below, & extra char
-   (let* ;; da: let* not really needed, added to nuke byte-comp warnings.
-       (x
-       (i 0)
-       (l (length string))
-       (eat-rest (lambda ()
-                   (aset string i ?\ )  ;; kill the \n or "-" at least
-                   (cl-incf i)
-                   (while (and (< i l) (/= (aref string i) ?\n))
-                     (aset string i ?\ )
-                     (cl-incf i) )))
-       (keep-rest (lambda ()
-                    (cl-loop for x in (string-to-list plastic-lit-string)
-                             do (aset string i ?\ ) (cl-incf i))
-                    (while (and (< i l)
-                                (/= (aref string i) ?\n)
-                                (/= (aref string i) ?-))
-                      (cl-incf i) ))))
-     (while (< i l)
-       (cond
-       ((eq 0 (string-match "--" (substring string i)))
-        (funcall eat-rest))            ; comment.
-       ((eq 0 (string-match "\n\n" (substring string i)))
-        (aset string i ?\ )
-        (cl-incf i))                   ; kill repeat \n
-       ((= (aref string i) ?\n)        ; start of new line
-        (aset string i ?\ ) (cl-incf i)        ; remove \n
-        (if (eq 0 (string-match plastic-lit-string
-                                (substring string i)))
-            (funcall keep-rest)        ; code line.
-          (funcall eat-rest)           ; non-code line
-          ))
-       (t
-        (cl-incf i))))                 ; else include.
-     (setq string (replace-regexp-in-string "  +" " " string))
-     (setq string (replace-regexp-in-string "^ +" "" string))
-   (if (string-match "^\\s-*$" string)
-       (setq string (concat "ECHO comment line" proof-terminal-string))
-     string)))))
-
-
-(defun plastic-all-ctxt ()
-       "show the full ctxt"
-       (interactive)
-       (proof-shell-invisible-command
-             (concat plastic-lit-string " &S Ctxt" proof-terminal-string))
-       )
-
-(defun plastic-send-one-undo ()
-       "send an Undo cmd"
-    ;; FIXME etc
-    ;; is like this because I don't want the undo output to be shown.
-    (proof-shell-insert (concat plastic-lit-string " &S Undo;")
-                       'proof-done-invisible))
-
-;; hacky expt version.
-;; still don't understand the significance of cmd!
-
-(defun plastic-minibuf-cmd (cmd)
-    "do minibuffer cmd then undo it, if error-free."
-    (interactive
-     (list (read-string "Command: " nil 'proof-minibuffer-history)))
-    (print "hello")
-    (plastic-reset-error)
-    (if (and proof-state-preserving-p
-          (not (funcall proof-state-preserving-p cmd)))
-      (error "Command is not state preserving, I won't execute it!"))
-    (proof-shell-invisible-command cmd)
-    (plastic-call-if-no-error 'plastic-send-one-undo))
-
-(defun plastic-minibuf ()
-    "do minibuffer cmd then undo it, if error-free."
-    (interactive)
-    (plastic-reset-error)
-    (plastic-send-minibuf)
-    (plastic-call-if-no-error 'plastic-send-one-undo))
-
-(defun plastic-synchro ()
-    "do minibuffer cmd BUT DON'T UNDO IT - use if things go wrong!"
-    (interactive)
-    (plastic-send-minibuf))
-
-(defun plastic-send-minibuf ()
-    "take cmd from minibuffer - see doc for proof-minibuffer-cmd"
-    (interactive)
-    (let (cmd)
-       (setq cmd (read-string "Command: " nil 'proof-minibuffer-history))
-       (setq cmd (concat plastic-lit-string " " cmd proof-terminal-string))
-       (proof-shell-invisible-command cmd)))
-
-(defun plastic-had-error ()
-    "sets var plastic-error-occurred, called from hook"
-    (if (eq proof-shell-error-or-interrupt-seen 'error)
-       (setq plastic-error-occurred t)))
-(defun plastic-reset-error ()
-    "UNsets var plastic-error-occurred, before minibuffer or try cmd"
-    (setq plastic-error-occurred nil))
-(defun plastic-call-if-no-error (fn)
-    "wait for proof process to be idle, and call fn if error-free."
-    (while proof-shell-busy (sleep-for 0.25))
-    (if (not plastic-error-occurred) (funcall fn)))
-
-(defun plastic-show-shell ()
-    "shortcut to shell buffer"
-    (interactive)
-    (proof-switch-to-buffer proof-shell-buffer))
-
-(define-key plastic-keymap [(control s)] 'plastic-small-bar)
-(define-key plastic-keymap [(control l)] 'plastic-large-bar)
-(define-key plastic-keymap [(control c)] 'plastic-all-ctxt)
-(define-key plastic-keymap [(control v)] 'plastic-minibuf)
-(define-key plastic-keymap [(control o)] 'plastic-synchro)
-(define-key plastic-keymap [(control p)] 'plastic-show-shell)
-
-
-;; original end.
-
-;;;;;;;;;;;;;;;;;
-;; hacky overriding of the toolbar command and C-c C-v action
-;; my version handles literate characters.
-;; (should do better for long-term though)
-
-(defalias 'proof-toolbar-command 'plastic-minibuf)
-(defalias 'proof-minibuffer-cmd  'plastic-minibuf)
-       ;; the latter doesn't seem to work (pcc, 05aug02)
-
-;;;
-
-(provide 'plastic)
diff --git a/obsolete/plastic/test.lf b/obsolete/plastic/test.lf
deleted file mode 100644
index 7c163d3..0000000
--- a/obsolete/plastic/test.lf
+++ /dev/null
@@ -1,64 +0,0 @@
-EXAMPLE FILE: less than or equal on Nat
-
-%---------------------------------------
-Nat
-
-> Inductive
->      [Nat : Type]
->      Constructors
->      [zero : Nat]
->      [succ : (n:Nat)Nat];
-
-> [plus [m:Nat] = E_Nat ([_:Nat]Nat) m ([_:Nat]succ) ];
-
-
------------------------
-Non-dependent Pi type.
-
-> Inductive
->      [A,B:Type]
->      [Pi_ : Type]
->      Constructors
->      [La_ : (f:(x:El A)El B)Pi_ ];
-
-
-application of Pi_ types, ie conversion to a dependent product.
-
-> Claim ap_ : (A,B:Type) Pi_ A B -> A -> B;
-> Intros A B f x;
-> Refine E_Pi_ ? ? ([_:?]B);
-> Refine f;
-> Intros fo;
-> Refine fo x;
-> ReturnAll;
-> ap_;
-
-
-
-%---------------------------------------
-Combined leq with if-branch - thus avoiding Boolean type.
-
-Notice that we have to prove (Pi_ Nat T) by induction on x, since we can't
-eliminate over (Nat -> T) in LF. 
-
-
-> Claim if_leq : (x,y:Nat)(T:Type)T -> T -> T;
-> Intros x y T leq not_leq;
-> Refine ap_ ? ? (ap_ ? ? ? x) y;
-
-> Refine La_;
-> Intros x1;
-> Refine E_Nat ([_:?]Pi_ Nat T) ?x_z ?x_s x1;
-> x_z Refine La_ ? ? ([_:?]leq);
-> Intros x1_ f_x1_;
-> Refine La_;
-> Intros y1;
-> Refine E_Nat ([_:?]T) ?y_z ?y_s y1;
-> y_z Refine not_leq;
-> Intros y1_ _;
-> Refine ap_ ? ? f_x1_ y1_;
-> ReturnAll;
-
-> if_leq;
-
-
diff --git a/proof-general.el b/proof-general.el
index 4feed65..b241255 100644
--- a/proof-general.el
+++ b/proof-general.el
@@ -81,7 +81,7 @@
            ;; FIXME: These dirs used to not be listed, but I needed to add
            ;; them for the compilation to succeed for me.  --Stef
            ;; These dirs are now obsolete and not published on MELPA.  --Erik
-           ;; "isar" "obsolete/plastic"
+           ;; "isar"
        )))
     (dolist (dir byte-compile-directories)
       (add-to-list 'load-path (expand-file-name dir pg-init--pg-root)))))