diff options
| -rw-r--r-- | generic/proof-shell.el | 5 | ||||
| -rw-r--r-- | plastic/plastic.el | 13 |
2 files changed, 12 insertions, 6 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 2b948fa2..44ef4e5e 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1057,8 +1057,7 @@ particularly in proof-start-queue and proof-shell-exec-loop." ;; Lego uses this hook for setting the pretty printer ;; width, Coq uses it for sending an initialization string ;; (although it could presumably use proof-shell-init-cmd?). - ;; Paul Callaghan wants to use this hook to massage STRING - ;; to remove literate-style markup from input. + ;; Plastic uses this hook to remove literate-style markup from 'string'. (run-hooks 'proof-shell-insert-hook) ;; Now we replace CRs from string with spaces. This was done in @@ -1778,4 +1777,4 @@ processing." (provide 'proof-shell) -;; proof-shell.el ends here.
\ No newline at end of file +;; proof-shell.el ends here. 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? |