diff options
| -rw-r--r-- | generic/proof-shell.el | 14 | ||||
| -rw-r--r-- | generic/proof-x-symbol.el | 9 |
2 files changed, 15 insertions, 8 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 8f9b74c9..5443963c 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -13,9 +13,9 @@ (require 'span) (require 'comint) (require 'font-lock) - (require 'proof-autoloads) (require 'proof-utils)) +(require 'proof-autoloads) (require 'pg-response) (require 'pg-goals) (require 'proof-script) @@ -1346,7 +1346,7 @@ MESSAGE should be a string annotated with ;; CASE theorem dependency: prover lists thms used in last proof ((and proof-shell-theorem-dependency-list-regexp (string-match proof-shell-theorem-dependency-list-regexp message)) - (let ((names (match- string 1 message)) + (let ((names (match-string 1 message)) (deps (match-string 2 message))) (setq proof-last-theorem-dependencies (cons @@ -1390,9 +1390,7 @@ MESSAGE should be a string annotated with "Issue MSG as a prompt and receive user input." (let ((input (ignore-errors - (read-input - msg - nil + (read-string msg nil 'proof-shell-minibuffer-urgent-interactive-input-history)))) ;; Always send something, even if read-input was errorful (proof-shell-insert (or input "") 'interactive-input))) @@ -1765,7 +1763,7 @@ Annotations are characters 128-255." (while (< i 256) (aset disp i []) (incf i)) - (cond ((fboundp 'add-spec-to-specifier) + (cond ((featurep 'xemacs) (add-spec-to-specifier current-display-table disp (current-buffer))) ((boundp 'buffer-display-table) (setq buffer-display-table disp)))))) @@ -1777,7 +1775,8 @@ in the shell buffer. Use proof-shell-dont-show-annotations to turn them off again. XEmacs only." (interactive) - (remove-specifier current-display-table (current-buffer))) + (if (featurep 'xemacs) + (remove-specifier current-display-table (current-buffer)))) @@ -1904,6 +1903,7 @@ usual, unless NOERROR is non-nil." (setq proof-shell-no-response-display nil)) proof-shell-last-output) +;;;###autoload (defun proof-shell-invisible-command-invisible-result (cmd &optional noerror) "Execute CMD, wait for but do not display result." ;; Just same as previous function, except we discard result diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el index aaf1dcc3..4cf3c09a 100644 --- a/generic/proof-x-symbol.el +++ b/generic/proof-x-symbol.el @@ -43,7 +43,14 @@ ;; ================================================================= (eval-when-compile - (require 'proof-utils)) ; proof-ass + (add-to-list 'load-path "../x-symbol/lisp") + (require 'x-symbol-hooks) ; <reduce compiler warnings> + (require 'x-symbol-autoloads) ; <reduce compiler warnings> + (require 'proof-utils)) ; proof-ass + +(require 'proof-config) ; variables +(require 'proof-autoloads) ; + (defvar proof-x-symbol-initialized nil "Non-nil if x-symbol support has been initialized.") |