diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 17:01:16 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2004-04-02 17:01:16 +0000 |
| commit | 7f2d7dc8a4684428b34ac31170696b106d297a76 (patch) | |
| tree | 0c2d68550c81893cc8725bb8bf4bbdf95b865741 /lclam | |
| parent | ed9f35dd30e87038bb2333a7fa9b7ff75ecb1335 (diff) | |
Remove/fix some junk
Diffstat (limited to 'lclam')
| -rw-r--r-- | lclam/lclam.el | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/lclam/lclam.el b/lclam/lclam.el index 2bc3129a..ae171aa0 100644 --- a/lclam/lclam.el +++ b/lclam/lclam.el @@ -2,6 +2,8 @@ ;; Description: Proof General instance for Lambda-CLAM ;; Author: James Brotherston <jjb@dai.ed.ac.uk> ;; Last modified: 23 October 2001 +;; +;; $Id$ (require 'proof) ; load generic parts (require 'proof-syntax) @@ -28,7 +30,7 @@ ;; (defun lclam-config () - "Configure Proof General scripting for Isabelle." + "Configure Proof General scripting for Lambda-CLAM." (setq proof-terminal-char ?\. proof-comment-start "/*" @@ -166,12 +168,14 @@ ["Next section" thy-goto-next-section t] ["Prev section" thy-goto-prev-section t] ["Insert template" thy-insert-template t] - ["Include definitions" match-and-assert-defs - :active (proof-locked-region-empty-p)] +; da: commented out this, function is incomplete +; ["Include definitions" match-and-assert-defs +; :active (proof-locked-region-empty-p)] ["Process theory" process-thy-file :active (proof-locked-region-empty-p)] - ["Retract theory" isa-retract-thy-file - :active (proof-locked-region-full-p)] +; da: commented out this, there's no retract function provided +; ["Retract theory" isa-retract-thy-file +; :active (proof-locked-region-full-p)] ["Next error" proof-next-error t] ["Switch to script" thy-find-other-file t]))) |