# HG changeset patch
# User aspinall
# Date 1121249663 -7200
# Node ID 31678cf364b165eed9c8ec9cfa0b1646581ff23e
# Parent  be2780f435e1c51be5c89c2524320722ca02e078
Add management for current working directory

diff -r be2780f435e1 -r 31678cf364b1 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Jul 13 11:30:37 2005 +0200
+++ b/src/Pure/proof_general.ML	Wed Jul 13 12:14:23 2005 +0200
@@ -1115,7 +1115,7 @@
 fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)
 
 
-(* load an arbitrary (.thy or .ML) file *)
+(* load an arbitrary file (must be .thy or .ML) *)
 
 fun use_thy_or_ml_file file =
     let
@@ -1125,7 +1125,6 @@
             "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
           | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
           | "ML" => isarcmd ("use " ^ quote file)
-          (* instead of error we could guess theory? *)
           | other => error ("Don't know how to read a file with extension " ^ other)
     end
 
@@ -1160,6 +1159,22 @@
 
   val currently_open_file = ref (NONE : string option)
 
+  (* Path management: we allow theory files to have dependencies
+     in their own directory, but when we change directory for a new
+     file we remove the path.  Leaving it there can cause confusion
+     with difference in batch mode.a  NB: PGIP does not assume
+     that the prover has a load path. *)
+  local 
+      val current_working_dir = ref (NONE : string option)
+  in
+      fun changecwd dir = 
+	  (case (!current_working_dir) of
+	       NONE => ()
+             | SOME dir => ThyLoad.del_path dir;
+	   ThyLoad.add_path dir;
+	   current_working_dir := SOME dir)
+  end
+
   val topnode = Toplevel.node_of o Toplevel.get_state
   fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph)
                                         | _ => NONE) handle Toplevel.UNDEF => NONE
@@ -1239,7 +1254,7 @@
                                            currently_open_file := NONE)
                               | NONE => raise PGIP ("closefile when no file is open!"))
      | "abortfile"      => (currently_open_file := NONE) (* perhaps error for no file open *)
-     | "changecwd"      => ThyLoad.add_path (dirname_attr attrs)
+     | "changecwd"      => changecwd (dirname_attr attrs)
      | "systemcmd"      => isarscript data
      (* unofficial command for debugging *)
      | "quitpgip" => raise PGIP_QUIT