path: root/obsolete/plastic/plastic.el

;; 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)