Added key binding to switch between theory and ML files.

2 files changed, 30 insertions, 0 deletions

diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi
index 08cb225a..7c59cb57 100644
--- a/doc/NewDoc.texi
+++ b/doc/NewDoc.texi
@@ -698,6 +698,23 @@ At present there is no easy way to get around this.
 @node Isabelle specific commands
 @section Isabelle specific commands
 
+@unnumberedsubsec Associated files
+@cindex Associated files
+
+In Isabelle proofscript mode, @kbd{C-c C-o} (@code{thy-find-other-file})
+finds and switches to the associated theory file, that is, the file with
+the same base name but extension @file{.thy} swapped for @file{.ML}.
+
+The same function (and keybinding) switches back to an ML file from the
+theory file.
+
+@deffn Command thy-find-other-file
+Find and switch to the associated ML file (when editing a theory file)
+or theory file (when editing an ML file).  
+@end deffn
+
+
+
 @node Isabelle customizations
 @section Isabelle customizations
 
diff --git a/isa/isa.el b/isa/isa.el
index 83cdb730..06c52c47 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -270,6 +270,10 @@ proof-shell-retract-files-regexp."
    "Isabelle script" nil
    (isa-mode-config))
 
+  
+
+
+
 ;; Automatically selecting theory mode or Proof General script mode.
 
 (defun isa-mode ()
@@ -346,6 +350,15 @@ Resulting output from Isabelle will be parsed by Proof General."
 (autoload 'thy-mode "thy-mode" 
 	  "Major mode for Isabelle theory files" t nil)
 
+(autoload 'thy-find-other-file "thy-mode" 
+	    "Find associated .ML or .thy file." t nil)
+
+;; Key to switch to theory mode
+(define-key isa-proofscript-mode-map 
+  [(control c) (control o)] 'thy-find-other-file)
+
+
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Code that's Isabelle specific                                  ;;