diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | coq/coq-smie.el | 76 | ||||
| -rw-r--r-- | coq/coq-system.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 57 | ||||
| -rwxr-xr-x | coq/coqtags | 121 | ||||
| -rw-r--r-- | coq/ex/example-utf8.v | 9 | ||||
| -rw-r--r-- | coq/ex/indent.v | 68 | ||||
| -rw-r--r-- | easycrypt/easycrypt-keywords.el | 4 | ||||
| -rw-r--r-- | easycrypt/easycrypt.el | 1 | ||||
| -rw-r--r-- | generic/proof-config.el | 18 | ||||
| -rw-r--r-- | generic/proof-script.el | 7 | ||||
| -rw-r--r-- | generic/proof-shell.el | 16 | ||||
| -rw-r--r-- | generic/proof-utils.el | 2 |
14 files changed, 289 insertions, 100 deletions
@@ -12,6 +12,12 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac - Using query-replace (or replace-string) in the processed region doesn't wrongly jump to the first match anymore. +*** remove key-binding for proof-electric-terminator-toggle + - The default key-binding for proof-electric-terminator-toggle + (C-c .) was too easy to enter by mistake. And it was not that + useful as we can expect users to configure electric-terminator + once and for all. Hence the removal of this default key-binding. + ** Coq changes *** new menu Coq -> Auto Compilation for all background compilation options @@ -33,7 +33,7 @@ EMACS=$(shell if [ -z "`which emacs`" ]; then echo "Emacs executable not found"; PREFIX=$(DESTDIR)/usr DEST_PREFIX=$(DESTDIR)/usr -PROVERS=acl2 ccc coq hol98 isar lego hol-light phox pgshell pgocaml pghaskell +PROVERS=acl2 ccc coq easycrypt hol-light hol98 isar lego pghaskell pgocaml pgshell phox twelf OTHER_ELISP=generic lib contrib/mmm ELISP_DIRS=${PROVERS} ${OTHER_ELISP} ELISP_EXTRAS= 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 @@ -1218,6 +1218,17 @@ flag Printing All set." (remove-hook 'proof-assert-command-hook 'coq-adapt-printing-width) (remove-hook 'proof-retract-command-hook 'coq-reset-printing-width))) +;; In case of nested proofs (which are announced as obsolete in future versions +;; of coq) Coq does not show the goals of enclosing proof when closing a nested +;; proof. This is coq's proof-shell-empty-action-list-command function which +;; inserts a "Show" if the last command of an action list is a save command and +;; there is more than one open proof before that save. +(defun coq-empty-action-list-command (cmd) + (when (or (and (string-match coq-save-command-regexp-strict cmd) + (> (length coq-last-but-one-proofstack) 1)) + (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd) + (> (length coq-last-but-one-proofstack) 0))) + (list "Show."))) (defpacustom auto-adapt-printing-width t "If non-nil, adapt automatically printing width of goals window. @@ -1541,6 +1552,9 @@ Near here means PT is either inside or just aside of a comment." proof-goal-command "Goal %s. " proof-save-command "Save %s. " proof-find-theorems-command "Search %s. ") + + (setq proof-shell-empty-action-list-command 'coq-empty-action-list-command) + ;; FIXME da: Does Coq have a help or about command? ;; proof-info-command "Help" @@ -2659,27 +2673,28 @@ Only when three-buffer-mode is enabled." ;; https://github.com/cpitclaudel/company-coq/issues/8. (unless (memq 'no-response-display proof-shell-delayed-output-flags) ;; If there is no frame with goql+response then do nothing - (when (and proof-three-window-enable (coq-find-threeb-frames)) - (let ((pg-frame (car (coq-find-threeb-frames)))) ; selecting one adequat frame - (with-selected-frame pg-frame - (when (and (> (frame-height) 10) - (get-buffer-window proof-response-buffer)) - (let ((maxhgth - (- (+ (with-selected-window (get-buffer-window proof-goals-buffer t) (window-text-height)) - (with-selected-window (get-buffer-window proof-response-buffer t) (window-text-height))) - window-min-height)) - hgt-resp nline-resp) - (with-selected-window (get-buffer-window proof-response-buffer) - (setq hgt-resp (window-text-height)) - (with-current-buffer proof-response-buffer - (setq nline-resp ; number of lines we want for response buffer - (min maxhgth (max window-min-height ; + 1 for comfort - (+ 1 (count-lines (point-max) (point-min))))))) - (unless (is-not-split-vertic (selected-window)) - (shrink-window (- hgt-resp nline-resp))) - (with-current-buffer proof-response-buffer - (goto-char (point-min)) - (recenter)))))))))) + (when proof-three-window-enable + (let ((threeb-frames (coq-find-threeb-frames))) + (when threeb-frames + (let ((pg-frame (car threeb-frames))) ; selecting one adequate frame + (with-selected-frame pg-frame + (let ((response-window (get-buffer-window proof-response-buffer t)) + (goals-window (get-buffer-window proof-goals-buffer t))) + (when (and response-window + (> (frame-height) 10)) + (with-selected-window response-window + (with-current-buffer proof-response-buffer + (let* ((response-height (window-text-height response-window)) + (goals-height (window-text-height goals-window)) + (maxhgth (- (+ response-height goals-height) + window-min-height)) + (nline-resp ; number of lines we want for response buffer + (min maxhgth (max window-min-height ; + 1 for comfort + (+ 1 (count-lines (point-max) (point-min))))))) + (unless (is-not-split-vertic (selected-window)) + (shrink-window (- response-height nline-resp))) + (goto-char (point-min)) + (recenter))))))))))))) ;; TODO: remove/add hook instead? (defun coq-optimise-resp-windows-if-option () diff --git a/coq/coqtags b/coq/coqtags index 76b5bcc9..50d4a2f5 100755 --- a/coq/coqtags +++ b/coq/coqtags @@ -2,26 +2,27 @@ # # Or perhaps: /usr/local/bin/perl # -# # $Id$ # -undef $/; +undef $/; # undef input file separator; $_ gives the whole file if($#ARGV<$[) {die "No Files\n";} -open(tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; +open($tagfile,">TAGS") || die "Couldn't open TAGS: $!\n"; while(<>) { print "Tagging $ARGV\n"; - $a=$_; - $cp=1; - $lp=1; - $tagstring=""; + $a=$_; # read the whole file into $a + $cp=1; # emacs char number of the start of + # the current line + $lp=1; # line number + $tagstring=""; # accumulate all tags of one file here while(1) { # ---- Get the next statement starting on a newline ---- + # read over balanced comments if($a=~/^[ \t\n]*\(\*/) { while($a=~/^\s*\(\*/) { $d=1; $a=$'; $cp+=length $&; $lp+=(($wombat=$&)=~tr/\n/\n/); @@ -33,14 +34,18 @@ while(<>) } } + # skip remainder of a line after a comment or a statement if($cp>1 && $a=~/.*\n/) {$a=$'; $cp+=length $&; $lp++;} - while($a=~/^\n/) {$cp++;$lp++;$a=$'} + # skip white space lines + while($a=~/^[ \t]*\n/) {$cp+=length $&;$lp++;$a=$'} + # match the next statement if($a=~/^[^\.]*\./) { $stmt=$&; $newa=$'; $newcp=$cp+length $&; - $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); } + $newlp=$lp+(($wombat=$&)=~tr/\n/\n/); + } else { last;} # ---- The above embarrasses itself if there are semicolons inside comments @@ -48,20 +53,28 @@ while(<>) # print "----- (",$lp,",",$cp,")\n", $stmt, "\n"; - if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem))\s+([\w\']+))\s*:/) - { $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; } + if($stmt=~/^([ \t]*((Fact)|(Goal)|(Lemma)|(Remark)|(Theorem)|(Proposition)|(Corollary))\s+([\w\']+))\s*:/) + { $tagstring.=$1."\177".$10."\001".$lp.",".$cp."\n"; } elsif($stmt=~/^([ \t]*((Axiom)|(Hypothesis)|(Parameter)|(Variable))\s+[\w\']+)/) { adddecs($stmt,$1); } - elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive))\s+[\w\']+)/) - { $tagstring.=$1."\177".$6."\001".$lp.",".$cp."\n"; } + elsif($stmt=~/^([ \t]*((Definition)|(Fixpoint)|(Inductive)|(CoInductive)|(Record))\s+([\w\']+))/) + { + $tagstring.=$1."\177".$8."\001".$lp.",".$cp."\n"; + if($2 eq "Inductive" || $2 eq "CoInductive"){ + add_constructors($stmt); + } + elsif($2 eq "Record"){ + add_record_labels($stmt, $8); + } + } $cp=$newcp; $lp=$newlp; $a=$newa; } - print tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; + print $tagfile "\f\n".$ARGV.",".(length $tagstring)."\n".$tagstring; } -close tagfile; +close $tagfile; sub adddecs { $wk=$_[0]; @@ -71,3 +84,81 @@ sub adddecs { { $sep=$2; $tagstring.=$tag."\177".$1."\001".$lp.",".$cp."\n"; $wk=$'; } 0; } + +sub add_constructors { + my ($stmt) = @_; + my ($line, $tag); + my $current=0; + + # skip to the body of the inductive definition + # and match the first constructor + if($stmt=~/:=\s*(?:\|\s*)?([\w\']+)/gc){ + do { + $tag=$1; + $line=substr($stmt, $current, pos($stmt)-$current); + + # the previous match may span several lines + # need to remove all but the last line + if($line=~/^.*\n/s){ + $current+= length($&); + $cp+= length($&); + $lp+= (($wombat=$&)=~ tr/\n/\n/); + $line=substr($stmt, $current, pos($stmt)-$current); + } + + # print "C $tag in line $lp at $cp\n\tline: $line\n"; + $tagstring.=$line."\177".$tag."\001".$lp.",".$cp."\n"; + + # match now the next constructor + } while($stmt=~/\G.*?\|\s*([\w\']+)/sgc); + } +} + +sub add_record_labels { + my ($stmt, $record_name) = @_; + my ($line, $tag); + my $current=0; + + # skip to the body of the record and match the record constructor + if($stmt=~/:=\s*([\w\']+)?/gc){ + if(defined($1)){ + $tag=$1; + } else { + $tag="Build_".$record_name; + } + + $line=substr($stmt, $current, pos($stmt)-$current); + + # the previous match may span several lines + # need to remove all but the last line + if($line=~/^.*\n/s){ + $current+= length($&); + $cp+= length($&); + $lp+= (($wombat=$&)=~ tr/\n/\n/); + $line=substr($stmt, $current, pos($stmt)-$current); + } + + $tagstring.=$line."\177".$tag."\001".$lp.",".$cp."\n"; + + # match the first record label + if($stmt=~/\G\s*{\s*([\w\']+)/gc){ + do { + $tag=$1; + $line=substr($stmt, $current, pos($stmt)-$current); + + # the previous match may span several lines + # need to remove all but the last line + if($line=~/^.*\n/s){ + $current+= length($&); + $cp+= length($&); + $lp+= (($wombat=$&)=~ tr/\n/\n/); + $line=substr($stmt, $current, pos($stmt)-$current); + } + + $tagstring.=$line."\177".$tag."\001".$lp.",".$cp."\n"; + + # match now the next record label + } while($stmt=~/\G.*?;\s*([\w\']+)/sgc); + } + } +} diff --git a/coq/ex/example-utf8.v b/coq/ex/example-utf8.v index 4cba17c8..0f528f14 100644 --- a/coq/ex/example-utf8.v +++ b/coq/ex/example-utf8.v @@ -1,11 +1,6 @@ (* -*- coding: utf-8; -*- *) -(* utf8 notations: You can (re)use the version here, - or a compiled version distributed with Coq IDE: - Add LoadPath "/usr/lib/coq/ide". - Require Import utf8. -*) -Load "utf8". +Require Import Utf8. (* Printing of unicode notation, in *goals* *) Lemma test : ∀ A:Prop, A -> A. @@ -23,4 +18,4 @@ Qed. Check (fun (X:Set)(x:X) => x). (* Parsing of unicode notation here, printing in *response* *) -Check (∀A, A→A).
\ No newline at end of file +Check (∀A, A→A). 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/easycrypt/easycrypt-keywords.el b/easycrypt/easycrypt-keywords.el index 0bc10346..e0b9d369 100644 --- a/easycrypt/easycrypt-keywords.el +++ b/easycrypt/easycrypt-keywords.el @@ -5,7 +5,7 @@ ;; Distributed under the terms of the GPL-v3 license ;; -------------------------------------------------------------------- -; Generated on Thu Dec 17 16:14:05 2015 +; Generated on Tue Feb 21 23:37:34 2017 (defvar easycrypt-bytac-keywords '( "exact" @@ -43,6 +43,7 @@ "const" "op" "pred" + "inductive" "notation" "abbrev" "require" @@ -96,6 +97,7 @@ "hoare" "phoare" "islossless" + "async" )) (defvar easycrypt-tactic-keywords '( diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el index ecea9744..017b2563 100644 --- a/easycrypt/easycrypt.el +++ b/easycrypt/easycrypt.el @@ -61,7 +61,6 @@ this list are strings." ;; -------------------------------------------------------------------- (defun easycrypt-prog-args () - (message "%s" easycrypt-load-path) (append easycrypt-prog-args (easycrypt-include-options))) ;; -------------------------------------------------------------------- diff --git a/generic/proof-config.el b/generic/proof-config.el index 8ce53168..8bb40634 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1187,6 +1187,24 @@ If nil, use the whole of the output from the match on :type '(choice (const nil) regexp) :group 'proof-shell) +(defcustom proof-shell-empty-action-list-command nil + "A function returning a list of commands (strings) to be sent +to the prover when the last command in the queue has been +performed. Typically to ask for some informational +display (goals, etc). + +The function takes as argument the last command in the queue. + +NOTE 1: The commands will be tagged invisible, i.e. not related +to a place in the buffer. + +NOTE 2: The commands should NOT have any effect on the state of +the prover. Otherwise running the script outside pg would be +inconsistent." + :type 'function + :group 'proof-shell) + + (defcustom proof-shell-eager-annotation-start nil "Eager annotation field start. A regular expression or nil. An \"eager annotation indicates\" to Proof General that some following output diff --git a/generic/proof-script.el b/generic/proof-script.el index e67a7774..7d9afe22 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2565,9 +2565,10 @@ finish setup which depends on specific proof assistant configuration." ;; Additional key def for (first character of) terminal string (if proof-terminal-string (progn - (define-key proof-mode-map - (vconcat [(control c)] (vector (aref proof-terminal-string 0))) - 'proof-electric-terminator-toggle) +;; This key-binding was disabled following a request in PG issue #160. +;; (define-key proof-mode-map +;; (vconcat [(control c)] (vector (aref proof-terminal-string 0))) +;; 'proof-electric-terminator-toggle) (define-key proof-mode-map (vector (aref proof-terminal-string 0)) 'proof-electric-terminator))) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 13da8d98..51305eef 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1110,6 +1110,22 @@ contains only invisible elements for Prooftree synchronization." (setq cbitems (cons item (proof-shell-slurp-comments))) + ;; If proof-action-list is empty after removing the already + ;; processed actions and the last action was not already + ;; added by proof-shell-empty-action-list-command (prover + ;; specific), call it. + (when (and (null proof-action-list) + (not (memq 'empty-action-list flags))) + (let* ((cmd (mapconcat 'identity (nth 1 item) " ")) + (extra-cmds (apply proof-shell-empty-action-list-command (list cmd))) + ;; tag all new items with 'empty-action-list + (extra-items (mapcar (lambda (s) (proof-shell-action-list-item + s 'proof-done-invisible + (list 'invisible 'empty-action-list))) + extra-cmds))) + ;; action-list should be empty at this point + (setq proof-action-list (append extra-items proof-action-list)))) + ;; This is the point where old items have been removed from ;; proof-action-list and where the next item has not yet been ;; sent to the proof assistant. This is therefore one of the 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)) |