Compatibility with coq trunk where some special symbols are removed.

3 files changed, 13 insertions, 7 deletions

diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 33c4e6c3..ab0fd279 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -897,6 +897,10 @@ Used by `coq-goal-command-p'"
    (list (coq-first-abstr-regexp "\\<fun\\>" "\\(?:=>\\|:\\)") 1 'font-lock-variable-name-face)
    ;; forall binder
    (list (coq-first-abstr-regexp "\\<forall\\>" "\\(?:,\\|:\\)") 1 'font-lock-variable-name-face)
+;   (list "\\<forall\\>"
+;         (list 0 font-lock-type-face)
+;         (list (concat "[^ :]\\s-*\\(" coq-ids "\\)\\s-*") nil nil 
+;               (list 0 font-lock-variable-name-face)))
    ;; parenthesized binders
    (list (coq-first-abstr-regexp "(" ":[ a-zA-Z]") 1 'font-lock-variable-name-face)
    )
@@ -932,7 +936,6 @@ Used by `coq-goal-command-p'"
   (concat "\\(" (proof-ids-to-regexp coq-keywords-defn)
           "\\)\\s-+\\(" coq-id "\\)"))
 
-
 ; must match:
 ; "with f x y :" (followed by = or not)
 ; "with f x y (z:" (not followed by =)
diff --git a/coq/coq.el b/coq/coq.el
index 68ea9bc1..78915803 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -66,7 +66,7 @@ To disable coqc being called (and use only make), set this to nil."
 (require 'coq-syntax)
 (require 'coq-indent)
 
-8(defvar coq-utf-safe coq-version-is-V8-1
+(defvar coq-utf-safe coq-version-is-V8-1
   "Obsolete, coq >= 8.1 does not use special symbols for delimiting prompts.")
 
 (if coq-version-is-V8-1 
@@ -76,7 +76,7 @@ To disable coqc being called (and use only make), set this to nil."
 ;; utf-8 is not yet well accepted (especially by xemacs)
 ;Set to t in your .emacs to enable it. Needs to load library `un-define' to
 ;work on xemacs."
-(setq proof-shell-unicode nil)
+(or (boundp 'proof-shell-unicode) (setq proof-shell-unicode nil))
 
 (defcustom coq-prog-env nil
   "*List of environment settings d to pass to Coq process.
@@ -961,9 +961,12 @@ To be used in `proof-shell-process-output-system-specific'."
    pg-subterm-sep-char ?\373            ; not done
    pg-subterm-end-char ?\374            ; not done
    pg-topterm-regexp "\375"
-   proof-shell-eager-annotation-start "\376\\|\\[Reinterning"
+   proof-shell-eager-annotation-start "\376\\|\\[Reinterning\\|Warning:"
    proof-shell-eager-annotation-start-length 12
-   proof-shell-eager-annotation-end "\377\\|done\\]" ; done
+   ;; ****** is added at the end of warnings in emacs mode, this is temporary I
+   ;;        want xml like tags, and I want them removed before warning display.
+   ;; I want the same for errors -> pgip
+   proof-shell-eager-annotation-end "\377\\|done\\]\\|\\*\\*\\*\\*\\*\\*" ; done
    proof-shell-annotated-prompt-regexp proof-shell-prompt-pattern
    proof-shell-result-start "\372 Pbp result \373"
    proof-shell-result-end "\372 End Pbp result \373"
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index e97fdd52..9d806a86 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -434,8 +434,8 @@ Does nothing if proof assistant is already running."
 		(setq proof-eagerly-raise nil))
 	      ;; Set mode for goals buffer
 	      (set-buffer proof-goals-buffer)
-	      (and (fboundp 'toggle-enable-multibyte-characters)
-		   (toggle-enable-multibyte-characters -1))
+;	      (and (fboundp 'toggle-enable-multibyte-characters)
+;		   (toggle-enable-multibyte-characters -1))
 	      (funcall proof-mode-for-goals)
 	      ;; Setting modes initialises local variables which
 	      ;; may affect frame/buffer appearance: so we fire up frames