rearranged code to avoid compiler warning messages

4 files changed, 21 insertions, 14 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 690eda08..b7334087 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -271,8 +271,8 @@ to allow other files loaded by proof assistants to be marked read-only."
   "Issue the warning STR."
     (proof-response-buffer-display str 'proof-warning-face)
     (display-buffer proof-response-buffer)
-    (set-window-buffer-dedicated
-     (get-buffer-window proof-response-buffer)  proof-response-buffer))
+    (set-window-dedicated-p
+     (get-buffer-window proof-response-buffer) 'dedicated))
 
 
 (defun proof-register-possibly-new-processed-file (file)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index fac7305b..7a25236c 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -15,7 +15,10 @@
 
 (eval-when-compile
   (require 'comint)
-  (require 'font-lock)
+  (require 'font-lock))
+
+;; Spans are our abstraction of extents/overlays.
+(eval-and-compile
   (cond ((fboundp 'make-extent) (require 'span-extent))
 	((fboundp 'make-overlay) (require 'span-overlay))))
 
@@ -745,17 +748,6 @@ arrive."
 	      'proof-eager-annotation-face))
     (proof-shell-message str))))
 
-(defun proof-response-buffer-display (str face)
-  "Display STR with FACE in response buffer."
-  (let ((start))
-    (save-excursion
-      (set-buffer proof-response-buffer)
-      (setq start (goto-char (point-max)))
-      (insert str)
-      (font-lock-fontify-region start (point-max))
-      (font-lock-append-text-property start (point-max) 'face face)
-      (insert "\n"))))
-
 (defun proof-files-to-buffers (filenames)
   "Converts a list of FILENAMES into a list of BUFFERS."
   (if (null filenames) nil
diff --git a/generic/proof.el b/generic/proof.el
index 62b9489a..1e64ffe3 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -78,6 +78,17 @@ The argument KBL is a list of tuples (k . f) where `k' is a keybinding
          (define-key map k f)))
    kbl))
 
+(defun proof-response-buffer-display (str face)
+  "Display STR with FACE in response buffer."
+  (let ((start))
+    (save-excursion
+      (set-buffer proof-response-buffer)
+      (setq start (goto-char (point-max)))
+      (insert str)
+      (font-lock-fontify-region start (point-max))
+      (font-lock-append-text-property start (point-max) 'face face)
+      (insert "\n"))))
+
 ;;;
 ;;; Global variables
 ;;;
diff --git a/todo b/todo
index 25565734..e0023f9b 100644
--- a/todo
+++ b/todo
@@ -20,6 +20,10 @@ A byte-compilation: continue fixups for clean byte compile.
   works for both varieties of Emacs. 
   Fill out Makefile.dist (4hr da)
 
+C support for templates e.g., in LEGO it would be nice if, by default, 
+  fresh buffers corrsponding to file foo.l would automatically insert
+  "Module foo;" (1h)
+
 C  Remove "FIXME notes" which are just notes I've put in about old
    code in case something breaks   (da, 30mins).