From 65e7ae5b99316edfae459efcb50758a2d23b3e2d Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 22 Oct 1998 15:58:24 +0000
Subject: Prevented .thy files from appearing in message buffer.

---
 isa/isa.el | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/isa/isa.el b/isa/isa.el
index 99030c76..41ffcd2d 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -137,10 +137,14 @@ no regular or easily discernable structure."
    proof-shell-process-file 
    (cons
     ;; Theory loader output and verbose update() output.
-    "Reading \"\\(.*\\.ML\\)\"\\|Not reading \"\\(.*\\.ML\\)\""
+    "Reading \"\\(.*\\)\"\\|Not reading \"\\(.*\\)\""
     (lambda (str)
-      (or (match-string 1 str)
-	  (match-string 2 str))))
+      (let ((filename (or (match-string 1 str)
+			  (match-string 2 str))))
+	(if (string-match "\\.ML$" filename)
+	    filename)
+	;; Ignore .thy files for now
+	)))
    ;; This is the output returned by a special command to
    ;; query Isabelle for outdated files.
    proof-shell-retract-files-regexp
@@ -163,7 +167,7 @@ about to send commands from it to Isabelle.  This function sends
 a command to read any theory file corresponding to the current ML file.
 This is a hook function for proof-activate-scripting-hook."
   (if (and
-       (eq (proof-unprocessed-begin) (point-min))
+       (proof-locked-region-empty-p)
        ;; If we switch to this buffer and it *does* have a locked
        ;; region, we could check that no updates are needed and
        ;; unlock the whole buffer in case they were.  But that's
-- 
cgit v1.2.3