diff options
| author | Pierre Courtieu | 2006-09-08 08:34:46 +0000 |
|---|---|---|
| committer | Pierre Courtieu | 2006-09-08 08:34:46 +0000 |
| commit | 2fb137dc539ac966f571e7e065ff4fab7f8b33b4 (patch) | |
| tree | 45ead2765d3028f18cf3c576708e64dae81944e8 | |
| parent | e68b54486c6f010a13a6de11e2ff3e0858f40a59 (diff) | |
Fixed nested comment support for scripting, in xemacs (worked already
on GNU Emacs). Instanciated proof-parse-function for that...
| -rw-r--r-- | coq/coq-indent.el | 10 | ||||
| -rw-r--r-- | coq/coq.el | 6 |
2 files changed, 15 insertions, 1 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 34021c57..4e0e3bd2 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -223,6 +223,16 @@ far as possible and return nil." (if (< direction 0) (coq-find-command-end-backward) (coq-find-command-end-forward))) +;; This one to deal with nested comments in xemacs +(defun coq-parse-function () + (skip-chars-forward " \n\t") + (forward-char 1) + (if (coq-find-comment-end) + 'comment + (when (coq-find-command-end-forward) + (forward-char 1) + 'cmd))) + (defun coq-find-current-start () "Move to the start of command at point. The point is put exactly after the end of previous command, or at the (point-min if @@ -832,6 +832,11 @@ This is specific to `coq-mode'." proof-state-preserving-p 'coq-state-preserving-p ) + ;; This one to deal with nested comments in xemacs + (if (string-match "XEmacs" emacs-version) + (setq proof-script-parse-function 'coq-parse-function) + ) + (setq proof-save-command-regexp coq-save-command-regexp proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>. proof-save-with-hole-regexp coq-save-with-hole-regexp @@ -1427,7 +1432,6 @@ buffer." ;; clean the response buffer from ultra-ugly underlined command line ;; parsed above. Don't kill the first \n (when (and clean mtch) (delete-region (+ mtch 1) (match-end 0))) - (goto-char (point-max)) (when mtch (let* ((pos (length (match-string 1))) (lgth (length (match-string 2))) |