Started the coq-insert-tactic.

6 files changed, 141 insertions, 88 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"
diff --git a/coq/coq.el b/coq/coq.el
index 3d9ea9ed..478deb19 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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   ;;
diff --git a/lib/holes.el b/lib/holes.el
index 3b182f19..529637bd 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -820,33 +820,44 @@ created.  Return the number of holes created."
 	  "to active hole.  C-h v holes-doc to see holes doc.")
   "Shortcut reminder string for jumping to active hole.")
 
+
+
+(defun holes-replace-string-by-holes-backward-jump (pos)
+  "Put holes between POS and point, backward, indenting.
+\"#\" and \"@{..}\" between this positions will become holes."
+  (save-excursion (indent-region pos (point) nil))
+  (let ((n (holes-replace-string-by-holes-backward pos)))
+    (case n
+      (0 nil)				; no hole, stay here.
+      (1
+       (goto-char pos)
+       (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
+      (t
+       (goto-char pos)
+       (message (substitute-command-keys
+		 "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc."))))))
+
+
+
 (defun holes-abbrev-complete ()
   "Complete abbrev by putting holes and indenting.
 Moves point at beginning of expanded text.  Put this function as
 call-back for your abbrevs, and just expanded \"#\" and \"@{..}\" will
 become holes."
-  (let ((pos last-abbrev-location))
-    (save-excursion (indent-region pos (point) nil))
-    (let ((n (holes-replace-string-by-holes-backward pos)))
-      (case n
-	(0 nil)				; no hole, stay here.
-	(1
-	 (goto-char pos)
-	 (holes-set-point-next-hole-destroy)) ; if only one hole, go to it.
-	(t
-	 (goto-char pos)
-	 (message (substitute-command-keys
-		   "\\[holes-set-point-next-hole-destroy] to jump to active hole.  \\[holes-short-doc] to see holes doc.")))))))
+  (holes-replace-string-by-holes-backward-jump last-abbrev-location))
+
+
 
 (defun holes-insert-and-expand (s)
   "Insert S, expand it and replace #s and @{]s by holes."
   ;; insert the expansion of abbrev s, and replace #s by holes.  It was
   ;; possible to implement it with a simple ((insert s) (expand-abbrev))
   ;; but undo would show the 2 steps, which is bad.
-  (let ((pos (point)))
-    (insert (abbrev-expansion s))
-    (let ((last-abbrev-location pos))
-      (holes-abbrev-complete))))
+  (let ((pos (point))
+	(ins (abbrev-expansion s)))
+    (insert (or ins s))
+    (setq last-abbrev-location pos)
+    (holes-abbrev-complete)))
 
 (defvar holes-mode nil
   "Is equal to t if holes mode is on, nil otherwise.")
diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el
index 7038ebf9..a79a870f 100644
--- a/lib/local-vars-list.el
+++ b/lib/local-vars-list.el
@@ -118,15 +118,10 @@ variable definition (or at the \"End:\" line)."
       (search-forward lpat eol)
       (re-search-forward "\\([^ :]+\\):" eol)
       (let ((varname (match-string 1)))
-	(message "varname = %s" varname)
 	(cond 
 	 ((string-equal varname "End") (setq endreached t) (beginning-of-line))
 	 ((string-equal varname symbname) (setq found t))
-	 (t (forward-line 1) (beginning-of-line))
-	 ))
-      (message "found %s" found)
-      (message "endreached %s" endreached)
-      )
+	 (t (forward-line 1) (beginning-of-line)))))
     (if found t nil)))
 
 
@@ -192,6 +187,11 @@ Raises an error if symb is not in the list."
       (beginning-of-line)
       (local-vars-list-get-current lpat rpat))))
 
+(defun local-vars-list-get-safe (symb)
+  "Return true if variable SYMB belongs to the local variable list of the current
+buffer."
+  (condition-case nil (local-vars-list-get symb) (error nil)))
+
 (defun local-vars-list-set (symb val)
   "Write the value val in the local variable list for variable symb.
 If the variable is already specified in the list, replace the value. If no local