diff options
| -rw-r--r-- | generic/pg-user.el | 9 | ||||
| -rw-r--r-- | generic/proof-utils.el | 12 |
2 files changed, 5 insertions, 16 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 9c1953b9..86dda135 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -20,9 +20,10 @@ (require 'proof-script) ; we build on proof-script -(eval-when-compile - (require 'cl) - (require 'completion)) ; loaded dynamically at runtime +(require 'cl) +(eval-when (compile) + (require 'completion) ; loaded dynamically at runtime + (defvar which-func-modes nil)) ; defined by which-func ; defined in proof-script/proof-setup-parsing-mechanism (declare-function proof-segment-up-to "proof-script") @@ -542,7 +543,7 @@ If variable `proof-electric-terminator-enable' is non-nil, the command will be sent to the assistant." (interactive) (if proof-electric-terminator-enable - (proof-insert-electric-terminator) + (proof-assert-electric-terminator) (self-insert-command 1))) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 4eabdb64..d937ce2b 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -674,18 +674,6 @@ or if the window is the only window of its frame." )))))) -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Function for manipulating output -;; - -(defsubst proof-shell-strip-output-markup (string &optional push) - "Strip output markup from STRING. -Convenience function to call function `proof-shell-strip-output-markup'. -Optional argument PUSH is ignored." - (funcall proof-shell-strip-output-markup string)) - - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; |