Added key binding to switch between theory and ML files.

1 files changed, 13 insertions, 0 deletions

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                                  ;;