basic setup for new indentation code;

2 files changed, 63 insertions, 76 deletions

diff --git a/coq/coq.el b/coq/coq.el
index fa2fb2ce..80f5cf12 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -360,49 +360,52 @@ This is specific to coq-mode."
 ;;   Indentation                                                    ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-;; "Case" is represented by 'c' on the stack, and
-;; "CoInductive" is represented by 'C'.
-(defun coq-stack-to-indent (stack)
-  (cond
-   ((null stack) 0)
-   ((null (car (car stack)))
-    (nth 1 (car stack)))
-   (t (let ((col (save-excursion
-		   (goto-char (nth 1 (car stack)))
-		   (current-column))))
-	(cond
-	 ((eq (car (car stack)) ?c)
-	  (save-excursion (move-to-column (current-indentation))
-			  (cond 
-			   ((eq (char-after (point)) ?|) (+ col 3))
-			   ((proof-looking-at "end") col)
-			   (t (+ col 5)))))	  
-	 ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C))
-	  (+ col (if (eq ?| (save-excursion 
-			      (move-to-column (current-indentation))
-			      (char-after (point)))) 2 4)))
-	 (t (1+ col)))))))
-
-(defun coq-parse-indent (c stack)
-  (cond
-   ((eq c ?C)
-    (cond ((proof-looking-at "Case")
-	   (cons (list ?c (point)) stack))
-	  ((proof-looking-at "CoInductive")
-	   (forward-char (length "CoInductive"))
-	   (cons (list c (- (point) (length "CoInductive"))) stack))
-	  (t stack)))
-   ((and (eq c ?e) (proof-looking-at "end") (eq (car (car stack)) ?c))
-    (cdr stack))
-
-   ((and (eq c ?I) (proof-looking-at "Inductive"))
-    (forward-char (length "Inductive"))
-    (cons (list c (- (point) (length "Inductive"))) stack))
-
-   ((and (eq c ?.) (or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C)))
-    (cdr stack))
-
-   (t stack)))
+;; FIXME mmw: code disabled; Is the new indentation scheme general
+;; enough to handle Coq as well?
+
+;;; "Case" is represented by 'c' on the stack, and
+;;; "CoInductive" is represented by 'C'.
+;(defun coq-stack-to-indent (stack)
+;  (cond
+;   ((null stack) 0)
+;   ((null (car (car stack)))
+;    (nth 1 (car stack)))
+;   (t (let ((col (save-excursion
+;		   (goto-char (nth 1 (car stack)))
+;		   (current-column))))
+;	(cond
+;	 ((eq (car (car stack)) ?c)
+;	  (save-excursion (move-to-column (current-indentation))
+;			  (cond 
+;			   ((eq (char-after (point)) ?|) (+ col 3))
+;			   ((proof-looking-at "end") col)
+;			   (t (+ col 5)))))	  
+;	 ((or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C))
+;	  (+ col (if (eq ?| (save-excursion 
+;			      (move-to-column (current-indentation))
+;			      (char-after (point)))) 2 4)))
+;	 (t (1+ col)))))))
+;
+;(defun coq-parse-indent (c stack)
+;  (cond
+;   ((eq c ?C)
+;    (cond ((proof-looking-at "Case")
+;	   (cons (list ?c (point)) stack))
+;	  ((proof-looking-at "CoInductive")
+;	   (forward-char (length "CoInductive"))
+;	   (cons (list c (- (point) (length "CoInductive"))) stack))
+;	  (t stack)))
+;   ((and (eq c ?e) (proof-looking-at "end") (eq (car (car stack)) ?c))
+;    (cdr stack))
+;
+;   ((and (eq c ?I) (proof-looking-at "Inductive"))
+;    (forward-char (length "Inductive"))
+;    (cons (list c (- (point) (length "Inductive"))) stack))
+;
+;   ((and (eq c ?.) (or (eq (car (car stack)) ?I) (eq (car (car stack)) ?C)))
+;    (cdr stack))
+;
+;   (t stack)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;    To guess the command line options   ;;
@@ -467,15 +470,23 @@ This is specific to coq-mode."
 	proof-find-and-forget-fn 'coq-find-and-forget
         proof-goal-hyp-fn 'coq-goal-hyp
 	proof-state-preserving-p 'coq-state-preserving-p
-	proof-global-p 'coq-global-p
-	proof-parse-indent 'coq-parse-indent
-	proof-stack-to-indent 'coq-stack-to-indent)
+	proof-global-p 'coq-global-p)
 
   (setq proof-save-command-regexp coq-save-command-regexp
 	proof-save-with-hole-regexp coq-save-with-hole-regexp
-	proof-goal-with-hole-regexp coq-goal-with-hole-regexp
-	proof-indent-commands-regexp (proof-ids-to-regexp coq-keywords))
-
+	proof-goal-with-hole-regexp coq-goal-with-hole-regexp)
+  
+  (setq	
+   proof-indent-close-offset -1
+   proof-indent-any-regexp
+   (proof-regexp-alt (proof-ids-to-regexp
+		      (append (list "Cases" "end") coq-keywords)) "\\s(" "\\s)")
+   proof-indent-enclose-regexp "|"
+   proof-indent-open-regexp
+   (proof-regexp-alt (proof-ids-to-regexp '("Cases")) "\\s(")
+   proof-indent-close-regexp
+   (proof-regexp-alt (proof-ids-to-regexp '("end")) "\\s)"))
+  
   (setq proof-auto-multiple-files t)	; until Coq has real support
 
   (setq proof-shell-start-silent-cmd "Begin Silent."
diff --git a/lego/lego.el b/lego/lego.el
index 5249100c..ea49805f 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -20,11 +20,6 @@
   :type 'file
   :group 'lego)
 
-(defcustom lego-indent 2
-  "*Indentation level."
-  :type 'number
-  :group 'lego)
-
 (defcustom lego-test-all-name "test_all"
   "*The name of the LEGO module which inherits all other modules of the
   library."
@@ -263,24 +258,6 @@ Given is the first SPAN which needs to be undone."
 (proof-defshortcut lego-intros "intros "  [(control i)])
 (proof-defshortcut lego-Refine "Refine "  [(control r)])
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;   Lego Indentation                                               ;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-
-(defun lego-stack-to-indent (stack)
-  (cond
-   ((null stack) 0)
-   ((null (car (car stack)))
-    (nth 1 (car stack)))
-   (t (save-excursion
-	(goto-char (nth 1 (car stack)))
-	(+ lego-indent (current-column))))))
-
-(defun lego-parse-indent (c stack)
-  (cond
-   ((eq c ?\{) (cons (list c (point)) stack))
-   ((eq c ?\}) (cdr stack))
-   (t stack)))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Lego shell startup and exit hooks                              ;;
@@ -341,16 +318,15 @@ Checks the width in the `proof-goals-buffer'"
 	proof-count-undos-fn 'lego-count-undos
 	proof-find-and-forget-fn 'lego-find-and-forget
         proof-goal-hyp-fn 'lego-goal-hyp
-	proof-state-preserving-p 'lego-state-preserving-p
-	proof-parse-indent 'lego-parse-indent
-	proof-stack-to-indent 'lego-stack-to-indent)
+	proof-state-preserving-p 'lego-state-preserving-p)
 
   (setq	proof-save-command-regexp lego-save-command-regexp
 	proof-goal-command-regexp lego-goal-command-regexp
 	proof-save-with-hole-regexp lego-save-with-hole-regexp
 	proof-goal-with-hole-regexp lego-goal-with-hole-regexp
 	proof-kill-goal-command lego-kill-goal-command
-	proof-indent-commands-regexp (proof-ids-to-regexp lego-commands))
+	proof-indent-any-regexp
+	(proof-regexp-alt (proof-ids-to-regexp lego-commands) "\\s(" "\\s)"))
 
   (lego-init-syntax-table)