From 0527617029cb1c1bc8250db9a93fb6c537bd7d67 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 6 May 2004 15:29:57 +0000 Subject: bug fix with terminal regexp (pb with :"unfold foo in |- *.") --- coq/coq-abbrev.el | 4 ++-- coq/coq-syntax.el | 46 ++++++++++++++++++++++++---------------------- coq/coq.el | 3 ++- 3 files changed, 28 insertions(+), 25 deletions(-) diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 7843e529..78f9aea6 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -72,7 +72,7 @@ ("i" "intro " holes-abbrev-complete 10) ("if" "if # then # else #" holes-abbrev-complete 1) ("in" "intro" holes-abbrev-complete 1) - ("inf" "infix \"#\" := # (at level #) : @{scope}." holes-abbrev-complete 1) + ("inf" "Infix \"#\" := # (at level #) : @{scope}." holes-abbrev-complete 1) ("ind" "induction #" holes-abbrev-complete 2) ("indv" "Inductive # : # := # : #." holes-abbrev-complete 0) ("indv2" "Inductive # : # :=\n| # : #\n| # : #." holes-abbrev-complete 0) @@ -191,7 +191,7 @@ ) ("Notations" "COMMAND ABBREVIATION" - ["infix inf" (insert-and-expand "inf") t] + ["Infix inf" (insert-and-expand "inf") t] ["Notation (no assoc) nota" (insert-and-expand "nota") t] ["Notation (assoc) notas" (insert-and-expand "notas") t] ["Notation (no assoc, scope) notasc" (insert-and-expand "notasc") t] diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 39af0890..560d8aa3 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -25,33 +25,35 @@ (defvar coq-version-is-V6 nil "This variable can be set to t to force ProofGeneral to coq version coq-6.x. To do that, put (setq coq-version-is-V6 t) in your .emacs and -restart emacs. This variable overrides coq-version-is-V7 and -coq-version-is-V74. If none of these 3 variables is set to t, then -ProofGeneral guesses the version of coq by doing 'coqtop -v'.") - -(defvar coq-version-is-V7 nil - "This variable can be set to t to force ProofGeneral to coq version -between coq-7.0 and coq-7.3.1. To do that, put (setq coq-version-is-V7 t) -in your .emacs and restart emacs. This variable overrides -coq-version-is-V74 and is overrriden by coq-version-is-V6. If none of -these 3 variables is set to t, then ProofGeneral guesses the version of -coq by doing 'coqtop -v'.") - -(defvar coq-version-is-V74 nil - "This variable can be set to t to force ProofGeneral to coq version -coq-7.4. To do that, put (setq coq-version-is-V74 t) in your -.emacs and restart emacs. This variable is overrriden by -coq-version-is-V6 and coq-version-is-V7. If none of these 3 variables -is set to t, then ProofGeneral guesses the version of coq by doing -'coqtop -v'." ) +restart emacs. This variable overrides coq-version-is-V7, V8 and +V74. If none of these 3 variables is set to t, then ProofGeneral +guesses the version of coq by doing 'coqtop -v'.") + +(defvar coq-version-is-V7 nil +"This variable can be set to t to force ProofGeneral to coq version +between coq-7.0 and coq-7.3.1. To do that, put (setq coq-version-is-V7 +t) in your .emacs and restart emacs. This variable overrides +coq-version-is-V74 and V8 and is overrriden by coq-version-is-V6. If +none of these 3 variables is set to t, then ProofGeneral guesses the +version of coq by doing 'coqtop -v'.") -(defvar coq-version-is-V8 nil - "This variable can be set to t to force ProofGeneral to coq version +(defvar coq-version-is-V74 nil +"This variable can be set to t to force ProofGeneral to coq version +coq-7.4. To do that, put (setq coq-version-is-V74 t) in your .emacs +and restart emacs. This variable is overrriden by coq-version-is-V6 +and coq-version-is-V7. If none of these 3 variables is set to t, then +ProofGeneral guesses the version of coq by doing 'coqtop -v'. If this +variable is put to t (before PG is loaded) then V7 is automatically +put to t." ) + +(defvar coq-version-is-V8 nil +"This variable can be set to t to force ProofGeneral to coq version above coq-8.0beta. To do that, put (setq coq-version-is-V8 t) in your .emacs and restart emacs. This variable is overrriden by coq-version-is-V6, coq-version-is-V7 and coq-version-is-V74. If none of these 4 variables is set to t, then ProofGeneral guesses the -version of coq by doing 'coqtop -v'." ) +version of coq by doing 'coqtop -v'. If this variable is put to t +(before PG is loaded) then V74 is automatically put to t." ) diff --git a/coq/coq.el b/coq/coq.el index 35c63e94..d64d4e93 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -622,7 +622,8 @@ Based on idea mentioned in Coq reference manual." (setq proof-terminal-char ?\.) (setq proof-script-command-end-regexp (if coq-version-is-V7 - "\\(?:\\w\\|\\s-\\|\\s)\\|\\(?:\\.\\.\\)+\\)\\.\\(\\s-\\|\\'\\)" +; "\\(?:\\w\\|\\s-\\|\\s)\\|\\\\*\\|\\(?:\\.\\.\\)+\\)\\.\\(\\s-\\|\\'\\)" + "\\(?:[^.]\\|\\(?:\\.\\.\\)\\)\\.\\(\\s-\\|\\'\\)" "[.]")) (setq proof-script-comment-start "(*") (setq proof-script-comment-end "*)") -- cgit v1.2.3