From a47df1c7efedc74ea484ecf278eb5123e9cde36f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 4 Nov 1998 13:56:11 +0000
Subject: Reimplemented thy-find-other-file

---
 isa/thy-mode.el | 27 +++++++++++++--------------
 1 file changed, 13 insertions(+), 14 deletions(-)

diff --git a/isa/thy-mode.el b/isa/thy-mode.el
index 641be424..99707615 100644
--- a/isa/thy-mode.el
+++ b/isa/thy-mode.el
@@ -384,26 +384,25 @@ Choice based on first name found by:
   (interactive)
   (and (fboundp 'sml-mode) (sml-mode)))
 
-(defvar isa-ml-file-extension ".ML"
-  "*File name extension to use for ML files.")
+(defcustom isa-ml-file-extension ".ML"
+  "*File name extension to use for ML files."
+  :type 'string
+  :group 'isabelle)
 
 (defun thy-find-other-file ()
   "Find associated .ML or .thy file."
   (interactive)
   (and 
    (buffer-file-name)
-   (let ((fname (buffer-file-name)))
-     (cond ((string-match "\\.thy$" fname)
-	    (find-file-other-window
-	     (concat 
-	      (substring fname 0 -4) 
-	      isa-ml-file-extension)))
-	   ((string-match (concat (regexp-quote isa-ml-file-extension) "$")
-			  fname)
-	    (find-file (concat
-			(substring fname 0 (- (length isa-ml-file-extension)))
-			".thy")))))))
-
+   (let* ((fname     (buffer-file-name))
+	  (thyfile   (string-match "\\.thy$" fname))
+	  (mlfile    (string-match
+		      (concat (regexp-quote isa-ml-file-extension) "$") fname))
+	  (basename  (file-name-sans-extension fname)))
+     (cond (thyfile
+	    (find-file-other-window (concat basename isa-ml-file-extension)))
+	   (mlfile
+	    (find-file-other-window (concat basename ".thy")))))))
   
 
 ;;; "minor" sml-mode inside theory files ==========
-- 
cgit v1.2.3