moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
authorwenzelm
Sat Jul 24 12:14:53 2010 +0200 (2010-07-24 ago)
changeset 3794948a874444164
parent 37948 94e9302a7fd0
child 37950 bc285d91041e
moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
theory loader: reduced warnings -- thy database can be bypassed in certain situations;
Proof/Local_Theory.propagate_ml_env;
ML use function: propagate ML environment as well;
pervasive type generic_theory;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/ProofGeneral/proof_general_emacs.ML
src/Pure/ROOT.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_load.ML
src/Pure/pure_setup.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Jul 23 18:42:46 2010 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Jul 24 12:14:53 2010 +0200
     1.3 @@ -274,10 +274,9 @@
     1.4  (* init and exit *)
     1.5  
     1.6  fun init_theory (name, imports, uses) =
     1.7 -  Toplevel.init_theory name (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
     1.8 -    (fn thy =>
     1.9 -      if Thy_Info.check_known_thy (Context.theory_name thy)
    1.10 -      then Thy_Info.end_theory thy else ());
    1.11 +  Toplevel.init_theory name
    1.12 +    (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses))
    1.13 +    (Theory.end_theory #> tap Thy_Load.check_loaded #> Thy_Info.end_theory);
    1.14  
    1.15  val exit = Toplevel.keep (fn state =>
    1.16   (Context.set_thread_data (try Toplevel.generic_theory_of state);
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Jul 23 18:42:46 2010 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Jul 24 12:14:53 2010 +0200
     2.3 @@ -304,30 +304,23 @@
     2.4  
     2.5  (* use ML text *)
     2.6  
     2.7 -fun propagate_env (context as Context.Proof lthy) =
     2.8 -      Context.Proof (Local_Theory.map_contexts (ML_Env.inherit context) lthy)
     2.9 -  | propagate_env context = context;
    2.10 -
    2.11 -fun propagate_env_prf prf = Proof.map_contexts
    2.12 -  (Context.proof_map (ML_Env.inherit (Context.Proof (Proof.context_of prf)))) prf;
    2.13 -
    2.14  val _ =
    2.15    Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
    2.16 -    (Parse.path >>
    2.17 -      (fn path => Toplevel.generic_theory (Thy_Info.exec_file path #> propagate_env)));
    2.18 +    (Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
    2.19  
    2.20  val _ =
    2.21    Outer_Syntax.command "ML" "ML text within theory or local theory"
    2.22      (Keyword.tag_ml Keyword.thy_decl)
    2.23      (Parse.ML_source >> (fn (txt, pos) =>
    2.24        Toplevel.generic_theory
    2.25 -        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #> propagate_env)));
    2.26 +        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
    2.27 +          Local_Theory.propagate_ml_env)));
    2.28  
    2.29  val _ =
    2.30    Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
    2.31      (Parse.ML_source >> (fn (txt, pos) =>
    2.32        Toplevel.proof (Proof.map_context (Context.proof_map
    2.33 -        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)));
    2.34 +        (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
    2.35  
    2.36  val _ =
    2.37    Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
     3.1 --- a/src/Pure/Isar/local_theory.ML	Fri Jul 23 18:42:46 2010 +0200
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Jul 24 12:14:53 2010 +0200
     3.3 @@ -5,6 +5,7 @@
     3.4  *)
     3.5  
     3.6  type local_theory = Proof.context;
     3.7 +type generic_theory = Context.generic;
     3.8  
     3.9  signature LOCAL_THEORY =
    3.10  sig
    3.11 @@ -25,6 +26,7 @@
    3.12    val target_result: (Proof.context -> 'a * Proof.context) -> local_theory -> 'a * local_theory
    3.13    val target: (Proof.context -> Proof.context) -> local_theory -> local_theory
    3.14    val map_contexts: (Context.generic -> Context.generic) -> local_theory -> local_theory
    3.15 +  val propagate_ml_env: generic_theory -> generic_theory
    3.16    val standard_morphism: local_theory -> Proof.context -> morphism
    3.17    val target_morphism: local_theory -> morphism
    3.18    val global_morphism: local_theory -> morphism
    3.19 @@ -173,6 +175,10 @@
    3.20    target (Context.proof_map f) #>
    3.21    Context.proof_map f;
    3.22  
    3.23 +fun propagate_ml_env (context as Context.Proof lthy) =
    3.24 +      Context.Proof (map_contexts (ML_Env.inherit context) lthy)
    3.25 +  | propagate_ml_env context = context;
    3.26 +
    3.27  
    3.28  (* morphisms *)
    3.29  
     4.1 --- a/src/Pure/Isar/proof.ML	Fri Jul 23 18:42:46 2010 +0200
     4.2 +++ b/src/Pure/Isar/proof.ML	Sat Jul 24 12:14:53 2010 +0200
     4.3 @@ -17,6 +17,7 @@
     4.4    val theory_of: state -> theory
     4.5    val map_context: (context -> context) -> state -> state
     4.6    val map_contexts: (context -> context) -> state -> state
     4.7 +  val propagate_ml_env: state -> state
     4.8    val bind_terms: (indexname * term option) list -> state -> state
     4.9    val put_thms: bool -> string * thm list option -> state -> state
    4.10    val the_facts: state -> thm list
    4.11 @@ -207,6 +208,9 @@
    4.12  
    4.13  fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
    4.14  
    4.15 +fun propagate_ml_env state = map_contexts
    4.16 +  (Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
    4.17 +
    4.18  val bind_terms = map_context o ProofContext.bind_terms;
    4.19  val put_thms = map_context oo ProofContext.put_thms;
    4.20  
     5.1 --- a/src/Pure/Isar/toplevel.ML	Fri Jul 23 18:42:46 2010 +0200
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Jul 24 12:14:53 2010 +0200
     5.3 @@ -7,7 +7,6 @@
     5.4  signature TOPLEVEL =
     5.5  sig
     5.6    exception UNDEF
     5.7 -  type generic_theory
     5.8    type state
     5.9    val toplevel: state
    5.10    val is_toplevel: state -> bool
    5.11 @@ -103,8 +102,6 @@
    5.12  
    5.13  (* local theory wrappers *)
    5.14  
    5.15 -type generic_theory = Context.generic;    (*theory or local_theory*)
    5.16 -
    5.17  val loc_init = Theory_Target.context_cmd;
    5.18  val loc_exit = Local_Theory.exit_global;
    5.19  
     6.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Jul 23 18:42:46 2010 +0200
     6.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jul 24 12:14:53 2010 +0200
     6.3 @@ -137,7 +137,7 @@
     6.4      val name = thy_name file;
     6.5      val _ = name = "" andalso error ("Bad file name: " ^ quote file);
     6.6      val _ =
     6.7 -      if Thy_Info.check_known_thy name then
     6.8 +      if Thy_Info.known_thy name then
     6.9          (Isar.>> (Toplevel.commit_exit Position.none);
    6.10              Thy_Info.touch_child_thys name; Thy_Info.register_thy name)
    6.11            handle ERROR msg =>
     7.1 --- a/src/Pure/ROOT.ML	Fri Jul 23 18:42:46 2010 +0200
     7.2 +++ b/src/Pure/ROOT.ML	Sat Jul 24 12:14:53 2010 +0200
     7.3 @@ -184,10 +184,8 @@
     7.4  
     7.5  (*theory sources*)
     7.6  use "Thy/thy_header.ML";
     7.7 -use "Thy/thy_load.ML";
     7.8  use "Thy/html.ML";
     7.9  use "Thy/latex.ML";
    7.10 -use "Thy/present.ML";
    7.11  
    7.12  (*basic proof engine*)
    7.13  use "Isar/proof_display.ML";
    7.14 @@ -227,10 +225,12 @@
    7.15  use "Isar/constdefs.ML";
    7.16  
    7.17  (*toplevel transactions*)
    7.18 +use "Thy/thy_load.ML";
    7.19  use "Isar/proof_node.ML";
    7.20  use "Isar/toplevel.ML";
    7.21  
    7.22  (*theory syntax*)
    7.23 +use "Thy/present.ML";
    7.24  use "Thy/term_style.ML";
    7.25  use "Thy/thy_output.ML";
    7.26  use "Thy/thy_syntax.ML";
     8.1 --- a/src/Pure/Thy/thy_info.ML	Fri Jul 23 18:42:46 2010 +0200
     8.2 +++ b/src/Pure/Thy/thy_info.ML	Sat Jul 24 12:14:53 2010 +0200
     8.3 @@ -11,7 +11,6 @@
     8.4    val add_hook: (action -> string -> unit) -> unit
     8.5    val get_names: unit -> string list
     8.6    val known_thy: string -> bool
     8.7 -  val check_known_thy: string -> bool
     8.8    val if_known_thy: (string -> unit) -> string -> unit
     8.9    val lookup_theory: string -> theory option
    8.10    val get_theory: string -> theory
    8.11 @@ -23,10 +22,6 @@
    8.12    val thy_ord: theory * theory -> order
    8.13    val remove_thy: string -> unit
    8.14    val kill_thy: string -> unit
    8.15 -  val provide_file: Path.T -> string -> unit
    8.16 -  val load_file: Path.T -> unit
    8.17 -  val exec_file: Path.T -> Context.generic -> Context.generic
    8.18 -  val use: string -> unit
    8.19    val use_thys: string list -> unit
    8.20    val use_thy: string -> unit
    8.21    val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
    8.22 @@ -80,18 +75,15 @@
    8.23  (* thy database *)
    8.24  
    8.25  type deps =
    8.26 -  {update_time: int,                      (*symbolic time of update; negative value means outdated*)
    8.27 -    master: (Path.T * File.ident) option, (*master dependencies for thy file*)
    8.28 -    text: string,                         (*source text for thy*)
    8.29 -    parents: string list,                 (*source specification of parents (partially qualified)*)
    8.30 -      (*auxiliary files: source path, physical path + identifier*)
    8.31 -    files: (Path.T * (Path.T * File.ident) option) list};
    8.32 + {update_time: int,                      (*symbolic time of update; negative value means outdated*)
    8.33 +  master: (Path.T * File.ident) option,  (*master dependencies for thy file*)
    8.34 +  text: string,                          (*source text for thy*)
    8.35 +  parents: string list};                 (*source specification of parents (partially qualified)*)
    8.36  
    8.37 -fun make_deps update_time master text parents files : deps =
    8.38 -  {update_time = update_time, master = master, text = text, parents = parents, files = files};
    8.39 +fun make_deps update_time master text parents : deps =
    8.40 +  {update_time = update_time, master = master, text = text, parents = parents};
    8.41  
    8.42 -fun init_deps master text parents files =
    8.43 -  SOME (make_deps ~1 master text parents (map (rpair NONE) files));
    8.44 +fun init_deps master text parents = SOME (make_deps ~1 master text parents);
    8.45  
    8.46  fun master_dir NONE = Path.current
    8.47    | master_dir (SOME (path, _)) = Path.dir path;
    8.48 @@ -123,8 +115,7 @@
    8.49    SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
    8.50  
    8.51  val known_thy = is_some o lookup_thy;
    8.52 -fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
    8.53 -fun if_known_thy f name = if check_known_thy name then f name else ();
    8.54 +fun if_known_thy f name = if known_thy name then f name else ();
    8.55  
    8.56  fun get_thy name =
    8.57    (case lookup_thy name of
    8.58 @@ -144,13 +135,6 @@
    8.59  val is_finished = is_none o get_deps;
    8.60  val master_directory = master_dir' o get_deps;
    8.61  
    8.62 -fun loaded_files name =
    8.63 -  (case get_deps name of
    8.64 -    NONE => []
    8.65 -  | SOME {master, files, ...} =>
    8.66 -      (case master of SOME (thy_path, _) => [thy_path] | NONE => []) @
    8.67 -      (map_filter (Option.map #1 o #2) files));
    8.68 -
    8.69  fun get_parents name =
    8.70    thy_graph Graph.imm_preds name handle Graph.UNDEF _ =>
    8.71      error (loader_msg "nothing known about theory" [name]);
    8.72 @@ -168,27 +152,16 @@
    8.73      SOME theory => theory
    8.74    | _ => error (loader_msg "undefined theory entry for" [name]));
    8.75  
    8.76 +fun loaded_files name =
    8.77 +  (case get_deps name of
    8.78 +    NONE => []
    8.79 +  | SOME {master, ...} => (case master of SOME (thy_path, _) => [thy_path] | NONE => [])) @
    8.80 +  Thy_Load.loaded_files (get_theory name);
    8.81 +
    8.82  
    8.83  
    8.84  (** thy operations **)
    8.85  
    8.86 -(* check state *)
    8.87 -
    8.88 -fun check_unfinished fail name =
    8.89 -  if known_thy name andalso is_finished name then
    8.90 -    fail (loader_msg "cannot update finished theory" [name])
    8.91 -  else ();
    8.92 -
    8.93 -fun check_files name =
    8.94 -  let
    8.95 -    val files = (case get_deps name of SOME {files, ...} => files | NONE => []);
    8.96 -    val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path) | _ => NONE) files;
    8.97 -    val _ = null missing_files orelse
    8.98 -      error (loader_msg "unresolved dependencies of theory" [name] ^
    8.99 -        " on file(s): " ^ commas_quote missing_files);
   8.100 -  in () end;
   8.101 -
   8.102 -
   8.103  (* maintain update_time *)
   8.104  
   8.105  local
   8.106 @@ -207,8 +180,8 @@
   8.107  fun outdate_thy name =
   8.108    if is_finished name orelse is_outdated name then ()
   8.109    else CRITICAL (fn () =>
   8.110 -   (change_deps name (Option.map (fn {master, text, parents, files, ...} =>
   8.111 -    make_deps ~1 master text parents files)); perform Outdate name));
   8.112 +   (change_deps name (Option.map (fn {master, text, parents, ...} =>
   8.113 +    make_deps ~1 master text parents)); perform Outdate name));
   8.114  
   8.115  fun touch_thys names =
   8.116    List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
   8.117 @@ -266,52 +239,6 @@
   8.118  val kill_thy = if_known_thy remove_thy;
   8.119  
   8.120  
   8.121 -(* load_file *)
   8.122 -
   8.123 -local
   8.124 -
   8.125 -fun provide path name info (SOME {update_time, master, text, parents, files}) =
   8.126 -     (if AList.defined (op =) files path then ()
   8.127 -      else warning (loader_msg "undeclared dependency of theory" [name] ^
   8.128 -        " on file: " ^ quote (Path.implode path));
   8.129 -      SOME (make_deps update_time master text parents
   8.130 -        (AList.update (op =) (path, SOME info) files)))
   8.131 -  | provide _ _ _ NONE = NONE;
   8.132 -
   8.133 -fun run_file path =
   8.134 -  (case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of
   8.135 -    NONE => (Thy_Load.load_ml Path.current path; ())
   8.136 -  | SOME name =>
   8.137 -      (case lookup_deps name of
   8.138 -        SOME deps =>
   8.139 -          change_deps name (provide path name (Thy_Load.load_ml (master_dir' deps) path))
   8.140 -      | NONE => (Thy_Load.load_ml Path.current path; ())));
   8.141 -
   8.142 -in
   8.143 -
   8.144 -fun provide_file path name =
   8.145 -  let
   8.146 -    val dir = master_directory name;
   8.147 -    val _ = check_unfinished error name;
   8.148 -  in change_deps name (provide path name (Thy_Load.check_file dir path)) end;
   8.149 -
   8.150 -fun load_file path =
   8.151 -  if ! Output.timing then
   8.152 -    let val name = Path.implode path in
   8.153 -      timeit (fn () =>
   8.154 -       (priority ("\n**** Starting file " ^ quote name ^ " ****");
   8.155 -        run_file path;
   8.156 -        priority ("**** Finished file " ^ quote name ^ " ****\n")))
   8.157 -    end
   8.158 -  else run_file path;
   8.159 -
   8.160 -fun exec_file path = ML_Context.exec (fn () => load_file path);
   8.161 -
   8.162 -val use = load_file o Path.explode;
   8.163 -
   8.164 -end;
   8.165 -
   8.166 -
   8.167  (* load_thy *)
   8.168  
   8.169  fun required_by _ [] = ""
   8.170 @@ -321,22 +248,22 @@
   8.171    let
   8.172      val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
   8.173      fun corrupted () = error (loader_msg "corrupted dependency information" [name]);
   8.174 -    val (pos, text, _) =
   8.175 +    val (pos, text) =
   8.176        (case get_deps name of
   8.177 -        SOME {master = SOME (master_path, _), text, files, ...} =>
   8.178 +        SOME {master = SOME (master_path, _), text, ...} =>
   8.179            if text = "" then corrupted ()
   8.180 -          else (Path.position master_path, text, files)
   8.181 +          else (Path.position master_path, text)
   8.182        | _ => corrupted ());
   8.183      val _ = touch_thy name;
   8.184      val _ = CRITICAL (fn () =>
   8.185 -      change_deps name (Option.map (fn {master, text, parents, files, ...} =>
   8.186 -        make_deps upd_time master text parents files)));
   8.187 +      change_deps name (Option.map (fn {master, text, parents, ...} =>
   8.188 +        make_deps upd_time master text parents)));
   8.189      val after_load = Outer_Syntax.load_thy name pos text;
   8.190      val _ =
   8.191        CRITICAL (fn () =>
   8.192         (change_deps name
   8.193 -          (Option.map (fn {update_time, master, parents, files, ...} =>
   8.194 -            make_deps update_time master "" parents files));
   8.195 +          (Option.map (fn {update_time, master, parents, ...} =>
   8.196 +            make_deps update_time master "" parents));
   8.197          perform Update name));
   8.198    in after_load end;
   8.199  
   8.200 @@ -410,43 +337,33 @@
   8.201  
   8.202  local
   8.203  
   8.204 -fun check_file master (src_path, info) =
   8.205 -  let val info' =
   8.206 -    (case info of
   8.207 -      NONE => NONE
   8.208 -    | SOME (_, id) =>
   8.209 -        (case Thy_Load.test_file (master_dir master) src_path of
   8.210 -          NONE => NONE
   8.211 -        | SOME (path', id') => if id <> id' then NONE else SOME (path', id')))
   8.212 -  in (src_path, info') end;
   8.213 -
   8.214  fun check_deps dir name =
   8.215    (case lookup_deps name of
   8.216      SOME NONE => (true, NONE, get_parents name)
   8.217    | NONE =>
   8.218 -      let val {master, text, imports = parents, uses = files} = Thy_Load.deps_thy dir name
   8.219 -      in (false, init_deps (SOME master) text parents files, parents) end
   8.220 -  | SOME (SOME {update_time, master, text, parents, files}) =>
   8.221 +      let val {master, text, imports = parents, ...} = Thy_Load.deps_thy dir name
   8.222 +      in (false, init_deps (SOME master) text parents, parents) end
   8.223 +  | SOME (SOME {update_time, master, text, parents}) =>
   8.224        let
   8.225          val (thy_path, thy_id) = Thy_Load.check_thy dir name;
   8.226          val master' = SOME (thy_path, thy_id);
   8.227        in
   8.228          if Option.map #2 master <> SOME thy_id then
   8.229 -          let val {text = text', imports = parents', uses = files', ...} =
   8.230 -            Thy_Load.deps_thy dir name;
   8.231 -          in (false, init_deps master' text' parents' files', parents') end
   8.232 +          let val {text = text', imports = parents', ...} = Thy_Load.deps_thy dir name;
   8.233 +          in (false, init_deps master' text' parents', parents') end
   8.234          else
   8.235            let
   8.236 -            val files' = map (check_file master') files;
   8.237 -            val current = update_time >= 0 andalso can get_theory name
   8.238 -              andalso forall (is_some o snd) files';
   8.239 +            val current =
   8.240 +              (case lookup_theory name of
   8.241 +                NONE => false
   8.242 +              | SOME theory => update_time >= 0 andalso Thy_Load.all_current theory);
   8.243              val update_time' = if current then update_time else ~1;
   8.244 -            val deps' = SOME (make_deps update_time' master' text parents files');
   8.245 +            val deps' = SOME (make_deps update_time' master' text parents);
   8.246            in (current, deps', parents) end
   8.247        end);
   8.248  
   8.249 -fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents, files}) =
   8.250 -  SOME (make_deps update_time master (File.read path) parents files);
   8.251 +fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents}) =
   8.252 +  SOME (make_deps update_time master (File.read path) parents);
   8.253  
   8.254  in
   8.255  
   8.256 @@ -495,28 +412,31 @@
   8.257    schedule_tasks (snd (require_thys [] dir arg Graph.empty));
   8.258  
   8.259  val use_thys = use_thys_dir Path.current;
   8.260 -
   8.261 -fun use_thy str =
   8.262 -  let
   8.263 -    val name = base_name str;
   8.264 -    val _ = check_unfinished warning name;
   8.265 -  in use_thys [str] end;
   8.266 +val use_thy = use_thys o single;
   8.267  
   8.268  
   8.269  (* begin / end theory *)
   8.270  
   8.271 +fun check_unfinished name =
   8.272 +  if known_thy name andalso is_finished name then
   8.273 +    error (loader_msg "cannot update finished theory" [name])
   8.274 +  else ();
   8.275 +
   8.276  fun begin_theory name parents uses int =
   8.277    let
   8.278      val parent_names = map base_name parents;
   8.279      val dir = master_dir'' (lookup_deps name);
   8.280 -    val _ = check_unfinished error name;
   8.281 +    val _ = check_unfinished name;
   8.282      val _ = if int then use_thys_dir dir parents else ();
   8.283  
   8.284 -    val theory = Theory.begin_theory name (map get_theory parent_names);
   8.285 +    val theory =
   8.286 +      Theory.begin_theory name (map get_theory parent_names)
   8.287 +      |> Thy_Load.init dir
   8.288 +      |> fold (Thy_Load.require o fst) uses;
   8.289  
   8.290      val deps =
   8.291        if known_thy name then get_deps name
   8.292 -      else init_deps NONE "" parents (map #1 uses);
   8.293 +      else init_deps NONE "" parents;
   8.294      val _ = change_thys (new_deps name parent_names (deps, NONE));
   8.295  
   8.296      val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
   8.297 @@ -527,16 +447,12 @@
   8.298  
   8.299      val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
   8.300      val theory'' =
   8.301 -      fold (fn x => Context.theory_map (exec_file x) o Theory.checkpoint) uses_now theory';
   8.302 +      fold (fn x => Context.theory_map (Thy_Load.exec_ml x) o Theory.checkpoint) uses_now theory';
   8.303    in theory'' end;
   8.304  
   8.305  fun end_theory theory =
   8.306 -  let
   8.307 -    val name = Context.theory_name theory;
   8.308 -    val _ = check_files name;
   8.309 -    val theory' = Theory.end_theory theory;
   8.310 -    val _ = change_thy name (fn (deps, _) => (deps, SOME theory'));
   8.311 -  in () end;
   8.312 +  let val name = Context.theory_name theory
   8.313 +  in if known_thy name then change_thy name (fn (deps, _) => (deps, SOME theory)) else () end;
   8.314  
   8.315  
   8.316  (* register existing theories *)
   8.317 @@ -546,14 +462,14 @@
   8.318      val _ = priority ("Registering theory " ^ quote name);
   8.319      val thy = get_theory name;
   8.320      val _ = map get_theory (get_parents name);
   8.321 -    val _ = check_unfinished error name;
   8.322 +    val _ = check_unfinished name;
   8.323      val _ = touch_thy name;
   8.324      val master = #master (Thy_Load.deps_thy Path.current name);
   8.325      val upd_time = #2 (Management_Data.get thy);
   8.326    in
   8.327      CRITICAL (fn () =>
   8.328 -     (change_deps name (Option.map
   8.329 -       (fn {parents, files, ...} => make_deps upd_time (SOME master) "" parents files));
   8.330 +     (change_deps name (Option.map (fn {parents, ...} =>
   8.331 +        make_deps upd_time (SOME master) "" parents));
   8.332        perform Update name))
   8.333    end;
   8.334  
     9.1 --- a/src/Pure/Thy/thy_load.ML	Fri Jul 23 18:42:46 2010 +0200
     9.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Jul 24 12:14:53 2010 +0200
     9.3 @@ -17,6 +17,10 @@
     9.4  signature THY_LOAD =
     9.5  sig
     9.6    include BASIC_THY_LOAD
     9.7 +  val master_directory: theory -> Path.T
     9.8 +  val init: Path.T -> theory -> theory
     9.9 +  val require: Path.T -> theory -> theory
    9.10 +  val provide: Path.T * (Path.T * File.ident) -> theory -> theory
    9.11    val ml_path: string -> Path.T
    9.12    val thy_path: string -> Path.T
    9.13    val split_thy_path: Path.T -> Path.T * string
    9.14 @@ -26,12 +30,57 @@
    9.15    val check_thy: Path.T -> string -> Path.T * File.ident
    9.16    val deps_thy: Path.T -> string ->
    9.17     {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
    9.18 -  val load_ml: Path.T -> Path.T -> Path.T * File.ident
    9.19 +  val loaded_files: theory -> Path.T list
    9.20 +  val check_loaded: theory -> unit
    9.21 +  val all_current: theory -> bool
    9.22 +  val provide_file: Path.T -> theory -> theory
    9.23 +  val use_ml: Path.T -> unit
    9.24 +  val exec_ml: Path.T -> generic_theory -> generic_theory
    9.25  end;
    9.26  
    9.27  structure Thy_Load: THY_LOAD =
    9.28  struct
    9.29  
    9.30 +(* manage source files *)
    9.31 +
    9.32 +type files =
    9.33 + {master_dir: Path.T,                                 (*master directory of theory source*)
    9.34 +  required: Path.T list,                              (*source path*)
    9.35 +  provided: (Path.T * (Path.T * File.ident)) list};   (*source path, physical path, identifier*)
    9.36 +
    9.37 +fun make_files (master_dir, required, provided): files =
    9.38 + {master_dir = master_dir, required = required, provided = provided};
    9.39 +
    9.40 +structure Files = Theory_Data
    9.41 +(
    9.42 +  type T = files;
    9.43 +  val empty = make_files (Path.current, [], []);
    9.44 +  fun extend _ = empty;
    9.45 +  fun merge _ = empty;
    9.46 +);
    9.47 +
    9.48 +fun map_files f =
    9.49 +  Files.map (fn {master_dir, required, provided} =>
    9.50 +    make_files (f (master_dir, required, provided)));
    9.51 +
    9.52 +
    9.53 +val master_directory = #master_dir o Files.get;
    9.54 +
    9.55 +fun init master_dir = map_files (fn _ => (master_dir, [], []));
    9.56 +
    9.57 +fun require src_path =
    9.58 +  map_files (fn (master_dir, required, provided) =>
    9.59 +    if member (op =) required src_path then
    9.60 +      error ("Duplicate source file dependency: " ^ Path.implode src_path)
    9.61 +    else (master_dir, src_path :: required, provided));
    9.62 +
    9.63 +fun provide (src_path, path_info) =
    9.64 +  map_files (fn (master_dir, required, provided) =>
    9.65 +    if AList.defined (op =) provided src_path then
    9.66 +      error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
    9.67 +    else (master_dir, required, (src_path, path_info) :: provided));
    9.68 +
    9.69 +
    9.70  (* maintain load path *)
    9.71  
    9.72  local val load_path = Unsynchronized.ref [Path.current] in
    9.73 @@ -121,13 +170,56 @@
    9.74    in {master = master, text = text, imports = imports, uses = uses} end;
    9.75  
    9.76  
    9.77 -(* ML files *)
    9.78 +
    9.79 +(* loaded files *)
    9.80 +
    9.81 +val loaded_files = map (#1 o #2) o #provided o Files.get;
    9.82  
    9.83 -fun load_ml dir raw_path =
    9.84 +fun check_loaded thy =
    9.85 +  let
    9.86 +    val {required, provided, ...} = Files.get thy;
    9.87 +    val provided_paths = map #1 provided;
    9.88 +    val _ =
    9.89 +      (case subtract (op =) provided_paths required of
    9.90 +        [] => NONE
    9.91 +      | bad => error ("Pending source file dependencies: " ^ commas (map Path.implode (rev bad))));
    9.92 +    val _ =
    9.93 +      (case subtract (op =) required provided_paths of
    9.94 +        [] => NONE
    9.95 +      | bad => error ("Undeclared source file dependencies: " ^ commas (map Path.implode (rev bad))));
    9.96 +  in () end;
    9.97 +
    9.98 +fun all_current thy =
    9.99    let
   9.100 -    val (path, id) = check_file dir raw_path;
   9.101 -    val _ = ML_Context.eval_file path;
   9.102 -  in (path, id) end;
   9.103 +    val {master_dir, provided, ...} = Files.get thy;
   9.104 +    fun current (src_path, path_info) =
   9.105 +      (case test_file master_dir src_path of
   9.106 +        NONE => false
   9.107 +      | SOME path_info' => eq_snd (op =) (path_info, path_info'));
   9.108 +  in can check_loaded thy andalso forall current provided end;
   9.109 +
   9.110 +
   9.111 +(* provide files *)
   9.112 +
   9.113 +fun provide_file src_path thy =
   9.114 +  provide (src_path, check_file (master_directory thy) src_path) thy;
   9.115 +
   9.116 +fun use_ml src_path =
   9.117 +  if is_none (Context.thread_data ()) then
   9.118 +    ML_Context.eval_file (#1 (check_file Path.current src_path))
   9.119 +  else
   9.120 +    let
   9.121 +      val thy = ML_Context.the_global_context ();
   9.122 +      val (path, info) = check_file (master_directory thy) src_path;
   9.123 +
   9.124 +      val _ = ML_Context.eval_file path;
   9.125 +      val _ = Context.>> Local_Theory.propagate_ml_env;
   9.126 +
   9.127 +      val provide = provide (src_path, (path, info));
   9.128 +      val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
   9.129 +    in () end
   9.130 +
   9.131 +fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
   9.132  
   9.133  end;
   9.134  
    10.1 --- a/src/Pure/pure_setup.ML	Fri Jul 23 18:42:46 2010 +0200
    10.2 +++ b/src/Pure/pure_setup.ML	Sat Jul 24 12:14:53 2010 +0200
    10.3 @@ -51,7 +51,8 @@
    10.4  
    10.5  (* ML toplevel use commands *)
    10.6  
    10.7 -fun use name = Toplevel.program (fn () => Thy_Info.use name);
    10.8 +fun use name = Toplevel.program (fn () => Thy_Load.use_ml (Path.explode name));
    10.9 +
   10.10  fun use_thys name = Toplevel.program (fn () => Thy_Info.use_thys name);
   10.11  fun use_thy name = Toplevel.program (fn () => Thy_Info.use_thy name);
   10.12