Moved proof-file-truename, proof-file-to-buffer, to proof.el

Made setting font-lock-always-fontify-immediately be buffer local
in proof scripts (it's an ugly hack for comma-defontification).

1 files changed, 11 insertions, 18 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index f2320327..576656df 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -414,20 +414,9 @@ to allow other files loaded by proof assistants to be marked read-only."
 	  ;; End of locked region is always end of buffer
 	  (proof-set-locked-end (proof-script-end))))))
 
-(defun proof-file-truename (filename)
-  "Returns the true name of the file FILENAME or nil if file non-existent."
-  (and filename (file-exists-p filename) (file-truename filename)))
-
-(defun proof-file-to-buffer (filename)
-  "Find a buffer visiting file FILENAME, or nil if there isn't one."
-  (let* ((buffers (buffer-list))
-	 (pos
-	  (position (file-truename filename)
-		    (mapcar 'proof-file-truename
-			    (mapcar 'buffer-file-name
-				    buffers))
-		    :test 'equal)))
-    (and pos (nth pos buffers))))
+
+
+
 
 ;; FIXME da: cleanup of odd asymmetry here: we have a nice setting for
 ;; proof-register-possibly-new-processed-file but something much more
@@ -2232,6 +2221,8 @@ finish setup which depends on specific proof assistant configuration."
 
   ;; Additional key definitions which depend on configuration for
   ;; specific proof assistant.
+  ;; This is rather fragile: we assume terminal char is something
+  ;; sensible (and exists) for this to be set.
   (define-key proof-mode-map
     (vconcat [(control c)] (vector proof-terminal-char))
     'proof-active-terminator-minor-mode)
@@ -2287,10 +2278,10 @@ finish setup which depends on specific proof assistant configuration."
   (add-hook 'font-lock-mode-hook 'proof-unfontify-separator nil t)
 
   ;; if we don't have the following, zap-commas fails to work.
-  ;; FIXME (da): setting this to t everywhere is too brutal.  Should
-  ;; probably make it local.
-  (and (boundp 'font-lock-always-fontify-immediately)
-       (setq font-lock-always-fontify-immediately t))
+  (if (boundp 'font-lock-always-fontify-immediately)
+      (progn
+	(make-local-variable 'font-lock-always-fontify-immediately)
+	(setq font-lock-always-fontify-immediately nil)))
 
   ;; Assume font-lock case folding follows proof-case-fold-search
   (setq font-lock-keywords-case-fold-search proof-case-fold-search)
@@ -2357,6 +2348,8 @@ finish setup which depends on specific proof assistant configuration."
   (proof-x-symbol-mode))
 
 
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; FIXME FIXME FIXME da: