diff options
| author | David Aspinall | 1998-11-04 13:56:11 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-04 13:56:11 +0000 |
| commit | a47df1c7efedc74ea484ecf278eb5123e9cde36f (patch) | |
| tree | 5990817ab2f6243db36552f05cc7b7bc089f78d1 /isa | |
| parent | 072b18a32a45984af854453ccfbd96f9682244dd (diff) | |
Reimplemented thy-find-other-file
Diffstat (limited to 'isa')
| -rw-r--r-- | isa/thy-mode.el | 27 |
1 files 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 ========== |