From 062204d996652b87ee1398c630937eda69b929c0 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 9 Sep 2010 13:12:50 +0000 Subject: Moved the modeline dislpay of open goals to scripting buffer. --- coq/coq.el | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index cb5b91d0..4530efb2 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1371,9 +1371,9 @@ number of hypothesis displayed, without hiding the goal" (select-window curwin) ))) -(defvar coq-modeline-string2 " SUBGOALS* ") -(defvar coq-modeline-string1 " SUBGOAL* ") -(defvar coq-modeline-string0 " Scripting *") +(defvar coq-modeline-string2 ")") +(defvar coq-modeline-string1 ")") +(defvar coq-modeline-string0 " Script(") (defun coq-build-subgoals-string (n) (concat coq-modeline-string0 (int-to-string n) (if (> n 1) coq-modeline-string2 @@ -1384,6 +1384,7 @@ number of hypothesis displayed, without hiding the goal" (save-window-excursion ; switch to buffer even if not visible (switch-to-buffer proof-goals-buffer) (let* ((nbgoals (string-to-number (first-word-of-buffer))) + (dummy (switch-to-buffer proof-script-buffer)) (toclean (assq 'proof-active-buffer-fake-minor-mode minor-mode-alist))) (while toclean ;; clean minor-mode-alist (setq minor-mode-alist (remove toclean minor-mode-alist)) -- cgit v1.2.3