src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 41885 1e081bfb2eaf
parent 41491 a2ad5b824051
child 42003 6e45dc518ebb
equal deleted inserted replaced
41884:335895ffbd94 41885:1e081bfb2eaf
   762     end
   762     end
   763 
   763 
   764 
   764 
   765 (*** Files ***)
   765 (*** Files ***)
   766 
   766 
   767 (* Path management: we allow theory files to have dependencies in
   767 fun changecwd (Changecwd {url, ...}) =
   768    their own directory, but when we change directory for a new file we
   768   Thy_Load.set_master_path (PgipTypes.path_of_pgipurl url)
   769    remove the path.  Leaving it there can cause confusion with
       
   770    difference in batch mode.
       
   771    NB: PGIP does not assume that the prover has a load path.
       
   772 *)
       
   773 
       
   774 local
       
   775     val current_working_dir = Unsynchronized.ref (NONE : string option)
       
   776 in
       
   777 fun changecwd_dir newdirpath =
       
   778    let
       
   779        val newdir = File.platform_path newdirpath
       
   780    in
       
   781        (case (!current_working_dir) of
       
   782             NONE => ()
       
   783           | SOME dir => Thy_Load.legacy_del_path dir;
       
   784         Thy_Load.legacy_add_path newdir;
       
   785         current_working_dir := SOME newdir)
       
   786    end
       
   787 end
       
   788 
       
   789 fun changecwd (Changecwd vs) =
       
   790     let
       
   791         val url = #url vs
       
   792         val newdir = PgipTypes.path_of_pgipurl url
       
   793     in
       
   794         changecwd_dir url
       
   795     end
       
   796 
   769 
   797 fun openfile (Openfile vs) =
   770 fun openfile (Openfile vs) =
   798   let
   771   let
   799       val url = #url vs
   772       val url = #url vs
   800       val filepath = PgipTypes.path_of_pgipurl url
   773       val filepath = PgipTypes.path_of_pgipurl url
   804   in
   777   in
   805       case !currently_open_file of
   778       case !currently_open_file of
   806           SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
   779           SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
   807                                 PgipTypes.string_of_pgipurl url)
   780                                 PgipTypes.string_of_pgipurl url)
   808         | NONE => (openfile_retract filepath;
   781         | NONE => (openfile_retract filepath;
   809                    changecwd_dir filedir;
   782                    Thy_Load.set_master_path filedir;
   810                    Output.urgent_message ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
   783                    Output.urgent_message ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
   811                    currently_open_file := SOME url)
   784                    currently_open_file := SOME url)
   812   end
   785   end
   813 
   786 
   814 fun closefile _ =
   787 fun closefile _ =