diff options
| author | Paul Callaghan | 1999-11-11 16:16:58 +0000 |
|---|---|---|
| committer | Paul Callaghan | 1999-11-11 16:16:58 +0000 |
| commit | 8c84cda43b393f0f4264df25a8aec91ea5f94b53 (patch) | |
| tree | 89e01f9e42391bc8c0e558bcf35271e57fbfc828 /generic | |
| parent | d0de06e3f8412da49f8423c211653e76437ee689 (diff) | |
small changes to plastic mode
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 5 |
1 files changed, 2 insertions, 3 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. |