diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2006-08-21 07:50:05 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2006-08-21 07:50:05 +0000 |
commit | 933112fcc5c21c816649ded7cff3564d407ab9d5 (patch) | |
tree | c969192a08d7851e24d37513a9a06a6e4f067b46 /coq | |
parent | b40cca6bde4d432934bdd6e38d7e7454f6e9ca5f (diff) |
Started the coq-insert-tactic.
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq-abbrev.el | 25 | ||||
-rw-r--r-- | coq/coq-local-vars.el | 68 | ||||
-rw-r--r-- | coq/coq-syntax.el | 3 | ||||
-rw-r--r-- | coq/coq.el | 78 |
4 files changed, 108 insertions, 66 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 19b2ac44..4b74b2b5 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -141,7 +141,7 @@ ("s" "simpl" holes-abbrev-complete 23) ("set" "set ( # := #)" holes-abbrev-complete 23) ("seth" "set ( # := #) in * |-" holes-abbrev-complete 23) - ("setg" "set ( # := #) in |-*" holes-abbrev-complete 23) + ("setg" "set ( # := #) in |- *" holes-abbrev-complete 23) ("seti" "set ( # := #) in #" holes-abbrev-complete 23) ("su" "subst #" holes-abbrev-complete 23) ("sc" "Scheme @{name} := Induction for # Sort #." nil 0) @@ -190,7 +190,7 @@ ["Print Scope/Visibility..." coq-PrintScope t] ) ["Smart intros" coq-intros t] - ["Require/Export/Import" coq-insert-requires t] + ["Require/Export/Import..." coq-insert-requires t] ("INSERT COMMAND" "COMMAND ABBREVIATION" ["Definition def<C-BS>" (holes-insert-and-expand "def") t] @@ -204,23 +204,8 @@ ["Inductive4 indv4<C-BS>" (holes-insert-and-expand "indv4") t] "" ["Section/Module (interactive)..." coq-insert-section-or-module t] - ["Require/Export/Import" coq-insert-requires t] + ["Require/Export/Import (interactive)..." coq-insert-requires t] "" - ("Modules" - "COMMAND ABBREVIATION" - ["Module (interactive)... " coq-insert-section-or-module t] - ["Module mo<C-BS>" (holes-insert-and-expand "mo") t] - ["Module (<:) mo2<C-BS>" (holes-insert-and-expand "mo") t] -; ["Module (interactive) moi<C-BS>" (holes-insert-and-expand "moi") t] -; ["Module (interactive <:) moi2<C-BS>" (holes-insert-and-expand "moi2") t] - ["Module Type mt<C-BS>" (holes-insert-and-expand "mt") t] -; ["Module Type (interactive) mti<C-BS>" (holes-insert-and-expand "mti") t] -; "" - ["Declare Module dm<C-BS>" (holes-insert-and-expand "dm") t] - ["Declare Module (<:) dm2<C-BS>" (holes-insert-and-expand "dm") t] -; ["Declare Module (inter.) dmi<C-BS>" (holes-insert-and-expand "dmi") t] -; ["Declare Module (inter. <:) dmi2<C-BS>" (holes-insert-and-expand "dmi2") t] - ) ("Hints" "COMMAND ABBREVIATION" ["Hint Constructors hc<C-BS>" (holes-insert-and-expand "hc") t] @@ -248,8 +233,8 @@ ["Set Printing All sprall<C-BS>" (holes-insert-and-expand "sprall") t] ["Unset Printing All unsprall<C-BS>" (holes-insert-and-expand "unsprall") t] "" - ["Print Scope/Visibility..." coq-PrintScope t] - ["Locate..." coq-LocateNotation t] + ["Print Scope/Visibility (interactive)..." coq-PrintScope t] + ["Locate (interactive)..." coq-LocateNotation t] "" ["Infix inf<C-BS>" (holes-insert-and-expand "inf") t] diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index f10ef6f1..4c51b2de 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.el @@ -80,35 +80,57 @@ launched on this file." ) -(defun coq-ask-build-addpath-option () +(defun coq-read-directory (prompt) "Ask for and return a directory name." (let* - ;; read-file-name here because it is convenient to see .v files when selecting - ;; directories to add to the path - ((path (read-file-name "library path to add (empty to stop) : " - "" "" t))) - (if (and (string-match " " path) - (not (y-or-n-p "The path contains spaces, are you sure? (y or n) :"))) - (coq-ask-build-addpath-option) ; retry - path))) - -(defun coq-ask-prog-args () + ;; read-file-name here because it is convenient to see .v files + ;; when selecting directories to add to the path. Moreover + ;; read-directory-name does not seem to exist in fsf emacs?? + ((path (read-file-name prompt "" "" t))) + path)) + +;(read-from-minibuffer +; PROMPT &optional INITIAL-CONTENTS KEYMAP READP HISTORY ABBREV-TABLE DEFAULT) +;(read-directory-name +; PROMPT &optional DIR DEFAULT MUST-MATCH INITIAL-CONTENTS HISTORY) + +(defun coq-extract-directories-from-args (args) + (if (not args) () + (let ((hd (car args)) (tl (cdr args))) + (cond + ((string-equal hd "-I") + (cond + ((not tl) nil) + ; if the option following -I starts with '-', forget the -I : + ((char-equal ?- (string-to-char (car tl))) + (coq-extract-directories-from-args tl)) + (t (cons (car tl) (coq-extract-directories-from-args (cdr tl)))))) + (t (coq-extract-directories-from-args tl)))))) + + +(defun coq-ask-prog-args (&optional oldvalue) "Ask for and return the information to put into variables coq-prog-args. These variable describes the coqtop arguments to be launched on this file." - (let ((progargs '("-emacs")) - (option (coq-ask-build-addpath-option))) - (message "progargs = %s" progargs) + (let* ((olddirs (coq-extract-directories-from-args oldvalue)) + (progargs '("-emacs")) + (option)) + ;; first suggest preious directories + (while olddirs + (if (y-or-n-p (format "keep the directory %s?" (car olddirs))) + (setq progargs (cons (car olddirs) (cons "-I" progargs)))) + (setq olddirs (cdr olddirs))) + ;; then ask for more + (setq option (coq-read-directory "Add directory (empty to stop) :")) (while (not (string-equal option "")) (setq progargs (cons option (cons "-I" progargs))) ;reversed - (message "progargs = %s" progargs) - (setq option (coq-ask-build-addpath-option))) - (message "progargs = %s" progargs) + (setq option (coq-read-directory "Add directory (empty to stop) -I :"))) (reverse progargs))) -(defun coq-ask-prog-name () +(defun coq-ask-prog-name (&optional oldvalue) "Ask for and return the local variables coq-prog-name. These variable describes the coqtop command to be launched on this file." - (let ((cmd (read-string "coq program name (default coqtop) : " "coqtop"))) + (let ((cmd (read-string "coq program name (default coqtop) : " + (or oldvalue "coqtop")))) (if (and (string-match " " cmd) (not (y-or-n-p "The prog name contains spaces, are you sure? (y or n) :"))) @@ -120,12 +142,16 @@ These variable describes the coqtop command to be launched on this file." "Ask for and insert the local variables coq-prog-name and coq-prog-args. These variables describe the coqtop command to be launched on this file." (interactive) - (let ((progname (coq-ask-prog-name)) - (progargs (coq-ask-prog-args))) + (let* ((oldname (local-vars-list-get-safe 'coq-prog-name)) + (oldargs (local-vars-list-get-safe 'coq-prog-args)) + (progname (coq-ask-prog-name oldname)) + (progargs (coq-ask-prog-args oldargs))) (coq-insert-coq-prog-name progname progargs) (setq coq-prog-name progname) (setq coq-prog-args progargs))) + + (provide 'coq-local-vars) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index c3402ecb..30f4a86a 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -443,7 +443,8 @@ Print and Check commands, put the following line in your .emacs: "All commands keyword.") (defvar coq-tacticals - '("abstract" + '("info" "solve" "first" + "abstract" "do" "idtac" ;; also in state-preserving-tactic "fail" @@ -182,6 +182,56 @@ To disable coqc being called (and use only make), set this to nil." ) +;;;;;;;;;;;;;;;;;;;;; +; defining a completion list for tactics +;;;;;;;;;;;;;;;;;;;;;; + +;(defun coq-assoc-from-list) + +;(defvar coq-tactics-completion-list +; (concat coq-tactics coq-tacticals)) + +(defvar coq-tactics-completion-list +; (concat + '( + ("autorewrite with" "autorewrite with @{db,db...}") + ("autorewrite in" "autorewrite in @{hyp}") + ("autorewrite with in" "autorewrite with @{db,db...} in @{hyp}") + ("autorewrite with using" "autorewrite with @{db,db...} using @{tac}") + ("autorewrite in using" "autorewrite in @{hyp} using @{tac}") + ("autorewrite with in using" "autorewrite with @{db,db...} in @{hyp} using @{tac}") + ("assert" "assert ( # : # )") + ("assert by" "assert ( # : # ) by #") + ("change in" "change # in #") + ("change with" "change # with") + ("change with in" "change # with # in #") + ("decompose" "decompose [#] @{hyp}") + ("auto" "auto with @{db}") + ("eauto" "eauto with @{db}") + ("functional induction" "functional induction @{f} @{args}") + ("pose" "pose ( # := # )") + ("replace with" "replace # with #") + ("rewrite <-" "rewrite <- #") + ("rewrite in" "rewrite # in #") + ("rewrite <- in" "rewrite <- # in #") + ("set" "set ( # := #)") + ("set in" "set ( # := #) in #") + ("set in |-" "set ( # := #) in # |- #") + ) +; coq-tactics coq-tacticals) + ) + + +(defun coq-insert-tactic () + (interactive) + (let* ((tac (completing-read "tactic (tab to see list, not exhaustive) : " + coq-tactics-completion-list)) + (s (cadr (assoc tac coq-tactics-completion-list))) + (pt (point))) + (insert s) + (holes-replace-string-by-holes-backward-jump pt))) + + ;; ----- outline @@ -802,15 +852,11 @@ This is specific to `coq-mode'." "Insert successive Intros commands with names given by Show Intros. Based on idea mentioned in Coq reference manual." (interactive) - (let* ((shints (proof-shell-invisible-cmd-get-result - "Show Intros.")) - (intros (replace-in-string shints "^\\([^\n]+\\)\n" "intros \\1.\n"))) - (proof-goto-end-of-locked) + (let* ((shints (proof-shell-invisible-cmd-get-result "Show Intros.")) + (replace-in-string shints "^\\([^\n]+\\)\n" "intros \\1.\n")) (unless (< (length shints) 2) ;; empty response is just NL - (newline) - (let ((start (point))) - (insert intros) - (indent-region start (point) nil))))) + (insert intros) + (indent-according-to-mode)))) (defun coq-match () "Insert a match expression from a type name by Show Intros. @@ -843,9 +889,6 @@ positions." ))))) -(proof-defshortcut coq-Apply "Apply " [(control ?a)]) - -;(proof-defshortcut coq-begin-Section "Section " [(control ?s)]) (define-key coq-keymap [(control ?i)] 'coq-intros) (define-key coq-keymap [(control ?s)] 'coq-insert-section-or-module) (define-key coq-keymap [(control ?r)] 'coq-insert-requires) @@ -859,20 +902,7 @@ positions." (define-key coq-keymap [(control ?l)] 'coq-LocateConstant) (define-key coq-keymap [(control ?n)] 'coq-LocateNotation) (define-key coq-keymap [(control ?g)] 'coq-Show) -;; da: I've moved this three buffer layout into the main code now, -;; making it default for three bufer mode. The function -;; `proof-layout-windows' lays out according to current display -;; mode: you can use this (C-c C-l) to do what binding below did. -;;(define-key coq-keymap [(control f3)] 'coq-three-b) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Indentation ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; FIXME mmw: code disabled; Is the new indentation scheme general -;; enough to handle Coq as well? -;; pc: no, this is now in coq-indent ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; To guess the command line options ;; |