diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-06-23 10:22:52 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-06-23 10:22:52 +0000 |
| commit | 086147fe901f149479dac0e187e6078d50857502 (patch) | |
| tree | 148ed1d236f8a65f331f09b86c2aceb016a75c7f | |
| parent | 22ffdd2c276a6527ffcb74ae19c5c5415132f86a (diff) | |
Disable provers whose file extensions clash with sml mode. Default to Isabelle/Isar
| -rw-r--r-- | generic/proof-site.el | 27 |
1 files changed, 17 insertions, 10 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index 25ce95b8..53416f4e 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -105,22 +105,29 @@ You can use customize to set this variable." (if (and atts (eq 't (car atts))) (list dne) nil))) - '(;; For demonstration instance of Proof General, - ;; export PROOFGENERAL_ASSISTANTS=demoisa. - ;; - ;; To use Isabelle/Isar instead of classic Isabelle, - ;; export PROOFGENERAL_ASSISTANTS=isar - ;; - (demoisa "Isabelle Demo" "\\.ML$") - (isa "Isabelle" "\\.ML$\\|\\.thy$") - (isar "Isabelle/Isar" "\\.thy$") + '( +;; To use classic Isabelle instead of Isabelle/Isar, +;; uncomment appropriate line below and set +;; export PROOFGENERAL_ASSISTANTS=isar +;; +;; To Use HOL, uncomment the line below. It's disabled +;; by default because of clash with SML mode (same for .ML). +;; +;; For the demonstration instance of Proof General, +;; uncomment first line below and set +;; export PROOFGENERAL_ASSISTANTS=demoisa. +;; +;; (demoisa "Isabelle Demo" "\\.ML$") +;; (isa "Isabelle" "\\.ML$\\|\\.thy$") + (isar "Isabelle" "\\.thy$") (lego "LEGO" "\\.l$") (coq "Coq" "\\.v$\\|\\.v8$\\|\\.v7$") (phox "PhoX" "\\.phx$") (ccc "CASL Consistency Checker" "\\.ccc$") ;; The following provers are not fully supported, and have only ;; preliminary support written (please volunteer to improve them!) - (hol98 "HOL" "\\.sml$") + +;; (hol98 "HOL" "\\.sml$") (acl2 "ACL2" "\\.acl2$") (twelf "Twelf" "\\.elf$") ;; The following provers have experimental support, WIP |