diff options
| -rw-r--r-- | coq/coq-abbrev.el | 6 | ||||
| -rw-r--r-- | coq/coq-smie-lexer.el | 15 | ||||
| -rw-r--r-- | coq/coq.el | 83 |
3 files changed, 96 insertions, 8 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 538ad5ec..c279e91b 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -89,12 +89,18 @@ ("OTHER QUERIES" ["Print Hint" coq-PrintHint t] ["Show ith goal..." coq-Show t] + ["Show ith goal... (show implicits)" coq-Show-with-implicits t] + ["Show ith goal... (show all)" coq-Show-with-all t] ["Show Tree" coq-show-tree t] ["Show Proof" coq-show-proof t] ["Show Conjectures" coq-show-conjectures t];; maybe not so useful with editing in PG? "" ["Print..." coq-Print t] + ["Print... (show implicits)" coq-Print-with-implicits t] + ["Print... (show all)" coq-Print-with-all t] ["Check..." coq-Check t] + ["Check (show implicits)..." coq-Check-show-implicits t] + ["Check (show all)..." coq-Check-show-all t] ["About..." coq-About t] ["Search..." coq-SearchConstant t] ["SearchRewrite..." coq-SearchRewrite t] diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el index 39fcdda9..a87beb82 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -121,7 +121,9 @@ command (and inside parenthesis)." ;; The default lexer is faster and is good enough for our needs. (let* ((next (smie-default-forward-token)) (parop (assoc next ignore-between))) - (if parop ; if we find something to ignore, we directly + ; if we find something to ignore, we directly jump to the + ; corresponding closer + (if parop (let ((parops ; corresponding matcher may be a list (if (listp parop) (cdr parop) (cons (cdr parop) nil)))) ; go to corresponding closer @@ -137,7 +139,8 @@ command (and inside parenthesis)." (looking-at "[[:space:]]")) (cond ((and (zerop (length next)) - (equal (char-syntax ?\)) (char-syntax (char-after)))) + (or (equal (point) (point-max)) ; protecting char-after next line + (equal (char-syntax ?\)) (char-syntax (char-after))))) (throw 'found nil)) ((zerop (length next)) ;; capture other characters than closing parent (forward-sexp 1)) @@ -162,8 +165,9 @@ command (and inside parenthesis). " (let* ((next2 (smie-default-backward-token)) (next (if (member next2 coq-smie-dot-friends) "." next2)) (parop (rassoc next ignore-between))) - ;(message "praop = %S" parop) - (if parop ; if we find something to ignore, we directly + ; if we find something to ignore, we directly jump to the + ; corresponding openner + (if parop (let ((p (point)) (parops ; corresponding matcher may be a list (if (listp (car parop)) (car parop) (cons (car parop) nil)))) @@ -181,7 +185,8 @@ command (and inside parenthesis). " (looking-at ".[[:space:]]")) (cond ((and (zerop (length next)) - (equal (char-syntax ?\() (char-syntax (char-before)))) + (or (equal (point) (point-min)) ; protecting char-before next line + (equal (char-syntax ?\() (char-syntax (char-before))))) (throw 'found nil)) ((zerop (length next)) (forward-sexp -1)) ((member next tokens) (throw 'found next)))))))) @@ -673,8 +673,55 @@ If locked span already has a state number, then do nothing. Also updates (proof-shell-ready-prover) (setq cmd (coq-guess-or-ask-for-string ask dontguess)) (proof-shell-invisible-command - (format (concat do " %s . ") (funcall postform cmd)))) - ) + (format (concat do " %s . ") (funcall postform cmd))))) + + +(defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd) + "Play commands SETCMD then CMD and then silently UNSETCMD." + (let* ((postform (if (eq postformatcmd nil) 'identity postformatcmd))) + (proof-shell-invisible-command + (format " %s . " (funcall postform setcmd)) 'wait) + (proof-shell-invisible-command + (format " %s . " (funcall postform cmd)) 'wait) + (proof-shell-invisible-command-invisible-result + (format " %s . " (funcall postform unsetcmd))))) + +(defun coq-ask-do-set-unset (ask do setcmd unsetcmd + &optional dontguess postformatcmd) + "Ask for an ident id and execute command DO in SETCMD mode. +More precisely it executes SETCMD, then DO id and finally silently UNSETCMD." + (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd))) + (proof-shell-ready-prover) + (setq cmd (coq-guess-or-ask-for-string ask dontguess)) + (coq-command-with-set-unset setcmd (concat do " " cmd) unsetcmd postformatcmd))) + + +(defun coq-ask-do-show-implicits (ask do &optional dontguess postformatcmd) + "Ask for an ident and print the corresponding term." + (coq-ask-do-set-unset ask do + "Set Printing Implicit" + "Unset Printing Implicit" + dontguess postformatcmd)) + +(defun coq-ask-do-show-all (ask do &optional dontguess postformatcmd) + "Ask for an ident and print the corresponding term." + (coq-ask-do-set-unset ask do + "Set Printing All" + "Unset Printing All" + dontguess postformatcmd)) + + + ;; (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd))) + + + ;; (proof-shell-ready-prover) + ;; (setq cmd (coq-guess-or-ask-for-string ask dontguess)) + ;; (coq-command-with-set-unset + ;; "Set Printing Implicit" + ;; (format (concat do " %s . ") cmd) + ;; "Unset Printing Implicit" ) + ;; )) + (defsubst coq-put-into-brackets (s) (concat "[ " s " ]")) @@ -715,6 +762,16 @@ This is specific to `coq-mode'." (interactive) (coq-ask-do "Print" "Print")) +(defun coq-Print-with-implicits () + "Ask for an ident and print the corresponding term." + (interactive) + (coq-ask-do-show-implicits "Print" "Print")) + +(defun coq-Print-with-all () + "Ask for an ident and print the corresponding term." + (interactive) + (coq-ask-do-show-all "Print" "Print")) + (defun coq-About () "Ask for an ident and print information on it." (interactive) @@ -761,11 +818,31 @@ This is specific to `coq-mode'." (interactive) (coq-ask-do "Check" "Check")) +(defun coq-Check-show-implicits () + "Ask for a term and print its type." + (interactive) + (coq-ask-do-show-implicits "Check" "Check")) + +(defun coq-Check-show-all () + "Ask for a term and print its type." + (interactive) + (coq-ask-do-show-all "Check" "Check")) + (defun coq-Show () "Ask for a number i and show the ith goal." (interactive) (coq-ask-do "Show goal number" "Show" t)) +(defun coq-Show-with-implicits () + "Ask for a number i and show the ith goal." + (interactive) + (coq-ask-do-show-implicits "Show goal number" "Show" t)) + +(defun coq-Show-with-all () + "Ask for a number i and show the ith goal." + (interactive) + (coq-ask-do-show-all "Show goal number" "Show" t)) + (proof-definvisible coq-PrintHint "Print Hint. ") @@ -2147,7 +2224,7 @@ Based on idea mentioned in Coq reference manual." (interactive) (add-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook) (proof-assert-next-command-interactive) - (remove-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook);as soone as possible + (remove-hook 'proof-shell-insert-hook 'coq-insert-infoH-hook);as soon as possible (proof-shell-wait) (let ((str (string-match "<info type=\"infoH\">\\([^<]*\\)</info>" |