diff options
| author |  Paul Callaghan <p.c.callaghan@durham.ac.uk> | 1999-11-11 16:16:58 +0000 |
|---|---|---|
| committer | Paul Callaghan <p.c.callaghan@durham.ac.uk> | 1999-11-11 16:16:58 +0000 |
| commit | 8c84cda43b393f0f4264df25a8aec91ea5f94b53 (patch) | |
| tree | 89e01f9e42391bc8c0e558bcf35271e57fbfc828 /plastic | |
| parent | d0de06e3f8412da49f8423c211653e76437ee689 (diff) | |
small changes to plastic mode
Diffstat (limited to 'plastic')
| -rw-r--r-- | plastic/plastic.el | 13 |
1 files changed, 10 insertions, 3 deletions
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? |