src/Pure/proof_general.ML
changeset 16791 31678cf364b1
parent 16789 e8f7a6ec92e5
child 16798 36d34186741b
     1.1 --- a/src/Pure/proof_general.ML	Wed Jul 13 11:30:37 2005 +0200
     1.2 +++ b/src/Pure/proof_general.ML	Wed Jul 13 12:14:23 2005 +0200
     1.3 @@ -1115,7 +1115,7 @@
     1.4  fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)
     1.5  
     1.6  
     1.7 -(* load an arbitrary (.thy or .ML) file *)
     1.8 +(* load an arbitrary file (must be .thy or .ML) *)
     1.9  
    1.10  fun use_thy_or_ml_file file =
    1.11      let
    1.12 @@ -1125,7 +1125,6 @@
    1.13              "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
    1.14            | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
    1.15            | "ML" => isarcmd ("use " ^ quote file)
    1.16 -          (* instead of error we could guess theory? *)
    1.17            | other => error ("Don't know how to read a file with extension " ^ other)
    1.18      end
    1.19  
    1.20 @@ -1160,6 +1159,22 @@
    1.21  
    1.22    val currently_open_file = ref (NONE : string option)
    1.23  
    1.24 +  (* Path management: we allow theory files to have dependencies
    1.25 +     in their own directory, but when we change directory for a new
    1.26 +     file we remove the path.  Leaving it there can cause confusion
    1.27 +     with difference in batch mode.a  NB: PGIP does not assume
    1.28 +     that the prover has a load path. *)
    1.29 +  local 
    1.30 +      val current_working_dir = ref (NONE : string option)
    1.31 +  in
    1.32 +      fun changecwd dir = 
    1.33 +	  (case (!current_working_dir) of
    1.34 +	       NONE => ()
    1.35 +             | SOME dir => ThyLoad.del_path dir;
    1.36 +	   ThyLoad.add_path dir;
    1.37 +	   current_working_dir := SOME dir)
    1.38 +  end
    1.39 +
    1.40    val topnode = Toplevel.node_of o Toplevel.get_state
    1.41    fun topproofpos () = (case topnode() of Toplevel.Proof ph => SOME(ProofHistory.position ph)
    1.42                                          | _ => NONE) handle Toplevel.UNDEF => NONE
    1.43 @@ -1239,7 +1254,7 @@
    1.44                                             currently_open_file := NONE)
    1.45                                | NONE => raise PGIP ("closefile when no file is open!"))
    1.46       | "abortfile"      => (currently_open_file := NONE) (* perhaps error for no file open *)
    1.47 -     | "changecwd"      => ThyLoad.add_path (dirname_attr attrs)
    1.48 +     | "changecwd"      => changecwd (dirname_attr attrs)
    1.49       | "systemcmd"      => isarscript data
    1.50       (* unofficial command for debugging *)
    1.51       | "quitpgip" => raise PGIP_QUIT