diff options
| -rw-r--r-- | coq/coq.el | 24 | ||||
| -rw-r--r-- | generic/pg-response.el | 5 | ||||
| -rw-r--r-- | generic/proof-config.el | 5 |
3 files changed, 24 insertions, 10 deletions
@@ -252,12 +252,13 @@ See also `coq-hide-additional-subgoals'." :type 'regexp :group 'coq-proof-tree) +;; pc: <infomsg> now has a newline (better output indentation) (defcustom coq-proof-tree-branch-finished-regexp (concat "^\\(\\(?:Proof completed\\.\\)\\|\\(?:No more subgoals\\.\\)\\|" "\\(No more subgoals but non-instantiated " "existential variables:\\)\\|" - "\\(<infomsg>This subproof is complete, but there are " - "still unfocused goals.</infomsg>\\)\\)") + "\\(<infomsg>\\s-*This subproof is complete, but there are " + "still unfocused goals.\\s-*</infomsg>\\)\\)") "Regexp for `proof-tree-branch-finished-regexp'." :type 'regexp :group 'coq-proof-tree) @@ -340,9 +341,13 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3." ;; (defun coq-remove-trailing-blanks (s) - (let ((pos (string-match "[[:blank:]]*\\'" s))) + (let ((pos (string-match "\\s-*\\'" s))) (substring s 0 pos))) +(defun coq-remove-starting-blanks (s) + (string-match "\\`\\s-*" s) + (substring s (match-end 0) (length s))) + ;; Due to the architecture of proofgeneral, informative message put *before* ;; the goal disappear unless marked as "urgent", i.e. being enclosed with @@ -362,12 +367,15 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3." (min end (save-excursion (end-of-line) (point)) (+ start 75)))) - (let* ((face + (let* + ((face (progn (goto-char start) - (if (looking-at "<infomsg>") 'default-face + (if (looking-at "<infomsg>") 'default 'proof-eager-annotation-face))) - (str (proof-shell-strip-eager-annotations start end)) - (strnotrailingspace (coq-remove-trailing-blanks str))) + (str (proof-shell-strip-eager-annotations start end)) + (strnotrailingspace + (coq-remove-starting-blanks (coq-remove-trailing-blanks str)))) + (message "STR = %S" strnotrailingspace) (pg-response-display-with-face strnotrailingspace face))) @@ -1307,7 +1315,7 @@ Warning: (setq proof-script-parse-function 'coq-script-parse-function) (setq proof-script-comment-start "(*") (setq proof-script-comment-end "*)") - + (setq proof-script-insert-newlines nil) (set (make-local-variable 'comment-start-skip) (regexp-quote (if (string-equal "" proof-script-comment-start) "\n" ;; end-of-line terminated comments diff --git a/generic/pg-response.el b/generic/pg-response.el index 89c35e9d..7afa77a5 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -357,8 +357,9 @@ Returns non-nil if response buffer was cleared." ;; with warnings after delayed output (non newline terminated). (goto-char (point-max)) ;; insert a newline before the new message unless the - ;; buffer is empty - (unless (eq (point-min) (point-max)) + ;; buffer is empty or proof-script-insert-newlines is nil + (unless (or (not proof-script-insert-newlines) + (eq (point-min) (point-max))) (newline)) (setq start (point)) (insert str) diff --git a/generic/proof-config.el b/generic/proof-config.el index 280b98cf..9f4494d2 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -752,6 +752,11 @@ Elisp errors will be trapped when evaluating; set :type 'string :group 'proof-script) +(defcustom proof-script-insert-newlines t + "if non-nil inserts a newline between each message in response buffer." + :type 'boolean + :group 'proof-script) + (defcustom proof-script-font-lock-keywords nil "Value of `font-lock-keywords' used to fontify proof scripts. |