diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-12-10 11:30:22 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-12-10 11:30:22 +0000 |
| commit | 6b9d0ef562f909b2a47664c8d381d888da74a189 (patch) | |
| tree | 9aeb1149f78f2da3335fc708ecd2f0d06723c1c2 /generic/proof-x-symbol.el | |
| parent | 9d9fe4ee3ae54c3b0937e5a5d6f57e6f30a418bd (diff) | |
proof-x-symbol-initialize: fix default mode name construction
Diffstat (limited to 'generic/proof-x-symbol.el')
| -rw-r--r-- | generic/proof-x-symbol.el | 18 |
1 files changed, 7 insertions, 11 deletions
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el index 3ab3c9d4..135768b9 100644 --- a/generic/proof-x-symbol.el +++ b/generic/proof-x-symbol.el @@ -128,21 +128,17 @@ The package is available at http://x-symbol.sourceforge.net/")) ((xs-xtra-modes proof-xsym-extra-modes) (xs-std-modes (list - ;; NB: there is a problem with initialization order - ;; here, these variables are set in script/shell mode - ;; initialization. They ought to be set earlier, and - ;; enforced as part of the generic scheme. For the - ;; time being, we use default constructed names [which - ;; every prover should follow] + ;; NB: these variables are set in script/shell mode + ;; initialization, maybe too late for here. Backup: + ;; default names, which everyone should follow. (or proof-mode-for-shell - (intern (concat assistant "-shell-mode"))) + (intern (concat proof-assistant "-shell-mode"))) (or proof-mode-for-response - (intern (concat assistant "-response-mode"))) + (intern (concat proof-assistant "-response-mode"))) (or proof-mode-for-script - ;; FIXME: next one only correct for isabelle - (intern (concat assistant "-proofscript-mode"))) + (intern (concat proof-assistant "-mode"))) (or proof-mode-for-goals - (intern (concat assistant "-goals-mode"))))) + (intern (concat proof-assistant "-goals-mode"))))) (all-xs-modes (append xs-std-modes xs-xtra-modes)) (am-entry (list proof-xsym-extra-modes t `(quote ,xs-lang))) |