Renamed file obsolete/plastic/plastic.el, formerly plastic/plastic.el

1 files changed, 661 insertions, 0 deletions

diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el
new file mode 100644
index 00000000..3461dbb8
--- /dev/null
+++ b/obsolete/plastic/plastic.el
@@ -0,0 +1,661 @@
+;; plastic.el  - Major mode for Plastic proof assistant
+;;
+;; 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)
+
+(eval-when-compile
+  (require 'cl)
+  (require 'span)
+  (require 'proof-syntax)
+  (require 'outline)
+  (defvar plastic-keymap nil))
+
+(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)
+    (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 (= (aref string i) proof-terminal-char) (setq ct (+ 1 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]))
+	    (return)
+	   )    ;; warn the user that undo of imports not yet working.
+	 (t (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-char ?\;)
+  (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 (char-to-string  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 (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
+		    (incf i)
+		    (while (and (< i l) (/= (aref string i) ?\n))
+		      (aset string i ?\ )
+		      (incf i) )))
+	(keep-rest (lambda ()
+		     (loop for x in (string-to-list plastic-lit-string)
+		       do (aset string i ?\ ) (incf i))
+		     (while (and (< i l)
+				 (/= (aref string i) ?\n)
+				 (/= (aref string i) ?-))
+		       (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 ?\ )
+	 (incf i))			; kill repeat \n
+	((= (aref string i) ?\n)	; start of new line
+	 (aset string i ?\ ) (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
+	 (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)