diff options
| author | David Aspinall | 2009-09-10 23:04:40 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-09-10 23:04:40 +0000 |
| commit | ee91c3f2f1dd5f2f731db385134f38726b37b7ca (patch) | |
| tree | d9cb381181a462fdbfab57f7e1f0d4e67ce567b2 /generic/proof-utils.el | |
| parent | a060c0dc046e526f8bf88b512e3c7c27e93421f8 (diff) | |
Experimental changes to queue several commands at once and to allow pre-processing of commands when they're queued from script
Diffstat (limited to 'generic/proof-utils.el')
| -rw-r--r-- | generic/proof-utils.el | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 7a1ac808..7347ab58 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -53,10 +53,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -(require 'proof-compat) ; -(require 'bufhist) ; bufhist -;(require 'proof-syntax) ; syntax utils - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Handy macros @@ -678,6 +674,19 @@ 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)) + + + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; ;; Function for submitting bug reports. ;; |