diff options
| -rw-r--r-- | coq-fontlock.el | 20 | ||||
| -rw-r--r-- | coq.el | 36 |
2 files changed, 38 insertions, 18 deletions
diff --git a/coq-fontlock.el b/coq-fontlock.el index 03b56242..81d2a1c7 100644 --- a/coq-fontlock.el +++ b/coq-fontlock.el @@ -4,6 +4,10 @@ ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> ;; $Log$ +;; Revision 1.8 1998/01/15 13:30:17 hhg +;; Added coq-shell-cd +;; Some new fontlocks +;; ;; Revision 1.7 1997/11/26 17:12:55 hhg ;; Incorporated tms's suggestion for simplifying coq-font-lock-keywords-1 ;; @@ -84,10 +88,12 @@ "Eval" "Extraction" "Focus" +"Immediate" "Hint" "Infix" "Opaque" "Print" +"Proof" "Pwd" "Reset" "Search" @@ -197,20 +203,22 @@ coq-id ")\\)?") 'font-lock-type-face)) "*Font-lock table for Coq terms.") -;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore, -;; it might be safer to append "\\s-*:". (defconst coq-save-command-regexp (concat "^" (ids-to-regexp coq-keywords-save))) (defconst coq-save-with-hole-regexp - (concat "\\(" (ids-to-regexp coq-keywords-save) "\\)\\s-+\\([^.]+\\)")) + (concat "\\(" (ids-to-regexp coq-keywords-save) + "\\)\\s-+\\(" coq-id "\\)\\s-*\.")) (defconst coq-goal-command-regexp (concat "^" (ids-to-regexp coq-keywords-goal))) (defconst coq-goal-with-hole-regexp - (concat "\\(" (ids-to-regexp coq-keywords-goal) "\\)\\s-+\\([^:]+\\)")) + (concat "\\(" (ids-to-regexp coq-keywords-goal) + "\\)\\s-+\\(" coq-id "\\)\\s-*:")) (defconst coq-decl-with-hole-regexp - (concat "\\(" (ids-to-regexp coq-keywords-decl) "\\)\\s-*\\([^:]+\\)")) + (concat "\\(" (ids-to-regexp coq-keywords-decl) + "\\)\\s-*\\(" coq-id "\\)\\s-*:")) (defconst coq-defn-with-hole-regexp - (concat "\\(" (ids-to-regexp coq-keywords-defn) "\\)\\s-*\\([^:]+\\)")) + (concat "\\(" (ids-to-regexp coq-keywords-defn) + "\\)\\s-*\\(" coq-id "\\)\\s-*[:[]")) (defvar coq-font-lock-keywords-1 (append @@ -3,6 +3,10 @@ ;; Author: Healfdene Goguen and Thomas Kleymann ;; $Log$ +;; Revision 1.14 1998/01/15 13:30:18 hhg +;; Added coq-shell-cd +;; Some new fontlocks +;; ;; Revision 1.13 1997/11/26 17:23:51 hhg ;; Added C-c C-s to run "Search" in Coq. ;; Moved coq-goal-with-hole-regexp etc to coq-fontlock. @@ -70,10 +74,13 @@ ; Configuration +(defvar proof-shell-cd "Cd \"%s\"" + "*Command of the inferior process to change the directory.") + (defconst coq-mode-version-string "Coq-MODE. ALPHA Version 1.11 (June 1996) LEGO Team <lego@dcs.ed.ac.uk>") -(defvar coq-tags "/net/pauillac/constr/V6.2/theories/TAGS" +(defvar coq-tags "/obj/local/coq/V6.1.beta/theories/TAGS" "the default TAGS table for the Coq library") (defconst coq-process-config "" @@ -107,6 +114,9 @@ (defvar coq-shell-prompt-pattern (concat "^" proof-id " < ") "*The prompt pattern for the inferior shell running coq.") +(defvar coq-shell-cd "Cd \"%s\"." + "*Command of the inferior process to change the directory.") + (defvar coq-shell-abort-goal-regexp "Current goal aborted" "*Regular expression indicating that the proof of the current goal has been abandoned.") @@ -114,18 +124,17 @@ (defvar coq-shell-proof-completed-regexp "Subtree proved!" "*Regular expression indicating that the proof has been completed.") -;; ----- outline - (defvar coq-goal-regexp "\\(============================\\)\\|\\(subgoal [0-9]+ is:\\)\n") +;; ----- outline + (defvar coq-outline-regexp - (concat "[[*]\\|" - (ids-to-regexp - '("Discharge" "DischargeKeep" "Freeze" "$?Goal" "Module" "Record" "Inductive" - "Unfreeze")))) + (ids-to-regexp + '("Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" + "Remark" "Record" "Inductive" "Definition"))) -(defvar coq-outline-heading-end-regexp ";\\|\\*)") +(defvar coq-outline-heading-end-regexp "\.\\|\\*)") (defvar coq-shell-outline-regexp coq-goal-regexp) (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) @@ -346,6 +355,7 @@ (interactive) (insert "Apply ")) +<<<<<<< coq.el (defun coq-Search () "Search for type in goals." (interactive) @@ -436,7 +446,8 @@ (interactive) (save-excursion (beginning-of-line) - (if (< (point) (proof-locked-end)) + (if (and (< (point) (proof-locked-end)) + (eq proof-script-buffer (current-buffer))) (error "can't indent locked region!")) (let* ((state (coq-parse-to-point)) (beg (point)) @@ -454,7 +465,8 @@ (save-excursion (goto-char start) (beginning-of-line) - (if (< (point) (proof-locked-end)) + (if (and (< (point) (proof-locked-end)) + (eq proof-script-buffer (current-buffer))) (error "can't indent locked region!")) (let* ((beg (point)) (state (coq-parse-to-point)) @@ -578,7 +590,7 @@ ;; Info (setq Info-directory-list - (cons "/home/hhg/src/info" Info-directory-list)) + (cons "/home/hhg/src/doc/info" Info-directory-list)) ;; keymaps and menus (easy-menu-add coq-mode-menu coq-mode-map) @@ -594,7 +606,7 @@ (defun coq-shell-mode-config () (setq proof-shell-prompt-pattern coq-shell-prompt-pattern - proof-shell-abort-goal-regexp coq-shell-abort-goal-regexp + proof-shell-cd coq-shell-cd proof-shell-proof-completed-regexp coq-shell-proof-completed-regexp proof-shell-error-regexp coq-error-regexp proof-shell-interrupt-regexp coq-interrupt-regexp |