fixed indentation bug: use proof-looking-at (proof-case-fold-search);

4 files changed, 24 insertions, 24 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 92912244..d09479a6 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -343,7 +343,7 @@
 	  (save-excursion (move-to-column (current-indentation))
 			  (cond 
 			   ((eq (char-after (point)) ?|) (+ col 3))
-			   ((looking-at "end") col)
+			   ((proof-looking-at "end") col)
 			   (t (+ col 5)))))	  
 	 ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C))
 	  (+ col (if (eq ?| (save-excursion 
@@ -354,16 +354,16 @@
 (defun coq-parse-indent (c stack)
   (cond
    ((eq c ?C)
-    (cond ((looking-at "Case")
+    (cond ((proof-looking-at "Case")
 	   (cons (list ?c (point)) stack))
-	  ((looking-at "CoInductive")
+	  ((proof-looking-at "CoInductive")
 	   (forward-char (length "CoInductive"))
 	   (cons (list c (- (point) (length "CoInductive"))) stack))
 	  (t stack)))
-   ((and (eq c ?e) (looking-at "end") (eq (car (car stack)) ?c))
+   ((and (eq c ?e) (proof-looking-at "end") (eq (car (car stack)) ?c))
     (cdr stack))
 
-   ((and (eq c ?I) (looking-at "Inductive"))
+   ((and (eq c ?I) (proof-looking-at "Inductive"))
     (forward-char (length "Inductive"))
     (cons (list c (- (point) (length "Inductive"))) stack))
 
diff --git a/generic/proof-indent.el b/generic/proof-indent.el
index 0295a3e6..6849cdd6 100644
--- a/generic/proof-indent.el
+++ b/generic/proof-indent.el
@@ -44,31 +44,31 @@
 	(setq forward-amount 1)   ; may be subject to dynamic scoping!
 	(cond 
 	 ;; strings
-	 ((and instring (looking-at proof-string-end-regexp))
+	 ((and instring (proof-looking-at proof-string-end-regexp))
 	  (setq forward-amount (length (match-string 0)))
 	  (setq instring nil))
 	 (instring)
-	 ((looking-at proof-string-start-regexp)
+	 ((proof-looking-at proof-string-start-regexp)
 	  (setq forward-amount (length (match-string 0)))
 	  (setq instring t))
 
 	 ;; comments
-	 ((looking-at cmt-start-regexp)
+	 ((proof-looking-at cmt-start-regexp)
 	  (setq forward-amount (length (match-string 0)))
 	  (incf cmt-level))
-	 ((looking-at cmt-end-regexp)
+	 ((proof-looking-at cmt-end-regexp)
 	  (setq forward-amount (length (match-string 0)))
 	  (decf cmt-level))
 	 ((> cmt-level 0))
 
 	 ;; parentheses
-	 ((looking-at "\\s(")
+	 ((proof-looking-at "\\s(")
 	  (setq stack (cons (list c (point)) stack)))
-	 ((looking-at "\\s)")
+	 ((proof-looking-at "\\s)")
 	  (setq stack (cdr stack)))
 	 
 	 ;; basic indentation for commands
-	 ((looking-at proof-indent-commands-regexp)
+	 ((proof-looking-at proof-indent-commands-regexp)
 	  (setq stack (cons (list proof-terminal-char (point)) stack)))
 	 ((and (eq c proof-terminal-char)
 	       (eq (car (car stack)) proof-terminal-char))
@@ -128,4 +128,4 @@
 	(setq state (proof-parse-to-point beg state)
 	      beg (point))))))
 
-(provide 'proof-indent)
\ No newline at end of file
+(provide 'proof-indent)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 576656df..e0471d5d 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1143,7 +1143,7 @@ the next command end."
 	   (setq done t alist (cons 'unclosed-comment alist))))
 	 (setq done t))
 	;; Case 3. Found a comment end, not inside a string
-	((and (looking-at comment-end-regexp) quote-parity)
+	((and (proof-looking-at comment-end-regexp) quote-parity)
 	 (if (= depth 0) 
 	     (progn
 	       (message "Warning: extraneous comment end")
@@ -1155,7 +1155,7 @@ the next command end."
 	     (aset str i ?\ )
 	     (incf i))))
 	;; Case 4. Found a comment start, not inside a string
-	((and (looking-at comment-start-regexp) quote-parity)
+	((and (proof-looking-at comment-start-regexp) quote-parity)
 	 (setq depth (+ depth 1))
 	 (forward-char (length (match-string 0))))
 	;; Case 5. Inside a comment. 
@@ -1173,9 +1173,9 @@ the next command end."
 
 	 ;; Maintain quote-parity
 	 (cond
-	  ((and quote-parity (looking-at proof-string-start-regexp))
+	  ((and quote-parity (proof-looking-at proof-string-start-regexp))
 	   (setq quote-parity nil))
-	  ((and (not quote-parity) (looking-at proof-string-end-regexp))
+	  ((and (not quote-parity) (proof-looking-at proof-string-end-regexp))
 	   (setq quote-parity t)))
 
 	 (forward-char)
diff --git a/isar/isar.el b/isar/isar.el
index a7bc567e..58ecd775 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -122,15 +122,15 @@
 		   (current-indentation))))
 	(if (and (eq (car (car stack)) ?p)
 		 (save-excursion (move-to-column (current-indentation))
-				 (looking-at isar-indent-enclose-regexp)))
+				 (proof-looking-at isar-indent-enclose-regexp)))
 	    col
 	  (+ isabelle-isar-indent col))))))
 
 (defun isar-parse-indent (c stack)
   (cond
-   ((looking-at isar-indent-open-regexp)
+   ((proof-looking-at isar-indent-open-regexp)
     (cons (list ?p (point)) stack))
-   ((and (looking-at isar-indent-close-regexp) (eq (car (car stack)) ?p))
+   ((and (proof-looking-at isar-indent-close-regexp) (eq (car (car stack)) ?p))
     (cdr stack))
    (t stack)))
 
@@ -154,18 +154,18 @@
 	(setq forward-amount 1)
 	(cond 
 	 ;; comments
-	 ((looking-at cmt-start-regexp)
+	 ((proof-looking-at cmt-start-regexp)
 	  (setq forward-amount (length (match-string 0)))
 	  (incf cmt-level))
-	 ((looking-at cmt-end-regexp)
+	 ((proof-looking-at cmt-end-regexp)
 	  (setq forward-amount (length (match-string 0)))
 	  (decf cmt-level))
 	 ((> cmt-level 0))
 	 ;; white space
-	 ((looking-at white-space-regexp)
+	 ((proof-looking-at white-space-regexp)
 	  (setq forward-amount (length (match-string 0))))
 	 ;; theory header
-	 ((looking-at header-regexp)
+	 ((proof-looking-at header-regexp)
 	  (setq found-header t)
 	  (setq cont nil))
 	 ;; bad stuff