From 34ad43fd72f6d9780fd7fc97cb51bb4d82fcc0d9 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 16 Sep 1998 14:36:38 +0000
Subject: Isabelle Proof General loads for .thy as well as .ML files.

---
 generic/proof-site.el | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'generic')

diff --git a/generic/proof-site.el b/generic/proof-site.el
index 9671940e..a31b8d1d 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -54,12 +54,14 @@ NB: To change proof assistant, you must start a new Emacs session."
 ;; to support the proof assistants selected
 (let ((assistants proof-assistants) proof-assistant)
   (while assistants
-    (let*  ((proof-assistant (car assistants))
-	    (fileregexp (cond ((eq proof-assistant 'coq)    "\\.v")
-			      ((eq proof-assistant 'lego)   "\\.l$")
-			      ((eq proof-assistant 'isa)    "\\.ML$")))
-	    (assistant-name   (symbol-name proof-assistant))
-	    (proof-mode  (intern (concat assistant-name "-mode"))))
+    (let*  
+	((proof-assistant (car assistants))
+	 (fileregexp 
+	  (cond ((eq proof-assistant 'coq)    "\\.v")
+		((eq proof-assistant 'lego)   "\\.l$")
+		((eq proof-assistant 'isa)    "\\.ML$|\\.thy$")))
+	 (assistant-name   (symbol-name proof-assistant))
+	 (proof-mode  (intern (concat assistant-name "-mode"))))
       (setq auto-mode-alist 
 	    (cons (cons fileregexp proof-mode) auto-mode-alist))
       ;; NB: File name for each prover is the same as its symbol name!
-- 
cgit v1.2.3