diff options
| -rw-r--r-- | CHANGES | 35 | ||||
| -rw-r--r-- | coq/coq-smie-lexer.el | 44 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 2 |
3 files changed, 51 insertions, 30 deletions
@@ -29,10 +29,32 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. *** Support proof-tree visualization -*** Indentation improvements using SMIE - Still experimental. +*** New commands for Print/Check/About/Show with "Printing All" flag + Avoids typing "Printing All" in the buffer. See the menu Coq > + Other queries. Thanks to Assia Mahboubi and Frederic Chyzak for + the suggestion. + Shortcut: add C-u before the usual shortcut + (example: C-u C-c C-a C-c for: + Set Printing All. + Check. + Unset Printing All. ) + +*** Coq menu visible in Response and goals buffers. + Shortcuts available too (Check, Print etc.) in response and goals + buffers. + +*** Tooltips hidden by default + Flickering when hovering commands is off by default! -**** Limitations: +*** "Insert Requires" now uses completion based on coq-load-path + +*** New setting for hiding additional goals from the *goals* buffer + Coq > Settings > Hide additional subgoals + +*** Indentation improvements using SMIE. Supporting bullets and { }. + Still experimental. Please submit bugs. + +**** Limitations of indentation: ***** hard-wired precedence between bullets: - < + < * example: @@ -51,12 +73,7 @@ the CVS ChangeLog and PG Trac, http://proofgeneral.inf.ed.ac.uk/trac. always introduce a proof with "Proof." (or "Next Obligation"). *** Minor parsing fixes - -*** New setting for hiding additional goals from the *goals* buffer - -*** New commands for Print/Check/Show with Printing All flag - -*** "Insert Requires" now uses completion based on coq-load-path +*** Windows resizing fixed ** HOL Light [WORK IN PROGRESS] diff --git a/coq/coq-smie-lexer.el b/coq/coq-smie-lexer.el index a87beb82..c40adda8 100644 --- a/coq/coq-smie-lexer.el +++ b/coq/coq-smie-lexer.el @@ -14,20 +14,23 @@ ;; - We identify the different types of bullets (First approximation). ;; - We distinguish "with match" from other "with". -(setq coq-smie-dot-friends '("*." "-*." "|-*." "*|-*.")) +(require 'coq-indent) +(require 'smie) + +(defconst coq-smie-dot-friends '("*." "-*." "|-*." "*|-*.")) ; for debuging (defun coq-time-indent () (interactive) - (let ((deb (time-to-seconds))) + (let ((deb (float-time))) (smie-indent-line) - (message "time: %S"(- (time-to-seconds) deb)))) + (message "time: %S"(- (float-time) deb)))) (defun coq-time-indent-region (beg end) (interactive "r") - (let ((deb (time-to-seconds))) + (let ((deb (float-time))) (indent-region beg end nil) - (message "time: %S"(- (time-to-seconds) deb)))) + (message "time: %S"(- (float-time) deb)))) @@ -131,9 +134,9 @@ command (and inside parenthesis)." (coq-smie-search-token-forward (append parops (cons "." nil)) end ignore-between) - (cons "." nil))) ;coq-smie-dot-friends + (cons "." nil)) ;coq-smie-dot-friends (goto-char (point)) - next) + next)) ;; Do not consider "." when not followed by a space (when (or (not (equal next ".")) (looking-at "[[:space:]]")) @@ -656,18 +659,19 @@ Lemma foo: forall n, ; To show the bug. Comment this and then try to indent the following: ; Module X. ; Module Y. <-- here --> Error: (wrong-type-argument integer-or-marker-p nil) -(defun smie-indent--parent () - (or smie--parent - (save-excursion - (let* ((pos (point)) - (tok (funcall smie-forward-token-function))) - (unless (numberp (cadr (assoc tok smie-grammar))) - (goto-char pos)) - (setq smie--parent - (or (smie-backward-sexp 'halfsexp) - (let (res) - (while (null (setq res (smie-backward-sexp)))) - (list nil (point) (nth 2 res))))))))) +; No need anymore? +;; (defun smie-indent--parent () +;; (or smie--parent +;; (save-excursion +;; (let* ((pos (point)) +;; (tok (funcall smie-forward-token-function))) +;; (unless (numberp (cadr (assoc tok smie-grammar))) +;; (goto-char pos)) +;; (setq smie--parent +;; (or (smie-backward-sexp 'halfsexp) +;; (let (res) +;; (while (null (setq res (smie-backward-sexp)))) +;; (list nil (point) (nth 2 res))))))))) (defun coq-smie-rules (kind token) "Indentation rules for Coq. See `smie-rules-function'. @@ -775,4 +779,4 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." -(provide 'coq-smie-lexer)
\ No newline at end of file +(provide 'coq-smie-lexer) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 2030d141..5d80c114 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -328,7 +328,7 @@ "Coq tactic(al)s that solve a subgoal." ) -(setq develock-coq-font-lock-keywords +(defvar develock-coq-font-lock-keywords '((develock-find-long-lines (1 'develock-long-line-1 t) (2 'develock-long-line-2 t)) |