From aa910d291903d518325f3a74aaaffe13a1a38e29 Mon Sep 17 00:00:00 2001 From: Healfdene Goguen Date: Wed, 26 Nov 1997 17:23:51 +0000 Subject: Added C-c C-s to run "Search" in Coq. Moved coq-goal-with-hole-regexp etc to coq-fontlock. Removed various superfluous definitions for COQPATH etc. --- coq.el | 81 ++++++++++++++++-------------------------------------------------- 1 file changed, 19 insertions(+), 62 deletions(-) diff --git a/coq.el b/coq.el index ec27e86c..d445fceb 100644 --- a/coq.el +++ b/coq.el @@ -3,6 +3,11 @@ ;; Author: Healfdene Goguen and Thomas Kleymann ;; $Log$ +;; 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. +;; Removed various superfluous definitions for COQPATH etc. +;; ;; Revision 1.12 1997/11/24 19:15:08 djs ;; Added proof-execute-minibuffer-cmd and scripting minor mode. ;; @@ -71,10 +76,7 @@ (defvar coq-tags "/net/pauillac/constr/V6.2/theories/TAGS" "the default TAGS table for the Coq library") -(defconst coq-process-config -"AddPath \"/home/pauillac/formel/fguestb/src/coq/pbp\". -Add ML Path \"/home/pauillac/formel/fguestb/src/coq/pbp\". -Require Emacs." +(defconst coq-process-config "" "Command to configure pretty printing of the Coq process for emacs.") ;; This doesn't exist at the moment @@ -85,29 +87,6 @@ Require Emacs." (defconst coq-interrupt-regexp "Interrupted" "Regexp corresponding to an interrupt") -;; This doesn't exist at the moment -(defvar coq-test-all-name "test_all" - "The name of the Coq module which inherits all other modules of the - library.") - -;; Could be set to "Load". To cite Mark, "Although this may sound -;; strange at first side, the Make command is much, much slower for my -;; files then the load command. That is because .o files do not save -;; Equiv's. So a Make of a .o file needs to find the proper -;; conversions itself, and hence will be much slower in some -;; cases. Especially when doing larger examples." - -(defvar coq-make-command "Make") - -(defvar coq-path-name "COQPATH" - "The name of the environmental variable to search for modules. This - is used by \\{coqgrep} to find the files corresponding to a - search.") - -(defvar coq-path-separator ":" - "A character indicating how the items in the \\{coq-path-name} are - separated.") - (defvar coq-save-query t "*If non-nil, ask user for permission to save the current buffer before processing a module.") @@ -117,17 +96,6 @@ Require Emacs." (defvar coq-www-home-page "http://pauillac.inria.fr/coq/") -;; ----- coqstat and coqgrep, courtesy of Mark Ruys - -(defvar coqgrep-command (concat "coqgrep -n \"\" " coq-test-all-name) - "Last coqgrep command used in \\{coqgrep}; default for next coqgrep.") - -(defvar coqstat-command "coqstat -t") - -(defvar coqgrep-regexp-alist - '(("^\\([^:( \t\n]+\\)[:( \t]+\\([0-9]+\\)[:) \t]" 1 2 nil ("%s.l"))) - "Regexp used to match coqgrep hits. See `compilation-error-regexp-alist'.") - ;; ----- coq-shell configuration options (defvar coq-prog-name "coqtop" @@ -162,19 +130,10 @@ Require Emacs." (defvar coq-shell-outline-regexp coq-goal-regexp) (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) -(defvar coq-save-command-regexp - (concat "^" (ids-to-regexp coq-keywords-save))) -(defvar coq-save-with-hole-regexp - (concat "\\(" (ids-to-regexp coq-keywords-save) "\\)\\s-+\\([^.]+\\)")) -(defvar coq-goal-command-regexp - (concat "^" (ids-to-regexp coq-keywords-goal))) -(defvar coq-goal-with-hole-regexp - (concat "\\(" (ids-to-regexp coq-keywords-goal) "\\)\\s-+\\([^:]+\\)")) +(defconst coq-kill-goal-command "Abort.") +(defconst coq-forget-id-command "Reset ") -(defvar coq-kill-goal-command "Abort.") -(defvar coq-forget-id-command "Reset ") - -(defvar coq-undoable-commands-regexp (ids-to-regexp coq-tactics)) +(defconst coq-undoable-commands-regexp (ids-to-regexp coq-tactics)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Derived modes - they're here 'cos they define keymaps 'n stuff ;; @@ -244,13 +203,6 @@ Require Emacs." ;; Code that's coq specific ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(defun coq-get-path () - (let ((path-name (getenv coq-path-name))) - (cond ((not path-name) - (message "Warning: COQPATH has not been set!") - (setq path-name "."))) - (string-to-list path-name coq-path-separator))) - (defun coq-count-undos (sext) (let ((ct 0) str i) (while sext @@ -394,6 +346,14 @@ Require Emacs." (interactive) (insert "Apply ")) +(defun coq-Search () + "Search for type in goals." + (interactive) + (let (cmd) + (proof-check-process-available) + (setq cmd (read-string "Search Type: " nil 'proof-minibuffer-history)) + (proof-invisible-command (concat "Search " cmd proof-terminal-string)))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Indentation ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -598,6 +558,7 @@ Require Emacs." (define-key (current-local-map) [(control c) h] 'coq-help) (define-key (current-local-map) [(control c) I] 'coq-Intros) (define-key (current-local-map) [(control c) a] 'coq-Apply) + (define-key (current-local-map) [(control c) (control s)] 'coq-Search) (define-key (current-local-map) [tab] 'coq-indent-line) ;; outline @@ -617,11 +578,7 @@ Require Emacs." ;; Info (setq Info-directory-list - (cons "/home/pauillac/formel/fguestb/src/info" Info-directory-list)) - -;; where to find files - - (setq compilation-search-path (cons nil (coq-get-path))) + (cons "/home/hhg/src/info" Info-directory-list)) ;; keymaps and menus (easy-menu-add coq-mode-menu coq-mode-map) -- cgit v1.2.3