--- a/Admin/isatest/settings/cygwin-poly-e Thu Mar 03 14:38:31 2011 +0100
+++ b/Admin/isatest/settings/cygwin-poly-e Thu Mar 03 18:43:15 2011 +0100
@@ -1,7 +1,7 @@
# -*- shell-script -*- :mode=shellscript:
- POLYML_HOME="/home/isatest/polyml-5.4.0"
- ML_SYSTEM="polyml-5.4.0"
+ POLYML_HOME="/home/isatest/polyml-svn"
+ ML_SYSTEM="polyml-5.4.1"
ML_PLATFORM="x86-cygwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
ML_OPTIONS="-H 200"
--- a/NEWS Thu Mar 03 14:38:31 2011 +0100
+++ b/NEWS Thu Mar 03 18:43:15 2011 +0100
@@ -16,6 +16,11 @@
* Discontinued old lib/scripts/polyml-platform, which has been
obsolete since Isabelle2009-2.
+* Theory loader: source files are exclusively located via the master
+directory of each theory node (where the .thy file itself resides).
+The global load path (such as src/HOL/Library) is has been
+discontinued. INCOMPATIBILITY.
+
*** HOL ***
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Thu Mar 03 14:38:31 2011 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Thu Mar 03 18:43:15 2011 +0100
@@ -23,7 +23,7 @@
val base_path = Path.explode base_name |> tap check_ext
val (full_path, _) =
- Thy_Load.check_file [Thy_Load.master_directory thy] base_path
+ Thy_Load.check_file (Thy_Load.master_directory thy) base_path
val _ = Boogie_VCs.is_closed thy orelse
error ("Found the beginning of a new Boogie environment, " ^
--- a/src/HOL/Codegenerator_Test/Candidates.thy Thu Mar 03 14:38:31 2011 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy Thu Mar 03 18:43:15 2011 +0100
@@ -7,7 +7,7 @@
imports
Complex_Main
Library
- List_Prefix
+ "~~/src/HOL/Library/List_Prefix"
"~~/src/HOL/Number_Theory/Primes"
"~~/src/HOL/ex/Records"
begin
--- a/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 14:38:31 2011 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Thu Mar 03 18:43:15 2011 +0100
@@ -5621,6 +5621,4 @@
apply mir
done
-unused_thms
-
end
--- a/src/HOL/HOLCF/HOLCF.thy Thu Mar 03 14:38:31 2011 +0100
+++ b/src/HOL/HOLCF/HOLCF.thy Thu Mar 03 18:43:15 2011 +0100
@@ -13,8 +13,6 @@
default_sort "domain"
-ML {* Thy_Load.legacy_path_add "~~/src/HOL/HOLCF/Library" *}
-
text {* Legacy theorem names deprecated after Isabelle2009-2: *}
lemmas expand_fun_below = fun_below_iff
--- a/src/HOL/Plain.thy Thu Mar 03 14:38:31 2011 +0100
+++ b/src/HOL/Plain.thy Thu Mar 03 18:43:15 2011 +0100
@@ -9,6 +9,4 @@
include @{text Hilbert_Choice}.
*}
-ML {* Thy_Load.legacy_path_add "~~/src/HOL/Library" *}
-
end
--- a/src/HOL/SPARK/Tools/spark_commands.ML Thu Mar 03 14:38:31 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Thu Mar 03 18:43:15 2011 +0100
@@ -18,8 +18,9 @@
fun spark_open vc_name thy =
let
val (vc_path, _) = Thy_Load.check_file
- [Thy_Load.master_directory thy] (Path.explode vc_name);
- val (base, header) = (case Path.split_ext vc_path of
+ (Thy_Load.master_directory thy) (Path.explode vc_name);
+ val (base, header) =
+ (case Path.split_ext vc_path of
(base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
| (base, "siv") => (base, Fdl_Lexer.siv_header >> K ())
| _ => error "File name must end with .vcg or .siv");
--- a/src/Pure/ProofGeneral/pgip_isabelle.ML Thu Mar 03 14:38:31 2011 +0100
+++ b/src/Pure/ProofGeneral/pgip_isabelle.ML Thu Mar 03 18:43:15 2011 +0100
@@ -80,7 +80,7 @@
NONE => (NONE, NONE)
| SOME fname =>
let val path = Path.explode fname in
- if can (Thy_Load.check_file [Path.current]) path
+ if can (Thy_Load.check_file Path.current) path
then (SOME (PgipTypes.pgipurl_of_path path), NONE)
else (NONE, SOME fname)
end);
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 03 14:38:31 2011 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 03 18:43:15 2011 +0100
@@ -764,35 +764,8 @@
(*** Files ***)
-(* 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.
- NB: PGIP does not assume that the prover has a load path.
-*)
-
-local
- val current_working_dir = Unsynchronized.ref (NONE : string option)
-in
-fun changecwd_dir newdirpath =
- let
- val newdir = File.platform_path newdirpath
- in
- (case (!current_working_dir) of
- NONE => ()
- | SOME dir => Thy_Load.legacy_del_path dir;
- Thy_Load.legacy_add_path newdir;
- current_working_dir := SOME newdir)
- end
-end
-
-fun changecwd (Changecwd vs) =
- let
- val url = #url vs
- val newdir = PgipTypes.path_of_pgipurl url
- in
- changecwd_dir url
- end
+fun changecwd (Changecwd {url, ...}) =
+ Thy_Load.set_master_path (PgipTypes.path_of_pgipurl url)
fun openfile (Openfile vs) =
let
@@ -806,7 +779,7 @@
SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
PgipTypes.string_of_pgipurl url)
| NONE => (openfile_retract filepath;
- changecwd_dir filedir;
+ Thy_Load.set_master_path filedir;
Output.urgent_message ("Working in file: " ^ PgipTypes.string_of_pgipurl url);
currently_open_file := SOME url)
end
--- a/src/Pure/Thy/present.ML Thu Mar 03 14:38:31 2011 +0100
+++ b/src/Pure/Thy/present.ML Thu Mar 03 18:43:15 2011 +0100
@@ -462,7 +462,7 @@
val files_html = files |> map (fn (raw_path, loadit) =>
let
- val path = #1 (Thy_Load.check_file [dir] raw_path);
+ val path = #1 (Thy_Load.check_file dir raw_path);
val base = Path.base path;
val base_html = html_ext base;
val _ = add_file (Path.append html_prefix base_html,
--- a/src/Pure/Thy/thy_load.ML Thu Mar 03 14:38:31 2011 +0100
+++ b/src/Pure/Thy/thy_load.ML Thu Mar 03 18:43:15 2011 +0100
@@ -15,12 +15,7 @@
val master_directory: theory -> Path.T
val imports_of: theory -> string list
val provide: Path.T * (Path.T * file_ident) -> theory -> theory
- val legacy_show_path: unit -> string list
- val legacy_add_path: string -> unit
- val legacy_path_add: string -> unit
- val legacy_del_path: string -> unit
- val legacy_reset_path: unit -> unit
- val check_file: Path.T list -> Path.T -> Path.T * file_ident
+ val check_file: Path.T -> Path.T -> Path.T * file_ident
val check_thy: Path.T -> string -> Path.T * file_ident
val deps_thy: Path.T -> string ->
{master: Path.T * file_ident, text: string, imports: string list, uses: Path.T list}
@@ -122,30 +117,12 @@
else (master_dir, imports, required, (src_path, path_id) :: provided));
-(* maintain default paths *)
+(* stateful master path *)
local
- val load_path = Synchronized.var "load_path" [Path.current];
val master_path = Unsynchronized.ref Path.current;
in
-fun legacy_show_path () = map Path.implode (Synchronized.value load_path);
-
-fun legacy_del_path s = Synchronized.change load_path (remove (op =) (Path.explode s));
-
-fun legacy_add_path s = Synchronized.change load_path (update (op =) (Path.explode s));
-
-fun legacy_path_add s =
- Synchronized.change load_path (fn path =>
- let val p = Path.explode s
- in remove (op =) p path @ [p] end);
-
-fun legacy_reset_path () = Synchronized.change load_path (K [Path.current]);
-
-fun search_path dir path =
- distinct (op =)
- (dir :: (if Path.is_basic path then (Synchronized.value load_path) else [Path.current]));
-
fun set_master_path path = master_path := path;
fun get_master_path () = ! master_path;
@@ -154,36 +131,25 @@
(* check files *)
-fun get_file dirs src_path =
+fun get_file dir src_path =
let
val path = Path.expand src_path;
val _ = Path.is_current path andalso error "Bad file specification";
+ val full_path = File.full_path (Path.append dir path);
in
- dirs |> get_first (fn dir =>
- let val full_path = File.full_path (Path.append dir path) in
- (case file_ident full_path of
- NONE => NONE
- | SOME id => SOME (dir, (full_path, id)))
- end)
+ (case file_ident full_path of
+ NONE => NONE
+ | SOME id => SOME (full_path, id))
end;
-fun check_file dirs file =
- (case get_file dirs file of
- SOME (_, path_id) =>
- (if is_some (get_file [hd dirs] file) then ()
- else
- legacy_feature ("File " ^ quote (Path.implode file) ^
- " located via secondary search path: " ^
- quote (Path.implode (#1 (the (get_file (tl dirs) file)))));
- path_id)
+fun check_file dir file =
+ (case get_file dir file of
+ SOME path_id => path_id
| NONE => error ("Could not find file " ^ quote (Path.implode file) ^
- "\nin " ^ commas_quote (map Path.implode dirs)));
+ "\nin " ^ quote (Path.implode dir)));
-fun check_thy master_dir name =
- let
- val thy_file = Thy_Header.thy_path name;
- val dirs = search_path master_dir thy_file;
- in check_file dirs thy_file end;
+fun check_thy dir name =
+ check_file dir (Thy_Header.thy_path name);
(* theory deps *)
@@ -221,9 +187,9 @@
let
val {master_dir, provided, ...} = Files.get thy;
fun current (src_path, (_, id)) =
- (case get_file [master_dir] src_path of
+ (case get_file master_dir src_path of
NONE => false
- | SOME (_, (_, id')) => id = id');
+ | SOME (_, id') => id = id');
in can check_loaded thy andalso forall current provided end;
val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
@@ -232,15 +198,15 @@
(* provide files *)
fun provide_file src_path thy =
- provide (src_path, check_file [master_directory thy] src_path) thy;
+ provide (src_path, check_file (master_directory thy) src_path) thy;
fun use_ml src_path =
if is_none (Context.thread_data ()) then
- ML_Context.eval_file (#1 (check_file [Path.current] src_path))
+ ML_Context.eval_file (#1 (check_file Path.current src_path))
else
let
val thy = ML_Context.the_global_context ();
- val (path, id) = check_file [master_directory thy] src_path;
+ val (path, id) = check_file (master_directory thy) src_path;
val _ = ML_Context.eval_file path;
val _ = Context.>> Local_Theory.propagate_ml_env;
--- a/src/Tools/case_product.ML Thu Mar 03 14:38:31 2011 +0100
+++ b/src/Tools/case_product.ML Thu Mar 03 18:43:15 2011 +0100
@@ -1,5 +1,5 @@
-(* Title: case_product.ML
- Author: Lars Noschinski
+(* Title: Tools/case_product.ML
+ Author: Lars Noschinski, TU Muenchen
Combines two case rules into a single one.
@@ -9,8 +9,7 @@
*)
signature CASE_PRODUCT =
- sig
-
+sig
val combine: Proof.context -> thm -> thm -> thm
val combine_annotated: Proof.context -> thm -> thm -> thm
val setup: theory -> theory
@@ -104,7 +103,8 @@
(* Attribute setup *)
-val case_prod_attr = let
+val case_prod_attr =
+ let
fun combine_list ctxt = fold (fn x => fn y => combine_annotated ctxt y x)
in
Attrib.thms >> (fn thms => Thm.rule_attribute (fn ctxt => fn thm =>