From 84807c20846c98db4f1dfd28f7f7ad66ed87cd1c Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 4 Apr 2000 13:23:58 +0000
Subject: Fix accidently introduced bug with passing full paths to theory
 loader.

---
 isa/isa.el | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/isa/isa.el b/isa/isa.el
index ad13eaf9..45cbce0b 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -281,10 +281,14 @@ and script mode."
 
 (defun isa-update-thy-only (file try wait)
   "Tell Isabelle to update current buffer's theory, and all ancestors."
+  ;; First make sure we're in the right directory to take care of
+  ;; relative "files" paths inside theory file.  (Isabelle bug??)
+  (proof-cd-sync)
   (proof-shell-invisible-command
    (proof-format-filename
-    (format "ProofGeneral.%supdate_thy_only \"%%s\";" (if try "try_" ""))
-    (file-name-sans-extension file))
+    ;; %r parameter means relative (don't expand) path
+    (format "ProofGeneral.%supdate_thy_only \"%%r\";" (if try "try_" ""))
+    (file-name-nondirectory (file-name-sans-extension file)))
    wait))
 
 (defun isa-shell-update-thy ()
-- 
cgit v1.2.3