aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--coq/coq-smie.el76
-rw-r--r--coq/coq-system.el2
-rw-r--r--coq/ex/indent.v68
-rw-r--r--generic/proof-utils.el2
4 files changed, 97 insertions, 51 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 1c0b9c67..c488e73f 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -185,6 +185,32 @@ the token of \".\" is simply \".\"."
+;; A variant of smie-default-backward-token that recognize "." and ";"
+;; as single token even if glued at the end of another symbols.
+
+(defun coq-backward-token-fast-nogluing-dot-friends ()
+ (forward-comment (- (point)))
+ (let ((pt (point)))
+ (let* ((tok-punc (skip-syntax-backward "."))
+ (str-punc (buffer-substring-no-properties pt (point)))
+ (tok-other (if (zerop tok-punc) (skip-syntax-backward "w_'"))))
+ ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token
+ (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
+ (skip-syntax-forward ".")
+ (forward-char -1))
+ (buffer-substring-no-properties pt (point)))))
+
+(defun coq-forward-token-fast-nogluing-dot-friends ()
+ (forward-comment (point-max))
+ (let ((pt (point)))
+ (let* ((tok-punc (skip-syntax-forward "."))
+ (str-punc (buffer-substring-no-properties pt (point)))
+ (tok-other (if (zerop tok-punc) (skip-syntax-forward "w_'"))))
+ ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token
+ (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc))
+ (forward-char -1))
+ (buffer-substring-no-properties pt (point)))))
+
;; ignore-between is a description of pseudo delimiters of blocks that
;; should be jumped when searching. There is a bad interaction when
;; tokens and ignore-bteween are not disjoint
@@ -200,9 +226,7 @@ command (and inside parenthesis)."
(catch 'found
(while (< (point) end)
;; The default lexer is faster and is good enough for our needs.
- (let* ((next2 (smie-default-forward-token))
- (is-dot-friend (coq-dot-friend-p next2))
- (next (if is-dot-friend "." next2))
+ (let* ((next (coq-forward-token-fast-nogluing-dot-friends))
(parop (assoc next ignore-between)))
; if we find something to ignore, we directly jump to the
; corresponding closer
@@ -231,6 +255,7 @@ command (and inside parenthesis)."
((member next tokens) (throw 'found next))))))))
(scan-error nil)))
+
;; ignore-between is a description of pseudo delimiters of blocks that
;; should be jumped when searching. There is a bad interaction when
;; tokens and ignore-bteween are not disjoint
@@ -246,9 +271,7 @@ command (and inside parenthesis). "
(catch 'found
(while (> (point) end)
;; The default lexer is faster and is good enough for our needs.
- (let* ((next2 (smie-default-backward-token))
- (is-dot-friend (coq-dot-friend-p next2))
- (next (if is-dot-friend "." next2))
+ (let* ((next (coq-backward-token-fast-nogluing-dot-friends))
(parop (rassoc next ignore-between)))
; if we find something to ignore, we directly jump to the
; corresponding openner
@@ -266,8 +289,8 @@ command (and inside parenthesis). "
(goto-char (point))
next))
;; Do not consider "." when not followed by a space
- ;(message "SPACE?: %S , %S , %S" next2 next (looking-at ".[[:space:]]"))
- (when (or (not (equal next2 "."))
+ ;(message "SPACE?: %S , %S , %S" next next (looking-at ".[[:space:]]"))
+ (when (or (not (equal next "."))
(looking-at "\\.[[:space:]]"))
(cond
((and (zerop (length next))
@@ -350,7 +373,7 @@ The point should be at the beginning of the command name."
(defun coq-smie-forward-token ()
- (let ((tok (smie-default-forward-token)))
+ (let ((tok (coq-forward-token-fast-nogluing-dot-friends)))
(cond
;; @ may be ahead of an id, it is part of the id.
((and (equal tok "@") (looking-at "[[:alpha:]_]"))
@@ -372,7 +395,7 @@ The point should be at the beginning of the command name."
(concat tok newtok)))
(t (save-excursion (coq-smie-backward-token))))) ;; recursive call
((or (string-match coq-bullet-regexp-nospace tok)
- (member tok '("=>" ":=" "exists" "in" "as" "∀" "∃" "→" "∨" "∧" ";"
+ (member tok '("=>" ":=" "::=" "exists" "in" "as" "∀" "∃" "→" "∨" "∧" ";"
"," ":" "eval")))
;; The important lexer for indentation's performance is the backward
;; lexer, so for the forward lexer we delegate to the backward one when
@@ -427,6 +450,8 @@ The point should be at the beginning of the command name."
(goto-char (1+ (point))) "|}")
((member tok coq-smie-proof-end-tokens) "Proof End")
((member tok '("Obligation")) "Proof")
+ ;; FIXME: this case should be useless now that we replace
+ ;; smie-default-forward... by a smarter function.
((coq-dot-friend-p tok) ".")
;; Try to rely on backward-token for non empty tokens: bugs (hangs)
;; ((not (zerop (length tok))) (save-excursion (coq-smie-backward-token)))
@@ -552,7 +577,7 @@ The point should be at the beginning of the command name."
((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil))
": ltacconstr")
- ((equal tok ":=")
+ ((member tok '(":=" "::="))
(save-excursion
(save-excursion (coq-smie-:=-deambiguate))))
@@ -905,6 +930,21 @@ Typical values are 2 or 4."
;; | Leaf => add x d l
+;; Returns the column of the beginning of current atomic tactic (non
+;; composed). Returns the command start column if not found.
+(defun coq-find-with-related-backward()
+ (let ((cmd-start (save-excursion (coq-find-real-start))))
+ (save-excursion
+ ;; no point in going further the start of the command
+ ;; let us find a tactical between it and point
+ (let ((tok (coq-smie-search-token-backward '(";" "||" "|" "+") cmd-start)))
+ ;; hopefully we found the start of the current (non composed)tactic
+ ;; move point after the token found (if not found it will not move)
+ (forward-char (length tok))
+ (forward-comment (point-max)); skip spaces
+ ;; (coq-find-not-in-comment-forward "[^;+[:space:]|]")
+ (current-column)))))
+
(defun coq-is-at-first-line-of-def-decl ()
(let ((pt (point)))
(save-excursion
@@ -927,7 +967,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
(basic proof-indent)))
(:close-all t)
(:list-intro
- (or (member token '("fun" "forall" "quantif exists"))
+ (or (member token '("fun" "forall" "quantif exists" "with"))
;; We include "." in list-intro for the ". { .. } \n { .. }" so the
;; second {..} is aligned with the first rather than being indented as
;; if it were an argument to the first.
@@ -949,6 +989,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
2)
((equal token "with match") coq-match-indent)
+ ((equal token "with") 2) ; add 2 to the column of "with" in the children
;;; the ";" tactical ;;;
@@ -1010,6 +1051,12 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
; (smie-rule-parent 2)
; (smie-rule-parent)))
+ ;; "with" is also in the :list-intro rules and in :after.
+ ((equal token "with")
+ ;; Hack: We know that "with" is linked to the first word of
+ ;; the current atomic tactic. This tactic is the parent, not
+ ;; the "." of the previous command.
+ `(column . ,(+ 2 (coq-find-with-related-backward))))
((equal token "with module")
(if (smie-rule-parent-p "with module")
@@ -1037,11 +1084,6 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
(smie-rule-parent 4)))
-
-
-
-
-
;; This applies to forall located on the same line than "Lemma"
;; & co. This says that "if it *were* be on the beginning of
;; line" (which it is not) it would be indented of 2 wrt
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 0b9b6c58..aad7d386 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -658,4 +658,4 @@ then be set using local file variables."
"-emacs-U"))
coq-prog-name))))
-;;; coq-compile-common.el ends here
+;;; coq-system.el ends here
diff --git a/coq/ex/indent.v b/coq/ex/indent.v
index 27b64942..411347f0 100644
--- a/coq/ex/indent.v
+++ b/coq/ex/indent.v
@@ -60,26 +60,33 @@ Let xxx (* Precedence of "else" w.r.t "," and "->"! *)
3).
Module Y.
- Lemma L : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x.
+ Lemma L : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
Proof with auto with arith.
intros x.
induction x;simpl;intros...
Qed.
- Lemma L2 : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x.
+ Lemma L2 : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
Proof with auto with arith.
idtac.
(* "as" tactical *)
induction x
as
[ | x IHx].
- - auto with arith.
+ - cbn.
+ apply Nat.le_trans
+ with
+ (n:=0) (* aligning the different closes of a "with". *)
+ (m:=0)
+ (p:=0).
+ + auto with arith.
+ + auto with arith.
- simpl.
intros.
auto with arith.
Qed.
- Lemma L' : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x
- with L'' : forall x:nat , nat_iter x (A:=nat) (plus 2) 0 >= x.
+ Lemma L' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x
+ with L'' : forall x:nat , Nat.iter x (A:=nat) (plus 2) 0 >= x.
Proof with auto with arith.
- induction x;simpl;intros...
- induction x;simpl;intros...
@@ -249,32 +256,29 @@ Module X.
intros r.
{{
idtac;
- exists
- {|
- fld1:=r.(fld2);
- fld2:=r.(fld1);
- fld3:=false
- |}.
+ exists
+ {|
+ fld1:=r.(fld2);
+ fld2:=r.(fld1);
+ fld3:=false
+ |}.
(* ltac *)
match goal with
- | _:rec |- ?a /\ ?b => split
- | _ => fail
- end.
-
- match goal with
_:rec |- ?a /\ ?b => split
| _ => fail
end.
- lazymatch goal with
- _:rec |- ?a /\ ?b => split
- | _ => fail
- end.
+ Fail
+ lazymatch goal with
+ _:rec |- ?a /\ ?b => split
+ | _ => fail
+ end.
- multimatch goal with
- _:rec |- ?a /\ ?b => split
- | _ => fail
- end.
+ Fail
+ multimatch goal with
+ _:rec |- ?a /\ ?b => split
+ | _ => fail
+ end.
{ simpl. auto. }
{ simpl. auto. }}}
@@ -337,13 +341,13 @@ Section SET.
Fixpoint setVecProd (T : Type) (n : nat) (v1:Vector.t (set T) n) {struct v1}:
(Vector.t T n) -> Prop :=
match v1 with
- Vector.nil =>
+ Vector.nil _ =>
fun v2 =>
match v2 with
- Vector.nil => True
+ Vector.nil _ => True
| _ => False
end
- | (Vector.cons x n' v1') =>
+ | (Vector.cons _ x n' v1') =>
fun v2 =>
(* indentation of dependen "match" clause. *)
match v2
@@ -354,8 +358,8 @@ Section SET.
return
(Vector.t T (pred n'') -> Prop) -> Prop
with
- | Vector.nil => fun _ => False
- | (Vector.cons y n'' v2') => fun v2'' => (x y) /\ (v2'' v2')
+ | Vector.nil _ => fun _ => False
+ | (Vector.cons _ y n'' v2') => fun v2'' => (x y) /\ (v2'' v2')
end (setVecProd T n' v1')
end.
@@ -373,7 +377,7 @@ Module curlybracesatend.
reflexivity. }
exists (S (S n)).
simpl.
- rewrite NPeano.Nat.add_1_r.
+ rewrite Nat.add_1_r.
reflexivity.
Qed.
@@ -388,7 +392,7 @@ Module curlybracesatend.
exists (S (S n)).
simpl.
- rewrite NPeano.Nat.add_1_r.
+ rewrite Nat.add_1_r.
reflexivity.
Qed.
@@ -402,7 +406,7 @@ Module curlybracesatend.
reflexivity. } {
exists (S (S n)).
simpl.
- rewrite NPeano.Nat.add_1_r.
+ rewrite Nat.add_1_r.
reflexivity. }
}
idtac.
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 75ddbf69..dff19e76 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -411,7 +411,7 @@ or if the window is the only window of its frame."
;; weird test cases:
;; cur=45, max=23, desired=121, extraline=0
;; current height
- ;;; ((cur-height (window-height window))
+ ;;; (cur-height (window-height window))
;; Most window is allowed to grow to
((max-height
(/ (frame-height (window-frame window))
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 07:36:23 +0000