equal
deleted
inserted
replaced
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 _ = |