From 8c84cda43b393f0f4264df25a8aec91ea5f94b53 Mon Sep 17 00:00:00 2001
From: Paul Callaghan
Date: Thu, 11 Nov 1999 16:16:58 +0000
Subject: small changes to plastic mode

---
 plastic/plastic.el | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

(limited to 'plastic')

diff --git a/plastic/plastic.el b/plastic/plastic.el
index 569fb12b..2795bd4b 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -118,7 +118,7 @@
 ;; ----- plastic-shell configuration options
 
 (defvar plastic-base 
-  (expand-file-name "~lego/OTHER/plastic")
+  "PLASTIC_BASE:TO_BE_CUSTOMISED"
   "*base dir of plastic distribution")
 
 (defvar plastic-prog-name 
@@ -256,8 +256,10 @@ Given is the first SPAN which needs to be undone."
 
       (cond
          ((null string) nil)
-         ((or (proof-string-match "\\s-*import" string) 
-	      (proof-string-match "\\s-*test" string))
+         ((or (string-match "^\\s-*import" string) 
+	      (string-match "^\\s-*test" string)
+	      (string-match "^\\s-*\\$" string)
+	      (string-match "^\\s-*#" string))
                (if (yes-or-no-p-dialog-box 
                            (concat "Can't Undo imports yet\n"
                                    "You have to exit prover for this\n"
@@ -388,6 +390,11 @@ Given is the first SPAN which needs to be undone."
   (setq proof-assistant-home-page plastic-www-home-page)
   (setq proof-mode-for-script 'plastic-mode)
 
+  (setq proof-prf-string   (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-ctxt-string  (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? 
-- 
cgit v1.2.3