Added coq-shell-cd

Some new fontlocks

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
diff --git a/coq.el b/coq.el
index d445fceb..78655eb6 100644
--- a/coq.el
+++ b/coq.el
@@ -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