diff options
| author |  Pierre Courtieu <courtieu@lri.fr> | 2000-08-14 17:09:06 +0000 |
|---|---|---|
| committer | Pierre Courtieu <courtieu@lri.fr> | 2000-08-14 17:09:06 +0000 |
| commit | 2bd0d2a681d79f027919aec58661f06a2d184426 (patch) | |
| tree | 5c536f7f12a8e8d2b353a3a3fc6914f6bceddae8 /coq | |
| parent | 6151201e58ed340b20670c0fed546dbdc56dc550 (diff) | |
enhancement of outline regexps for coq, now when hiding bodies, we see
completely definitions and theorems, but proof script are hidden (but
can be blindly sent to the prover). Seems to work correctly.
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq.el | 8 |
1 files changed, 4 insertions, 4 deletions
@@ -88,11 +88,11 @@ ;; ----- outline (defvar coq-outline-regexp - (proof-ids-to-regexp - '("Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" - "Remark" "Record" "Inductive" "Definition"))) + (concat "(\\*\\|" (proof-ids-to-regexp + '( +"Tactic" "Axiom" "Parameter" "Parameters" "Variable" "Variables" "Syntax" "Grammar" "Syntactic" "Load" "Require" "Hint" "Hints" "Correctness" "Section" "Chapter" "Goal" "Lemma" "Theorem" "Fact" "Remark" "Record" "Inductive" "Mutual" "Definition" "Fixpoint")))) -(defvar coq-outline-heading-end-regexp "\.\\|\\*)") +(defvar coq-outline-heading-end-regexp "\\*\)\n\\|\\.\n") (defvar coq-shell-outline-regexp coq-goal-regexp) (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp) |