diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2004-08-30 13:36:53 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2004-08-30 13:36:53 +0000 |
commit | 803614383b7247bd7dd7739cc24749de245ae7c9 (patch) | |
tree | b3abac949aacf03525e7a741ed26053bdb75eabf /coq | |
parent | c4aaf65bc749e139f3d87d8780e5110cdcc1a488 (diff) |
debugged the indentation of coq (bug report of Batsiaan Zapf august
3rd 2004). I found another bug (infinite loop due to an error in
coq-back-to-indentation-prevline).
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq-indent.el | 24 | ||||
-rw-r--r-- | coq/ex-module.v | 35 | ||||
-rw-r--r-- | coq/example-x-symbols.v | 8 |
3 files changed, 35 insertions, 32 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 4849acae..3e720aad 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -84,11 +84,11 @@ (defun coq-find-command-start () - (proof-re-search-backward "\\.\\B\\|\\`") + (proof-re-search-backward "\\.\\s-\\|\\`") (while (and (proof-looking-at-syntactic-context) (> (point) (point-min))) - (proof-re-search-backward "\\.\\B\\|\\`")) - (if (proof-looking-at "\\.\\B") (forward-char 1)) + (proof-re-search-backward "\\.\\s-\\|\\`")) + (if (proof-looking-at "\\.\\s-") (forward-char 1)) (point) ) @@ -105,12 +105,13 @@ ) (defun coq-find-end () - (proof-re-search-forward "\\.\\B\\|\\'") + (proof-re-search-forward "\\.\\s-\\|\\.\\'\\|\\'") + (if (= (point) (+ (match-beginning 0) 2)) (backward-char 1)) (while (and (proof-looking-at-syntactic-context) (<= (point) (point-max))) (proof-re-search-forward "\\*\\s)") - (proof-re-search-forward "\\.\\B\\|\\'")) -; (backward-char 1) + (proof-re-search-forward "\\.\\s-\\|\\.\\'\\|\\'") + (if (= (point) (+ (match-beginning 0) 2)) (backward-char 1))) (point) ) @@ -136,6 +137,7 @@ ) (defun find-reg (lim reg) + (message "findreg") (let ((limit lim)) (if (< limit (point)) ;swap limit and point (let ((x limit)) (setq limit (point)) (goto-char x))) @@ -163,12 +165,12 @@ (setq topnotreached (= (forward-line -1) 0))) (back-to-indentation) (if (not topnotreached) 0 ; returns nil if top of buffer was reached - (if (find-reg oldpt "\\.\\B");; if we are at end of a command (dot) find this command + (if (find-reg oldpt "\\.\\s-\\|\\.\\'");; if we are at end of a command (dot) find this command (progn (coq-find-real-start) 1) (if (save-excursion - (coq-find-real-start) - (proof-looking-at-safe "Record") - (find-reg oldpt "{")) + (and (coq-find-real-start) + (proof-looking-at-safe "Record") + (find-reg oldpt "{"))) 4 2)) @@ -479,10 +481,12 @@ (defun coq-indent-offset () (let (kind prevcol prevpoint) + (message "ici") (save-excursion (setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert) prevcol (current-column) prevpoint (point))) + (message "la") (cond ((= kind 0) 0) ; top of the buffer reached ((= kind 1) ; we are at the command level diff --git a/coq/ex-module.v b/coq/ex-module.v index 240d0ad1..5b9d638a 100644 --- a/coq/ex-module.v +++ b/coq/ex-module.v @@ -72,26 +72,25 @@ Module Type N'. End N''. Declare Module N':M.SIG. (* no interactive def started *) - Declare Module N''':= N'. (* no interactive def started *) - Declare Module N''''. (* interactive def started *) - Parameter foo:nat. - End N''''. (* interactive def ended *) - End N'. + Declare Module N''':= N'. (* no interactive def started *) + Declare Module N''''. (* interactive def started *) + Parameter foo:nat. + End N''''. (* interactive def ended *) +End N'. - Lemma titi : O=O. - trivial. - Module Type K:=N'. - Module N''':=M. - Save. +Lemma titi : O=O. + trivial. + Module Type K:=N'. + Module N''':=M. +Save. - (* Here is a bug of Coq: *) - - Lemma bar:O=O. - Module Type L. (* This should not be allowed by Coq, since the End L. below fails *) - Axiom foo: O=O. - End L. (* fails --> if we go back to Module Type: unsync *) - Module I. - End I. + (* Here is a bug of Coq: *) +Lemma bar:O=O. + Module Type L. (* This should not be allowed by Coq, since the End L. below fails *) + Axiom foo: O=O. + End L. (* fails --> if we go back to Module Type: unsync *) + Module I. +End I. diff --git a/coq/example-x-symbols.v b/coq/example-x-symbols.v index 5b48a2f5..f890eab6 100644 --- a/coq/example-x-symbols.v +++ b/coq/example-x-symbols.v @@ -14,18 +14,18 @@ Fixpoint toto (x:nat) {struct x} : nat := (* nat should appear as |N *) end. Lemma titi : forall x:nat,x=x. (* symbolique for-all and nat *) - +Admitted. (* this should appear like foo'a'1_B_3 where a and B are greek *) Variable foo'alpha'1_beta_3 : Set. Fixpoint pow (n m:nat) {struct n} : nat := match n with - | O => 0 - | S p => m * pow p m + | O => 0 + | S p => m * pow p m end. -Notation "a ,{ b }" := (a - b) +Notation " a ,{ b } " := (a - b) (at level 1, no associativity). Notation "a ^^ b" := (pow a b) |