diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-response.el | 1 | ||||
| -rw-r--r-- | generic/proof-shell.el | 11 |
2 files changed, 11 insertions, 1 deletions
diff --git a/generic/pg-response.el b/generic/pg-response.el index 46c7e1b5..484ee0d5 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -22,6 +22,7 @@ (defvar proof-assistant-menu nil)) (require 'pg-assoc) +(require 'span) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 7b19fded..4cb46b0c 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -21,11 +21,20 @@ (require 'span) (require 'proof-utils)) +;; declare a few functions and variables from proof-tree - if we +;; require proof-tree the compiler complains about a recusive +;; dependency. +(declare-function proof-tree-urgent-action "proof-tree" (flags)) +(declare-function proof-tree-handle-delayed-output "proof-tree" + (old-proof-marker cmd flags span)) +(eval-when (compile) + ;; without the nil initialization the compiler still warns about this variable + (defvar proof-tree-external-display nil)) + (require 'scomint) (require 'pg-response) (require 'pg-goals) (require 'pg-user) ; proof-script, new-command-advance -(require 'proof-tree) ;; |