Fixed a small bug in indentation of coq.

Fixed behavior for making abbrev table (don't if it already exists).

5 files changed, 27 insertions, 58 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index d8a53f47..164ac4a5 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -51,15 +51,18 @@
   (coq-build-abbrev-table-from-db coq-terms-db))
 
 
+
 ;;; The abbrev table built from keywords tables
 ;#s and @{..} are replaced by holes by holes-abbrev-complete
-(if (boundp 'holes-abbrev-complete)
-	 ()
+(if (and (boundp 'coq-mode-abbrev-table)
+	 (not (equal coq-mode-abbrev-table (make-abbrev-table)))) 
+    (message "Coq abbrevs already exists, default not loaded")    
+  (message "Coq default abbrevs loaded")
   (define-abbrev-table 'coq-mode-abbrev-table
-    (append coq-tactics-abbrev-table
-	    coq-tacticals-abbrev-table
-	    coq-commands-abbrev-table
-	    coq-terms-abbrev-table)))
+    (append coq-tactics-abbrev-table coq-tacticals-abbrev-table 
+	    coq-commands-abbrev-table coq-terms-abbrev-table))
+  ;if we use default coq abbrev, never ask to save it
+  (setq save-abbrevs nil))
 
 ;;;;;
 
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index 33656248..14205f03 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -196,46 +196,36 @@ is moved at the end of the match if found, at LIM otherwise."
         (while 
             (and (not pos)
                  (setq pos (proof-string-match reg (buffer-substring (point) limit))))
-;          (message "while body...")
           (forward-char (- (match-end 0) 1))          
           (when (save-excursion (forward-char -1)
                                 (proof-looking-at-syntactic-context))
             (setq pos nil))
-;          (message "while body... done")
           )
 ;        (message "find-reg... after while")
         (and pos (point))))))
 
 
 (defun coq-find-no-syntactic-on-line ()
-  (let ((bol (save-excursion (beginning-of-line) (point)))
-        (eol (save-excursion (end-of-line) (point))))
-    (beginning-of-line)
-    (back-to-indentation)
-    (while (and (or (coq-looking-at-syntactic-context)
-                    (is-at-a-space-or-tab))
-                    (not (eq (point) eol)))
-      (forward-char 1))
-    (not (eq (point) eol))))
-
-(defun coq-find-no-syntactic-on-line ()
+  "Return non-nil if there is a not commented non white character on the line.
+Moves point to this char or to the end of the line if not found (and return nil in
+this case)."
   (let ((bol (save-excursion (beginning-of-line) (point)))
         (eol (save-excursion (end-of-line) (point))))
     (back-to-indentation)
     (while (and (coq-looking-at-syntactic-context)
-                (re-search-forward coq-comment-end-regexp eol 'dummy)))
+                (re-search-forward coq-comment-end-regexp eol 'dummy))
+      (skip-chars-forward " \t"))
     (not (eq (point) eol))))
 
 
-;    (while (and (or (coq-looking-at-syntactic-context)
-;                    (is-at-a-space-or-tab))
-;                    (not (eq (point) eol)))
-;      (forward-char 1))
-;    (not (eq (point) eol))))
-
 
 (defun coq-back-to-indentation-prevline ()
-  "Moves point back to previous pertinent line for indentation. Move point to the first non white space character. Returns 0 if top of buffer was reached, 3 if inside a comment or string, 4 if inside the {} of a record, 1 if the line found is not in the same command as the point before the function was called, 2 otherwise (point and previous line are in the same command, and not inside the {} of a record)."
+  "Moves point back to previous pertinent line for indentation. Move point to the
+first non white space character. Returns 0 if top of buffer was reached, 3 if inside
+a comment or string, 4 if inside the {} of a record, 1 if the line found is not in
+the same command as the point before the function was called, 2 otherwise (point and
+previous line are in the same command, and not inside the {} of a record)."
+
   (if (proof-looking-at-syntactic-context) 3
     (let ((oldpt (point))
           (topnotreached (= (forward-line -1) 0))) ;;; nil if going one line backward
@@ -247,17 +237,13 @@ is moved at the end of the match if found, at LIM otherwise."
                   )
         (setq topnotreached (= (forward-line -1) 0)))
       (back-to-indentation)
-;      (message "coq-back-to-indentation-prevline... after while")
       (if (not topnotreached) 0 ;; returns nil if top of buffer was reached
         ;; if we are at end of a command (dot) find this command
         (if (find-reg oldpt coq-end-command-regexp) 
             (progn (forward-char -2)
-;                   (message "coq-back-to-indentation-prevline... coq-find-real-start")
                    (coq-find-real-start)
-;                   (message "coq-back-to-indentation-prevline... coq-find-real-start2")
                    1)
           (if (save-excursion 
-;                (message "coq-back-to-indentation-prevline... if 3")
                 (and (or (forward-char -1) t)
                      (coq-find-real-start)
                      (proof-looking-at-safe "Record")
@@ -590,12 +576,10 @@ argument must be t if inside the {}s of a record, nil otherwise."
          ;; The previous line is a comment start
          ((and (not atstart) (string-match coq-comment-start-regexp 
                                            (buffer-substring (point) eol)))
-          (message "indenting... point = %s" (point))
           (proof-re-search-forward coq-comment-start-regexp) 
           (+ 1 (current-column)))
 
          ((and (not atstart) (proof-looking-at-syntactic-context))
-          (message "coq-indent-comment-offset \\S-")
           (proof-re-search-forward "\\S-")
           (goto-char (match-beginning 0))
           (current-column))
@@ -626,17 +610,7 @@ argument must be t if inside the {}s of a record, nil otherwise."
 	  ((= kind 3) (if notcomments nil (coq-indent-comment-offset))))))
 
 (defun coq-indent-calculate (&optional notcomments) 
-  (coq-indent-offset notcomments)
-
-;  (let ((oldpt (point)) (prvfound nil) (res 0))
-;    (setq res
-;          (+ (save-excursion 
-;               (setq prvfound (coq-back-to-indentation-prevline))
-;               (current-column)) ; indentation of previous pertinent line
-;             (coq-indent-offset))) ; + offset for the current line
-;    (if (= prvfound 0) 0 res) ; if we are at buffer top, then 0 else res
-;    )
-  )
+  (coq-indent-offset notcomments))
 
 
 (defun proof-indent-line ()
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 5477629e..ba52abf9 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -124,10 +124,10 @@ will be used to suggest values to the user."
 	  (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) :"))
+    (setq option (coq-read-directory "Add directory (tab to complete, empty to stop) :"))
     (while (not (string-equal option ""))
       (setq progargs (cons option (cons "-I" progargs))) ;reversed
-      (setq option (coq-read-directory "Add directory (empty to stop) -I :")))
+      (setq option (coq-read-directory "Add directory (tab to complete, empty to stop) -I :")))
     (reverse progargs)))
 
 (defun coq-ask-prog-name (&optional oldvalue)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 5d86b123..33de4dee 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -381,8 +381,11 @@ so for the following reasons:
      ("Comments" nil "Comments #." nil "Comments")
      ("Delimit Scope" "delsc" "Delimit Scope @{scope} with @{id}." t "Delimit\\s-+Scope" )
      ("Eval" nil "Eval #." nil "Eval")
+     ("Extract Constant" "extrc" "Extract Constant @{id} => \"@{id}\"." nil "Extract\\s-+Constant")
+     ("Extract Inlined Constant" "extric" "Extract Inlined Constant @{id} => \"@{id}\"." nil "Extract\\s-+Inlined\\s-+Constant")
+     ("Extract Inductive" "extri" "Extract Inductive @{id} => \"@{id}\" [\"@{id}\" \"@{id...}\"]." nil "Extract")
      ("Extraction" "extr" "Extraction @{id}." nil "Extraction")
-     ("Extraction (in a file)" "extrf" "Extraction \" t@{file}\" @{id}.")
+     ("Extraction (in a file)" "extrf" "Extraction \"@{file}\" @{id}.")
      ("Extraction Inline" nil "Extraction Inline #." t "Extraction\\s-+Inline")
      ("Extraction NoInline" nil "Extraction NoInline #." t "Extraction\\s-+NoInline")
      ("Extraction Language" "extrlang" "Extraction Language #." t "Extraction\\s-+Language")
diff --git a/coq/coq.el b/coq/coq.el
index 6bf7c453..9af9b2f9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1212,17 +1212,6 @@ mouse activation."
   )
 
 
-;load the default coq abbrev file if no coq abbrev file is already read
-
-(if (and (boundp 'coq-mode-abbrev-table)
-         (not (equal coq-mode-abbrev-table (make-abbrev-table))))
-    (message "An abbrev table exists for coq, no default loaded")
-  (progn
-    (quietly-read-abbrev-file "coq-abbrev.el")
-    (message "coq default abbreviations loaded"))
-  )
-
-
 ;;;;;;;;;;;;;;;;;;;;;
 ; Some smart insertion function
 ;;;;;;;;;;;;;;;;;;;;;;