diff options
| author | Healfdene Goguen | 1998-05-08 17:09:13 +0000 |
|---|---|---|
| committer | Healfdene Goguen | 1998-05-08 17:09:13 +0000 |
| commit | 4a2fd039c1168773576b88f344dc85286fa51bbd (patch) | |
| tree | 7749cf9e7b0e31c3d0756b6d0eff0b14d6496ab1 | |
| parent | 8a5741f228fe53decdf7f49566850f40e8001c68 (diff) | |
Made separated indentation more elegant.
Separated consideration of {}'s so it only happens for LEGO.
| -rw-r--r-- | lego.el | 11 |
1 files changed, 11 insertions, 0 deletions
@@ -5,6 +5,10 @@ ;; $Log$ +;; Revision 1.43 1998/05/08 17:09:13 hhg +;; Made separated indentation more elegant. +;; Separated consideration of {}'s so it only happens for LEGO. +;; ;; Revision 1.42 1998/05/08 15:36:41 hhg ;; Merged indentation code for LEGO and Coq into proof.el. ;; @@ -526,6 +530,12 @@ (goto-char (nth 1 (car stack))) (1+ (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 ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -570,6 +580,7 @@ proof-goal-hyp-fn 'lego-goal-hyp proof-state-preserving-p 'lego-state-preserving-p proof-global-p 'lego-global-p + proof-parse-indent 'lego-parse-indent proof-stack-to-indent 'lego-stack-to-indent) (setq proof-save-command-regexp lego-save-command-regexp |
