From 0ebffe5a142f157a9a8715221d9e167dd16484a6 Mon Sep 17 00:00:00 2001 From: Makarius Wenzel Date: Thu, 8 Jun 2000 19:45:59 +0000 Subject: basic setup for new indentation code; --- coq/coq.el | 109 ++++++++++++++++++++++++++++++++--------------------------- lego/lego.el | 30 ++-------------- 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) -- cgit v1.2.3