diff options
| -rw-r--r-- | coq/coq-syntax.el | 14 | ||||
| -rw-r--r-- | coq/coq.el | 34 |
2 files changed, 44 insertions, 4 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 7f518615..7317eae6 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1079,6 +1079,14 @@ It is used: ;; Remove spurious variable and function faces on commas. '(proof-zap-commas)))) + +;; ", " is for multiple hypothesis diplayed in v8.5. If more than +;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5) +;; "^ " is for goals in debug mode. +(defvar coq-hyp-name-in-goal-or-response-regexp + "\\(^\\|^ \\|^ \\|[^^ ] ? \\)\\(\\(?:[^\n :(),=]\\|, \\|,$\\)+ *\\(?:: \\|,$\\)\\)" + "regexp matching hypothesis names in goal or response buffer") + ;; We define a slightly different set of keywords for response buffer. (defvar coq-response-font-lock-keywords @@ -1092,9 +1100,7 @@ It is used: (cons (proof-regexp-alt-list-symb (list "In environment" "The term" "has type")) 'proof-error-face) (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face) (list (concat "[?]" coq-id) 0 'proof-eager-annotation-face);; highlight evars - ;; ", " is for multiple hypothesis diplayed in v8.5. If more than - ;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5) - (cons "\\(^\\| \\) \\{0,1,2\\}\\([^\n :(),]\\|, \\)+ *:" 'proof-declaration-name-face) + (list coq-hyp-name-in-goal-or-response-regexp 2 'proof-declaration-name-face) (list "^\\([^ \n]+\\) \\(is defined\\)" (list 1 'font-lock-function-name-face t))))) (defvar coq-goals-font-lock-keywords @@ -1103,7 +1109,7 @@ It is used: (list (cons coq-reserved-regexp 'font-lock-type-face) (list (concat "[?]" coq-id) 0 'proof-eager-annotation-face);; highlight evars - (cons "\\(^\\| \\) \\{0,2\\}\\([^ \n:()=]\\|, \\)+ *:" 'proof-declaration-name-face) + (list coq-hyp-name-in-goal-or-response-regexp 2 'proof-declaration-name-face) (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)))) @@ -1522,6 +1522,40 @@ Near here means PT is either inside or just aside of a comment." (cm-prefix (match-string 2))) (concat (make-string (length cm-start) ? ) cm-prefix))))) + + +;;;;;;;;;;;;;;;;;;;;;;;attempt to deal with debug mode ;;;;;;;;;;;;;;;; + +;; tries to extract the last debug goal and display it in goals buffer +(defun coq-display-debug-goal () + (interactive) + (with-current-buffer proof-shell-buffer + (let ((pt (progn (save-excursion (forward-line -1) (point))))) + (message "DERIVE: %S %S" (point) pt) + (save-excursion + (re-search-backward "^TcDebug" pt t) + (re-search-backward "<infomsg>\\|^TcDebug\\|^</prompt>" nil t) + (when (looking-at "<infomsg>") + (let ((pt2 (point))) + (re-search-backward "Goal:\\|^TcDebug\\|^</prompt>" nil t) + (when (looking-at "Goal") + (pg-goals-display (buffer-substring (point) pt2) nil)))))))) + +;; overwrite the generic one, interactive prompt is Debug mode;; try to display +;; the debug goal in the goals buffer. +(defun proof-shell-process-interactive-prompt-regexp () + "Action taken when `proof-shell-interactive-prompt-regexp' is observed." + (when (and (proof-shell-live-buffer) + ; not already visible + t) + (switch-to-buffer proof-shell-buffer) + (coq-display-debug-goal) + (message "Prover expects input in %s buffer (if debug mode: h<return> for help))" proof-shell-buffer))) + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + + (defun coq-mode-config () ;; SMIE needs this. (set (make-local-variable 'parse-sexp-ignore-comments) t) |