From 6a3c8d9bd0db3a4db6a01a0f587f309da568a943 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 15 Jan 2008 13:07:11 +0000 Subject: Many compatibility updates, bug fixes, rearrangements for compilation. --- lego/lego.el | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) (limited to 'lego') diff --git a/lego/lego.el b/lego/lego.el index 7a80df31..bffdf290 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -195,7 +195,7 @@ Given is the first SPAN which needs to be undone." ;; FIXME: make this stuff generic. This should be undo-n-times-cmd (concat "Undo " (int-to-string ct) ";"))) -(defun lego-goal-command-p (str) +(defun lego-goal-command-p (span) "Decide whether argument is a goal or not" (proof-string-match lego-goal-command-regexp (or (span-property span 'cmd) ""))) @@ -294,13 +294,6 @@ Checks the width in the `proof-goals-buffer'" (insert (format lego-pretty-set-width (- current-width 1))) ))))) -(defun lego-pre-shell-start () - (setq proof-prog-name lego-prog-name - proof-mode-for-shell 'lego-shell-mode - proof-mode-for-response 'lego-response-mode - proof-mode-for-goals 'lego-goals-mode)) - - (defun lego-mode-config () (setq proof-terminal-char ?\;) @@ -309,14 +302,14 @@ Checks the width in the `proof-goals-buffer'" (setq proof-assistant-home-page lego-www-home-page) - (setq proof-mode-for-script 'lego-mode) - (setq proof-showproof-command "Prf;" proof-goal-command "Goal %s;" proof-save-command "Save %s;" proof-context-command "Ctxt;" proof-info-command "Help;") + (setq proof-prog-name lego-prog-name) + (setq proof-goal-command-p 'lego-goal-command-p proof-completed-proof-behaviour 'closeany ; new in 3.0 proof-count-undos-fn 'lego-count-undos @@ -367,7 +360,6 @@ Checks the width in the `proof-goals-buffer'" ;; hooks and callbacks - (add-hook 'proof-pre-shell-start-hook 'lego-pre-shell-start nil t) (add-hook 'proof-shell-insert-hook 'lego-shell-adjust-line-width)) (defun lego-equal-module-filename (module filename) -- cgit v1.2.3