diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 1999-05-27 19:24:05 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 1999-05-27 19:24:05 +0000 |
| commit | 654813cfbde23c0855f1619d5894491dc1f7eec4 (patch) | |
| tree | 5748b5fca5ab3dd49407b3012432d7426add9044 | |
| parent | b50aa5058c361ac72a293c70b4ee82e7cd608279 (diff) | |
renamed proof-commands-regexp to proof-indent-commands-regexp, which
is less confusing);
| -rw-r--r-- | coq/coq.el | 2 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 6 | ||||
| -rw-r--r-- | isa/isa.el | 2 | ||||
| -rw-r--r-- | lego/lego.el | 2 | ||||
| -rw-r--r-- | plastic/plastic.el | 2 |
5 files changed, 7 insertions, 7 deletions
@@ -443,7 +443,7 @@ proof-save-with-hole-regexp coq-save-with-hole-regexp proof-goal-with-hole-regexp coq-goal-with-hole-regexp proof-kill-goal-command coq-kill-goal-command - proof-commands-regexp (proof-ids-to-regexp coq-keywords)) + proof-indent-commands-regexp (proof-ids-to-regexp coq-keywords)) (coq-init-syntax-table) diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index d531d107..7a4a8330 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -56,10 +56,10 @@ nil if a region cannot be found." ;; Generic font-lock -;; proof-commands-regexp is used for indentation -(defvar proof-commands-regexp "" +(defvar proof-indent-commands-regexp "" "Subset of keywords and tacticals which are terminated by the - `proof-terminal-char'") +`proof-terminal-char'. Basic indentation is provided automatically +for these.") (defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" @@ -125,7 +125,7 @@ no regular or easily discernable structure." (list isa-save-with-hole-regexp 2 'backward isa-goal-command-regexp)) ;; - proof-commands-regexp (proof-ids-to-regexp isa-keywords) + proof-indent-commands-regexp (proof-ids-to-regexp isa-keywords) ;; proof engine commands (first three for menus, last for undo) proof-prf-string "pr();" diff --git a/lego/lego.el b/lego/lego.el index 5b34d6bc..f7eafdbe 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -368,7 +368,7 @@ Checks the width in the `proof-goals-buffer'" 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-commands-regexp (proof-ids-to-regexp lego-commands)) + proof-indent-commands-regexp (proof-ids-to-regexp lego-commands)) (lego-init-syntax-table) diff --git a/plastic/plastic.el b/plastic/plastic.el index 6eb8061c..4ba4586a 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -406,7 +406,7 @@ Given is the first SPAN which needs to be undone." 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-commands-regexp (proof-ids-to-regexp plastic-commands)) + proof-indent-commands-regexp (proof-ids-to-regexp plastic-commands)) (plastic-init-syntax-table) |