diff options
| author | David Aspinall | 1998-09-16 14:36:38 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-09-16 14:36:38 +0000 |
| commit | 34ad43fd72f6d9780fd7fc97cb51bb4d82fcc0d9 (patch) | |
| tree | 74d6d582dc306ef42c4dbb11e4b64c29a42b0ca6 | |
| parent | 6c6bd41dd41d3854ce57bb613dee63b2e181d550 (diff) | |
Isabelle Proof General loads for .thy as well as .ML files.
| -rw-r--r-- | generic/proof-site.el | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index 9671940e..a31b8d1d 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -54,12 +54,14 @@ NB: To change proof assistant, you must start a new Emacs session." ;; to support the proof assistants selected (let ((assistants proof-assistants) proof-assistant) (while assistants - (let* ((proof-assistant (car assistants)) - (fileregexp (cond ((eq proof-assistant 'coq) "\\.v") - ((eq proof-assistant 'lego) "\\.l$") - ((eq proof-assistant 'isa) "\\.ML$"))) - (assistant-name (symbol-name proof-assistant)) - (proof-mode (intern (concat assistant-name "-mode")))) + (let* + ((proof-assistant (car assistants)) + (fileregexp + (cond ((eq proof-assistant 'coq) "\\.v") + ((eq proof-assistant 'lego) "\\.l$") + ((eq proof-assistant 'isa) "\\.ML$|\\.thy$"))) + (assistant-name (symbol-name proof-assistant)) + (proof-mode (intern (concat assistant-name "-mode")))) (setq auto-mode-alist (cons (cons fileregexp proof-mode) auto-mode-alist)) ;; NB: File name for each prover is the same as its symbol name! |