diff options
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? |