diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-indent.el | 6 | ||||
| -rw-r--r-- | coq/coq.el | 10 |
2 files changed, 9 insertions, 7 deletions
diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 3e720aad..adac6527 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -364,8 +364,8 @@ ;; previous line of previous line. ;; prevcol is the indentation column of the previous line, prevpoint -;; is the indetation point of previous line, record tells if we are -;; inside a the accolades of a record. +;; is the indentation point of previous line, record tells if we are +;; inside the accolades of a record. (defun coq-indent-expr-offset (kind prevcol prevpoint record) "Returns the indentation column of the current line. This function indents a *expression* line (a line inside of a command). Use `coq-indent-command-offset' to indent a line belonging to a command. The fourth argument must be t if inside the {}s of a record, nil otherwise." @@ -481,12 +481,10 @@ (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 @@ -6,7 +6,7 @@ ;; $Id$ (require 'proof) -(require 'holes) ; in generic directory +(require 'holes-load) ; in lib directory ;; coq-syntaxe is required below ;; ----- coq-shell configuration options @@ -369,6 +369,7 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no ;;go to next span (setq span (next-span span 'type)) ) + ;;let's build the backtrack command now: (let (last-staten) (setq last-staten (coq-last-statenum-safe)) (setq ans @@ -797,6 +798,8 @@ Based on idea mentioned in Coq reference manual." ;; font-lock (setq font-lock-keywords coq-font-lock-keywords-1) + ;;holes + (holes-mode 1) (proof-config-done) @@ -815,7 +818,6 @@ Based on idea mentioned in Coq reference manual." tag-table-alist))) (setq blink-matching-paren-dont-ignore-comments t) - ;; multiple file handling (setq proof-cannot-reopen-processed-files t ;; proof-shell-inform-file-retracted-cmd 'coq-retract-file @@ -867,7 +869,7 @@ Based on idea mentioned in Coq reference manual." (coq-init-syntax-table) (setq font-lock-keywords coq-font-lock-keywords-1) - + (holes-mode 1) (proof-shell-config-done)) (defun coq-goals-mode-config () @@ -875,11 +877,13 @@ Based on idea mentioned in Coq reference manual." (setq pg-goals-error-regexp coq-error-regexp) (coq-init-syntax-table) (setq font-lock-keywords coq-font-lock-keywords-1) + (holes-mode 1) (proof-goals-config-done)) (defun coq-response-config () (coq-init-syntax-table) (setq font-lock-keywords coq-font-lock-keywords-1) + (holes-mode 1) (proof-response-config-done)) |