diff options
| author | David Aspinall | 1998-11-06 15:50:28 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-06 15:50:28 +0000 |
| commit | 612d4dc6a021662d85d5a0ced9b17d1cb0c8cd2d (patch) | |
| tree | 1d387e93188eeea0fc5471d601f0bb20c5523e18 | |
| parent | 7551e2199a7eb05a4968fdd6f4d599d42ad520ab (diff) | |
Added prefix arg to thy-find-other-file to use same window
| -rw-r--r-- | isa/thy-mode.el | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/isa/thy-mode.el b/isa/thy-mode.el index 99707615..dd0416a8 100644 --- a/isa/thy-mode.el +++ b/isa/thy-mode.el @@ -389,20 +389,23 @@ Choice based on first name found by: :type 'string :group 'isabelle) -(defun thy-find-other-file () - "Find associated .ML or .thy file." - (interactive) +(defun thy-find-other-file (&optional samewindow) + "Find associated .ML or .thy file. +If SAMEWINDOW is non-nil (prefix argument when called interactively), +use find-file instead of find-file-other-window." + (interactive "p") (and (buffer-file-name) (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))) + (basename (file-name-sans-extension fname)) + (findfn (if samewindow 'find-file else 'find-file-other-window))) (cond (thyfile - (find-file-other-window (concat basename isa-ml-file-extension))) + (funcall findfn (concat basename isa-ml-file-extension))) (mlfile - (find-file-other-window (concat basename ".thy"))))))) + (funcall findfn (concat basename ".thy"))))))) ;;; "minor" sml-mode inside theory files ========== |