aboutsummaryrefslogtreecommitdiffhomepage
path: root/lego
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-09 21:08:51 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-09 21:08:51 +0000
commitf5cf54710cb0d72eba35a59b1a3e86fb0c56473b (patch)
tree7d7c613186c9341092a3970502544efba568e97d /lego
parentc4d3e63e3bdc5041eedf2b9c7fb166963ed4020c (diff)
p-s-classify-output -> p-s-handle-output, and simplify system-specific hook
Diffstat (limited to 'lego')
-rw-r--r--lego/lego.el14
1 files changed, 7 insertions, 7 deletions
diff --git a/lego/lego.el b/lego/lego.el
index be48be41..dfec529f 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -44,12 +44,12 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Users should not need to change this.
-(defvar lego-shell-classify-output
- '((lambda (cmd string) (proof-string-match "^Module" cmd)) .
- (lambda (cmd string)
- (setq proof-shell-delayed-output
- ;;FIXME: This should be displayed in the minibuffer only
- (cons 'insert "\n\nImports done!"))))
+(defvar lego-shell-handle-output
+ '(lambda (cmd string)
+ (when (proof-string-match "^Module" cmd)
+ ;; prevent output and just give a minibuffer message
+ (setq proof-shell-last-output-kind 'systemspecific)
+ (message "Imports done!")))
"Acknowledge end of processing import declarations.")
(defconst lego-process-config
@@ -396,7 +396,7 @@ For LEGO, we assume that module identifiers coincide with file names."
proof-shell-init-cmd lego-process-config
proof-shell-restart-cmd lego-process-config
pg-subterm-anns-use-stack nil
- proof-shell-classify-output-system-specific lego-shell-classify-output
+ proof-shell-handle-output-system-specific lego-shell-handle-output
lego-shell-current-line-width nil
;; LEGO uses Unicode escape prefix: liable to create problems