# HG changeset patch
# User wenzelm
# Date 1299174195 -3600
# Node ID 550a8ecffe0c49498e3032e768c065b58c128c76
# Parent  58c4e0d75492e65d8246fa9332514ac541bb5cd5# Parent  ececcbd08d352a8a411367dbaa8935debbb74596
merged

diff -r 58c4e0d75492 -r 550a8ecffe0c Admin/isatest/settings/cygwin-poly-e
--- 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"
diff -r 58c4e0d75492 -r 550a8ecffe0c NEWS
--- 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 ***
 
diff -r 58c4e0d75492 -r 550a8ecffe0c src/HOL/Boogie/Tools/boogie_commands.ML
--- 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, " ^
diff -r 58c4e0d75492 -r 550a8ecffe0c src/HOL/Codegenerator_Test/Candidates.thy
--- 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
diff -r 58c4e0d75492 -r 550a8ecffe0c src/HOL/Decision_Procs/MIR.thy
--- 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
diff -r 58c4e0d75492 -r 550a8ecffe0c src/HOL/HOLCF/HOLCF.thy
--- 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
diff -r 58c4e0d75492 -r 550a8ecffe0c src/HOL/Plain.thy
--- 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
diff -r 58c4e0d75492 -r 550a8ecffe0c src/HOL/SPARK/Tools/spark_commands.ML
--- 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");
diff -r 58c4e0d75492 -r 550a8ecffe0c src/Pure/ProofGeneral/pgip_isabelle.ML
--- 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);
diff -r 58c4e0d75492 -r 550a8ecffe0c src/Pure/ProofGeneral/proof_general_pgip.ML
--- 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
diff -r 58c4e0d75492 -r 550a8ecffe0c src/Pure/Thy/present.ML
--- 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,
diff -r 58c4e0d75492 -r 550a8ecffe0c src/Pure/Thy/thy_load.ML
--- 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;
diff -r 58c4e0d75492 -r 550a8ecffe0c src/Tools/case_product.ML
--- 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 =>