diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2010-09-09 13:12:50 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2010-09-09 13:12:50 +0000 |
| commit | 062204d996652b87ee1398c630937eda69b929c0 (patch) | |
| tree | 14c7184785ed0db988955bf6e5608cfcfc7eae97 | |
| parent | 09ee7250a06c8fe23b8a7ab093f683e1d336bd48 (diff) | |
Moved the modeline dislpay of open goals to scripting buffer.
| -rw-r--r-- | coq/coq.el | 7 |
1 files changed, 4 insertions, 3 deletions
@@ -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)) |