diff options
author | Makarius Wenzel <makarius@sketis.net> | 2000-06-08 19:52:01 +0000 |
---|---|---|
committer | Makarius Wenzel <makarius@sketis.net> | 2000-06-08 19:52:01 +0000 |
commit | 81956504f52a67275d0f267ab259aaafe6300d8c (patch) | |
tree | bd16152975d52765c944e57d3a519ebd5f571399 | |
parent | ef28215c14bf6cec69a7a430526b2b819e264251 (diff) |
adapted to new indentation setup;
-rw-r--r-- | isa/isa.el | 35 | ||||
-rw-r--r-- | plastic/plastic.el | 31 |
2 files changed, 3 insertions, 63 deletions
@@ -44,13 +44,6 @@ ;;; 'isabelle-config - Configuration of Isabelle Proof General ;;; (constants, but may be nice to tweak) -(defcustom isabelle-indent 2 - "*Indentation degree in proof scripts. -Somewhat irrelevant for Isabelle because normal proof scripts have -no regular or easily discernable structure." - :type 'number - :group 'isabelle) - ;;; ;;; ======== Configuration of generic modes ======== @@ -102,8 +95,6 @@ and script mode." (list isa-goal-with-hole-regexp 2) (list isa-save-with-hole-regexp 2 'backward isa-goal-command-regexp)) - ;; - proof-indent-commands-regexp (proof-ids-to-regexp isa-keywords) ;; proof engine commands proof-showproof-command "pr();" @@ -123,8 +114,6 @@ and script mode." proof-count-undos-fn 'isa-count-undos proof-find-and-forget-fn 'isa-find-and-forget proof-state-preserving-p 'isa-state-preserving-p - proof-parse-indent 'isa-parse-indent - proof-stack-to-indent 'isa-stack-to-indent ;; close goal..save regions eagerly proof-completed-proof-behaviour 'closeany @@ -543,30 +532,6 @@ you will be asked to retract the file or process the remainder of it." "Non-nil if command preserves the proofstate." (not (proof-string-match isa-not-undoable-commands-regexp cmd))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Indentation ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -;; -;; Sadly this is pretty pointless for Isabelle. -;; Proof scripts in Isabelle don't really have an easily-observed -;; block structure -- a case split can be done by any obscure tactic, -;; and then solved in a number of steps that bears no relation to the -;; number of cases! And the end is certainly not marked in anyway. -;; -(defun isa-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))) - (+ isabelle-indent (current-column)))))) - -(defun isa-parse-indent (c stack) - "Indentation function for Isabelle. Does nothing." - stack) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Isa shell startup and exit hooks ;; diff --git a/plastic/plastic.el b/plastic/plastic.el index 9da59458..8ca3058b 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -37,11 +37,6 @@ :type 'file :group 'plastic) -(defcustom plastic-indent 2 - "*Indentation" - :type 'number - :group 'plastic) - (defcustom plastic-test-all-name "need_a_global_lib" "*The name of the LEGO module which inherits all other modules of the library." @@ -310,25 +305,6 @@ Given is the first SPAN which needs to be undone." ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Plastic Indentation ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - -(defun plastic-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))) - (+ plastic-indent (current-column)))))) - -(defun plastic-parse-indent (c stack) - (cond - ((eq c ?\{) (cons (list c (point)) stack)) - ((eq c ?\}) (cdr stack)) - (t stack))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Plastic shell startup and exit hooks ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -404,16 +380,15 @@ Given is the first SPAN which needs to be undone." proof-count-undos-fn 'plastic-count-undos proof-find-and-forget-fn 'plastic-find-and-forget proof-goal-hyp-fn 'plastic-goal-hyp - proof-state-preserving-p 'plastic-state-preserving-p - proof-parse-indent 'plastic-parse-indent - proof-stack-to-indent 'plastic-stack-to-indent) + proof-state-preserving-p 'plastic-state-preserving-p) (setq proof-save-command-regexp plastic-save-command-regexp proof-goal-command-regexp plastic-goal-command-regexp proof-save-with-hole-regexp plastic-save-with-hole-regexp proof-goal-with-hole-regexp plastic-goal-with-hole-regexp proof-kill-goal-command plastic-kill-goal-command - proof-indent-commands-regexp (proof-ids-to-regexp plastic-commands)) + proof-indent-any-regexp + (proof-regexp-alt (proof-ids-to-regexp plastic-commands) "\\s(" "\\s)")) (plastic-init-syntax-table) |