diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2012-02-07 11:20:14 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2012-02-07 11:20:14 +0000 |
commit | 5f7695ac97fe7e624f00954fa39b1b6149427654 (patch) | |
tree | 872d30079ced2442854969b2fa3e9291d9ad0601 /generic | |
parent | 04845cc6d877bc23976befc9a9d08b873a2a47ad (diff) |
New pseudo instances to help tool demonstrators in ocaml/ghci (in progress)
Diffstat (limited to 'generic')
-rw-r--r-- | generic/proof-site.el | 20 |
1 files changed, 15 insertions, 5 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index 92069167..b7101222 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -32,18 +32,28 @@ ;; auto-mode-alist, if it is not present, a regexp will be made up from ;; FILE-EXTENSION. IGNORED-EXTENSIONS-LIST, if present, is appended to ;; completion-ignored-extensions. See proof-assistant-table for more info. +;; (defconst proof-assistant-table-default - '((isar "Isabelle" "thy") + '( + ;; Main instances of PG. + + (isar "Isabelle" "thy") (coq "Coq" "v" nil (".vo" ".glob")) (phox "PhoX" "phx") - ;; Obscure/conflict with other useful modes: + ;; Obscure instances or conflict with other Emacs modes. - (lego "LEGO" "l") - (hol-light "HOL Light" "ml") ; [for testing] + ;; (lego "LEGO" "l") ;; (ccc "CASL Consistency Checker" "ccc") - ;; (pgshell "PG-Shell" "pgsh") + (hol-light "HOL Light" "ml") ; [for testing] + + ;; Cut-and-paste management only + + (pgshell "PG-Shell" "pgsh") + (pgocaml "PG-OCaml" "pgml") + (pghaskell "PG-Haskell" "pghci") + ;; Incomplete/obsolete: ;; (hol98 "HOL" "sml") |