simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database;
Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command;
added Thy_Load.begin_theory for clarity;
structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader;
moved some basic commands from isar_cmd.ML to isar_syn.ML;
misc tuning and simplification;
1.1 --- a/src/Pure/General/secure.ML Tue Jul 27 12:59:22 2010 +0200
1.2 +++ b/src/Pure/General/secure.ML Tue Jul 27 22:00:26 2010 +0200
1.3 @@ -57,7 +57,7 @@
1.4 fun commit () = use_global "commit();"; (*commit is dynamically bound!*)
1.5
1.6 fun Isar_setup () = use_global "open Unsynchronized;";
1.7 -fun PG_setup () = use_global "structure ThyLoad = Thy_Load;";
1.8 +fun PG_setup () = use_global "structure ThyLoad = ProofGeneral.ThyLoad;";
1.9
1.10
1.11 (* shell commands *)
2.1 --- a/src/Pure/Isar/isar_cmd.ML Tue Jul 27 12:59:22 2010 +0200
2.2 +++ b/src/Pure/Isar/isar_cmd.ML Tue Jul 27 22:00:26 2010 +0200
2.3 @@ -34,10 +34,6 @@
2.4 val immediate_proof: Toplevel.transition -> Toplevel.transition
2.5 val done_proof: Toplevel.transition -> Toplevel.transition
2.6 val skip_proof: Toplevel.transition -> Toplevel.transition
2.7 - val init_theory: string * string list * (string * bool) list ->
2.8 - Toplevel.transition -> Toplevel.transition
2.9 - val exit: Toplevel.transition -> Toplevel.transition
2.10 - val quit: Toplevel.transition -> Toplevel.transition
2.11 val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
2.12 val disable_pr: Toplevel.transition -> Toplevel.transition
2.13 val enable_pr: Toplevel.transition -> Toplevel.transition
2.14 @@ -271,19 +267,6 @@
2.15 val skip_proof = local_skip_proof o global_skip_proof;
2.16
2.17
2.18 -(* init and exit *)
2.19 -
2.20 -fun init_theory (name, imports, uses) =
2.21 - Toplevel.init_theory name
2.22 - (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses));
2.23 -
2.24 -val exit = Toplevel.keep (fn state =>
2.25 - (Context.set_thread_data (try Toplevel.generic_theory_of state);
2.26 - raise Toplevel.TERMINATE));
2.27 -
2.28 -val quit = Toplevel.imperative quit;
2.29 -
2.30 -
2.31 (* print state *)
2.32
2.33 fun set_limit _ NONE = ()
3.1 --- a/src/Pure/Isar/isar_syn.ML Tue Jul 27 12:59:22 2010 +0200
3.2 +++ b/src/Pure/Isar/isar_syn.ML Tue Jul 27 22:00:26 2010 +0200
3.3 @@ -28,7 +28,10 @@
3.4
3.5 val _ =
3.6 Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
3.7 - (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
3.8 + (Thy_Header.args >> (fn (name, imports, uses) =>
3.9 + Toplevel.print o
3.10 + Toplevel.init_theory name
3.11 + (fn () => Thy_Info.toplevel_begin_theory name imports (map (apfst Path.explode) uses))));
3.12
3.13 val _ =
3.14 Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
3.15 @@ -992,11 +995,14 @@
3.16
3.17 val _ =
3.18 Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
3.19 - (Parse.opt_unit >> (Toplevel.no_timing oo K Isar_Cmd.quit));
3.20 + (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
3.21
3.22 val _ =
3.23 Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
3.24 - (Scan.succeed (Toplevel.no_timing o Isar_Cmd.exit));
3.25 + (Scan.succeed
3.26 + (Toplevel.no_timing o Toplevel.keep (fn state =>
3.27 + (Context.set_thread_data (try Toplevel.generic_theory_of state);
3.28 + raise Toplevel.TERMINATE))));
3.29
3.30 end;
3.31
4.1 --- a/src/Pure/Isar/outer_syntax.ML Tue Jul 27 12:59:22 2010 +0200
4.2 +++ b/src/Pure/Isar/outer_syntax.ML Tue Jul 27 22:00:26 2010 +0200
4.3 @@ -31,7 +31,7 @@
4.4 type isar
4.5 val isar: bool -> isar
4.6 val prepare_command: Position.T -> string -> Toplevel.transition
4.7 - val load_thy: string -> Position.T -> string -> (unit -> unit) * theory
4.8 + val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory
4.9 end;
4.10
4.11 structure Outer_Syntax: OUTER_SYNTAX =
4.12 @@ -249,9 +249,9 @@
4.13 handle ERROR msg => (Toplevel.malformed range_pos msg, true)
4.14 end;
4.15
4.16 -fun prepare_unit commands (cmd, proof, proper_proof) =
4.17 +fun prepare_unit commands init (cmd, proof, proper_proof) =
4.18 let
4.19 - val (tr, proper_cmd) = prepare_span commands cmd;
4.20 + val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
4.21 val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
4.22 in
4.23 if proper_cmd andalso proper_proof then [(tr, proof_trs)]
4.24 @@ -268,7 +268,7 @@
4.25
4.26 (* load_thy *)
4.27
4.28 -fun load_thy name pos text =
4.29 +fun load_thy name init pos text =
4.30 let
4.31 val (lexs, commands) = get_syntax ();
4.32 val time = ! Output.timing;
4.33 @@ -279,7 +279,7 @@
4.34 val spans = Source.exhaust (Thy_Syntax.span_source toks);
4.35 val _ = List.app Thy_Syntax.report_span spans;
4.36 val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
4.37 - |> Par_List.map (prepare_unit commands) |> flat;
4.38 + |> Par_List.map (prepare_unit commands init) |> flat;
4.39
4.40 val _ = Present.theory_source name
4.41 (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
5.1 --- a/src/Pure/Isar/toplevel.ML Tue Jul 27 12:59:22 2010 +0200
5.2 +++ b/src/Pure/Isar/toplevel.ML Tue Jul 27 22:00:26 2010 +0200
5.3 @@ -46,7 +46,8 @@
5.4 val interactive: bool -> transition -> transition
5.5 val print: transition -> transition
5.6 val no_timing: transition -> transition
5.7 - val init_theory: string -> (bool -> theory) -> transition -> transition
5.8 + val init_theory: string -> (unit -> theory) -> transition -> transition
5.9 + val modify_init: (unit -> theory) -> transition -> transition
5.10 val exit: transition -> transition
5.11 val keep: (state -> unit) -> transition -> transition
5.12 val keep': (bool -> state -> unit) -> transition -> transition
5.13 @@ -295,16 +296,16 @@
5.14 (* primitive transitions *)
5.15
5.16 datatype trans =
5.17 - Init of string * (bool -> theory) | (*theory name, init*)
5.18 + Init of string * (unit -> theory) | (*theory name, init*)
5.19 Exit | (*formal exit of theory*)
5.20 Keep of bool -> state -> unit | (*peek at state*)
5.21 Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*)
5.22
5.23 local
5.24
5.25 -fun apply_tr int (Init (_, f)) (State (NONE, _)) =
5.26 +fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
5.27 State (SOME (Theory (Context.Theory
5.28 - (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE)
5.29 + (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
5.30 | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
5.31 State (NONE, prev)
5.32 | apply_tr int (Keep f) state =
5.33 @@ -394,6 +395,12 @@
5.34 (* basic transitions *)
5.35
5.36 fun init_theory name f = add_trans (Init (name, f));
5.37 +
5.38 +fun modify_init f tr =
5.39 + (case init_of tr of
5.40 + SOME name => init_theory name f (reset_trans tr)
5.41 + | NONE => tr);
5.42 +
5.43 val exit = add_trans Exit;
5.44 val keep' = add_trans o Keep;
5.45
6.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jul 27 12:59:22 2010 +0200
6.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Tue Jul 27 22:00:26 2010 +0200
6.3 @@ -8,9 +8,10 @@
6.4 signature PROOF_GENERAL =
6.5 sig
6.6 val test_markupN: string
6.7 + val sendback: string -> Pretty.T list -> unit
6.8 val init: bool -> unit
6.9 val init_outer_syntax: unit -> unit
6.10 - val sendback: string -> Pretty.T list -> unit
6.11 + structure ThyLoad: sig val add_path: string -> unit end
6.12 end;
6.13
6.14 structure ProofGeneral: PROOF_GENERAL =
6.15 @@ -130,19 +131,17 @@
6.16 (*liberal low-level version*)
6.17 val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
6.18
6.19 -val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
6.20 +val inform_file_retracted = Thy_Info.kill_thy o thy_name;
6.21
6.22 fun inform_file_processed file =
6.23 let
6.24 val name = thy_name file;
6.25 val _ = name = "" andalso error ("Bad file name: " ^ quote file);
6.26 val _ =
6.27 - if Thy_Info.known_thy name then
6.28 - Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
6.29 - handle ERROR msg =>
6.30 - (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
6.31 - tell_file_retracted (Thy_Header.thy_path name))
6.32 - else ();
6.33 + Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
6.34 + handle ERROR msg =>
6.35 + (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
6.36 + tell_file_retracted (Thy_Header.thy_path name))
6.37 val _ = Isar.init ();
6.38 in () end;
6.39
6.40 @@ -247,4 +246,12 @@
6.41 Secure.PG_setup ();
6.42 Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
6.43
6.44 +
6.45 +(* fake old ThyLoad -- with new semantics *)
6.46 +
6.47 +structure ThyLoad =
6.48 +struct
6.49 + val add_path = Thy_Load.set_master_path o Path.explode;
6.50 end;
6.51 +
6.52 +end;
7.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jul 27 12:59:22 2010 +0200
7.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Tue Jul 27 22:00:26 2010 +0200
7.3 @@ -217,11 +217,11 @@
7.4
7.5 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
7.6
7.7 -val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
7.8 +val inform_file_retracted = Thy_Info.kill_thy o thy_name;
7.9
7.10 fun inform_file_processed path state =
7.11 let val name = thy_name path in
7.12 - if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then
7.13 + if Toplevel.is_toplevel state then
7.14 Thy_Info.register_thy (Toplevel.end_theory Position.none state)
7.15 handle ERROR msg =>
7.16 (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
7.17 @@ -804,8 +804,7 @@
7.18 val filepath = PgipTypes.path_of_pgipurl url
7.19 val filedir = Path.dir filepath
7.20 val thy_name = Path.implode o #1 o Path.split_ext o Path.base
7.21 - val openfile_retract = Output.no_warnings_CRITICAL
7.22 - (Thy_Info.if_known_thy Thy_Info.remove_thy) o thy_name;
7.23 + val openfile_retract = Output.no_warnings_CRITICAL Thy_Info.kill_thy o thy_name;
7.24 in
7.25 case !currently_open_file of
7.26 SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^
8.1 --- a/src/Pure/Thy/thy_info.ML Tue Jul 27 12:59:22 2010 +0200
8.2 +++ b/src/Pure/Thy/thy_info.ML Tue Jul 27 22:00:26 2010 +0200
8.3 @@ -10,8 +10,6 @@
8.4 datatype action = Update | Outdate | Remove
8.5 val add_hook: (action -> string -> unit) -> unit
8.6 val get_names: unit -> string list
8.7 - val 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 val is_finished: string -> bool
8.12 @@ -23,7 +21,7 @@
8.13 val kill_thy: string -> unit
8.14 val use_thys: string list -> unit
8.15 val use_thy: string -> unit
8.16 - val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
8.17 + val toplevel_begin_theory: string -> string list -> (Path.T * bool) list -> theory
8.18 val register_thy: theory -> unit
8.19 val finish: unit -> unit
8.20 end;
8.21 @@ -60,6 +58,9 @@
8.22 fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
8.23 handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
8.24
8.25 +fun new_node name parents entry =
8.26 + Graph.new_node (name, entry) #> add_deps name parents;
8.27 +
8.28 fun upd_deps name entry G =
8.29 fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G
8.30 |> Graph.map_node name (K entry);
8.31 @@ -72,21 +73,18 @@
8.32 (* thy database *)
8.33
8.34 type deps =
8.35 - {update_time: int, (*symbolic time of update; negative value means outdated*)
8.36 - master: (Path.T * File.ident) option, (*master dependencies for thy file*)
8.37 - text: string, (*source text for thy*)
8.38 - parents: string list}; (*source specification of parents (partially qualified)*)
8.39 + {update_time: int, (*symbolic time of update; negative value means outdated*)
8.40 + master: (Path.T * File.ident), (*master dependencies for thy file*)
8.41 + parents: string list}; (*source specification of parents (partially qualified)*)
8.42
8.43 -fun make_deps update_time master text parents : deps =
8.44 - {update_time = update_time, master = master, text = text, parents = parents};
8.45 +fun make_deps update_time master parents : deps =
8.46 + {update_time = update_time, master = master, parents = parents};
8.47
8.48 -fun init_deps master text parents = SOME (make_deps ~1 master text parents);
8.49 +fun init_deps master parents = SOME (make_deps (serial ()) master parents);
8.50
8.51 -fun master_dir NONE = Path.current
8.52 - | master_dir (SOME (path, _)) = Path.dir path;
8.53 +fun master_dir (path, _) = Path.dir path;
8.54
8.55 -fun master_dir' (d: deps option) = the_default Path.current (Option.map (master_dir o #master) d);
8.56 -fun master_dir'' d = the_default Path.current (Option.map master_dir' d);
8.57 +fun master_dir' (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
8.58
8.59 fun base_name s = Path.implode (Path.base (Path.explode s));
8.60
8.61 @@ -112,7 +110,6 @@
8.62 SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
8.63
8.64 val known_thy = is_some o lookup_thy;
8.65 -fun if_known_thy f name = if known_thy name then f name else ();
8.66
8.67 fun get_thy name =
8.68 (case lookup_thy name of
8.69 @@ -128,7 +125,6 @@
8.70 val lookup_deps = Option.map #1 o lookup_thy;
8.71 val get_deps = #1 o get_thy;
8.72 fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
8.73 -fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory));
8.74
8.75 val is_finished = is_none o get_deps;
8.76 val master_directory = master_dir' o get_deps;
8.77 @@ -153,10 +149,7 @@
8.78 fun loaded_files name =
8.79 (case get_deps name of
8.80 NONE => []
8.81 - | SOME {master, ...} =>
8.82 - (case master of
8.83 - NONE => []
8.84 - | SOME (thy_path, _) => thy_path :: Thy_Load.loaded_files (get_theory name)));
8.85 + | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name));
8.86
8.87
8.88
8.89 @@ -180,8 +173,8 @@
8.90 fun outdate_thy name =
8.91 if is_finished name orelse is_outdated name then ()
8.92 else CRITICAL (fn () =>
8.93 - (change_deps name (Option.map (fn {master, text, parents, ...} =>
8.94 - make_deps ~1 master text parents)); perform Outdate name));
8.95 + (change_deps name (Option.map (fn {master, parents, ...} =>
8.96 + make_deps ~1 master parents)); perform Outdate name));
8.97
8.98 fun touch_thys names =
8.99 List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
8.100 @@ -191,136 +184,91 @@
8.101 end;
8.102
8.103
8.104 -(* management data *)
8.105 +(* abstract update time *)
8.106
8.107 -structure Management_Data = Theory_Data
8.108 +structure Update_Time = Theory_Data
8.109 (
8.110 - type T =
8.111 - Task_Queue.group option * (*worker thread group*)
8.112 - int; (*abstract update time*)
8.113 - val empty = (NONE, 0);
8.114 + type T = int;
8.115 + val empty = 0;
8.116 fun extend _ = empty;
8.117 fun merge _ = empty;
8.118 );
8.119
8.120 -val thy_ord = int_ord o pairself (#2 o Management_Data.get);
8.121 -
8.122 -
8.123 -(* pending proofs *)
8.124 -
8.125 -fun join_thy name =
8.126 - (case lookup_theory name of
8.127 - NONE => ()
8.128 - | SOME thy => PureThy.join_proofs thy);
8.129 -
8.130 -fun cancel_thy name =
8.131 - (case lookup_theory name of
8.132 - NONE => ()
8.133 - | SOME thy =>
8.134 - (case #1 (Management_Data.get thy) of
8.135 - NONE => ()
8.136 - | SOME group => Future.cancel_group group));
8.137 +val thy_ord = int_ord o pairself Update_Time.get;
8.138
8.139
8.140 (* remove theory *)
8.141
8.142 fun remove_thy name =
8.143 - if is_finished name then error (loader_msg "cannot remove finished theory" [name])
8.144 + if is_finished name then error (loader_msg "cannot change finished theory" [name])
8.145 else
8.146 let
8.147 val succs = thy_graph Graph.all_succs [name];
8.148 - val _ = List.app cancel_thy succs;
8.149 val _ = priority (loader_msg "removing" succs);
8.150 val _ = CRITICAL (fn () =>
8.151 (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)));
8.152 in () end;
8.153
8.154 -val kill_thy = if_known_thy remove_thy;
8.155 -
8.156 -
8.157 -(* load_thy *)
8.158 -
8.159 -fun required_by _ [] = ""
8.160 - | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
8.161 -
8.162 -fun load_thy upd_time initiators name =
8.163 - let
8.164 - val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
8.165 - fun corrupted () = error (loader_msg "corrupted dependency information" [name]);
8.166 - val (pos, text) =
8.167 - (case get_deps name of
8.168 - SOME {master = SOME (master_path, _), text, ...} =>
8.169 - if text = "" then corrupted ()
8.170 - else (Path.position master_path, text)
8.171 - | _ => corrupted ());
8.172 - val _ = touch_thy name;
8.173 - val _ =
8.174 - change_deps name (Option.map (fn {master, text, parents, ...} =>
8.175 - make_deps upd_time master text parents));
8.176 - val (after_load, theory) = Outer_Syntax.load_thy name pos text;
8.177 - val _ = put_theory name theory;
8.178 - val _ =
8.179 - CRITICAL (fn () =>
8.180 - (change_deps name
8.181 - (Option.map (fn {update_time, master, parents, ...} =>
8.182 - make_deps update_time master "" parents));
8.183 - perform Update name));
8.184 - in after_load end;
8.185 +fun kill_thy name =
8.186 + if known_thy name then remove_thy name
8.187 + else ();
8.188
8.189
8.190 (* scheduling loader tasks *)
8.191
8.192 -datatype task = Task of (unit -> unit -> unit) | Finished | Running;
8.193 -fun task_finished Finished = true | task_finished _ = false;
8.194 +datatype task =
8.195 + Task of string list * (theory list -> (theory * (unit -> unit))) |
8.196 + Finished of theory;
8.197 +
8.198 +fun task_finished (Task _) = false
8.199 + | task_finished (Finished _) = true;
8.200
8.201 local
8.202
8.203 +fun schedule_seq task_graph =
8.204 + ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
8.205 + (case Graph.get_node task_graph name of
8.206 + Task (parents, body) =>
8.207 + let
8.208 + val (thy, after_load) = body (map (the o Symtab.lookup tab) parents);
8.209 + val _ = after_load ();
8.210 + in Symtab.update (name, thy) tab end
8.211 + | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
8.212 +
8.213 fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
8.214 let
8.215 - val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
8.216 - (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
8.217 -
8.218 + val tasks = Graph.topological_order task_graph;
8.219 val par_proofs = ! parallel_proofs >= 1;
8.220
8.221 - fun fork (name, body) tab =
8.222 + val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
8.223 + (case Graph.get_node task_graph name of
8.224 + Task (parents, body) =>
8.225 + let
8.226 + val get = the o Symtab.lookup tab;
8.227 + val deps = map (`get) (Graph.imm_preds task_graph name);
8.228 + fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
8.229 +
8.230 + val future = Future.fork_deps (map #1 deps) (fn () =>
8.231 + (case map_filter failed deps of
8.232 + [] => body (map (#1 o Future.join o get) parents)
8.233 + | bad => error (loader_msg
8.234 + ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
8.235 + val future' =
8.236 + if par_proofs then future
8.237 + else Future.map (fn (thy, after_load) => (after_load (); (thy, I))) future;
8.238 + in Symtab.update (name, future') tab end
8.239 + | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
8.240 +
8.241 + val exns = tasks |> maps (fn name =>
8.242 let
8.243 - val deps = Graph.imm_preds task_graph name
8.244 - |> map_filter (fn parent =>
8.245 - (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
8.246 - fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
8.247 + val (thy, after_load) = Future.join (the (Symtab.lookup futures name));
8.248 + val _ = PureThy.join_proofs thy;
8.249 + val _ = after_load ();
8.250 + in [] end handle exn => [exn]) |> rev;
8.251
8.252 - val future = Future.fork_deps (map #2 deps) (fn () =>
8.253 - (case map_filter failed deps of
8.254 - [] => body ()
8.255 - | bad => error (loader_msg
8.256 - ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
8.257 - val future' =
8.258 - if par_proofs then future
8.259 - else Future.map (fn after_load => (after_load (); fn () => ())) future;
8.260 - in Symtab.update (name, future') tab end;
8.261 -
8.262 - val futures = fold fork tasks Symtab.empty;
8.263 -
8.264 - val failed = tasks |> maps (fn (name, _) =>
8.265 - let
8.266 - val after_load = Future.join (the (Symtab.lookup futures name));
8.267 - val _ = join_thy name;
8.268 - val _ = after_load ();
8.269 - in [] end handle exn => [(name, exn)]) |> rev;
8.270 -
8.271 - val _ = List.app (kill_thy o #1) failed;
8.272 - val _ = Exn.release_all (map (Exn.Exn o #2) failed);
8.273 + val _ = Exn.release_all (map Exn.Exn exns);
8.274 in () end) ();
8.275
8.276 -fun schedule_seq tasks =
8.277 - Graph.topological_order tasks
8.278 - |> List.app (fn name =>
8.279 - (case Graph.get_node tasks name of
8.280 - Task body =>
8.281 - let val after_load = body ()
8.282 - in after_load () handle exn => (kill_thy name; reraise exn) end
8.283 - | _ => ()));
8.284 -
8.285 in
8.286
8.287 fun schedule_tasks tasks =
8.288 @@ -337,34 +285,56 @@
8.289
8.290 local
8.291
8.292 +fun required_by _ [] = ""
8.293 + | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
8.294 +
8.295 +fun load_thy initiators (deps: deps) text dir name parent_thys =
8.296 + let
8.297 + val _ = kill_thy name;
8.298 + val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
8.299 +
8.300 + val {update_time, master = (thy_path, _), ...} = deps;
8.301 + val pos = Path.position thy_path;
8.302 + val uses =
8.303 + map (apfst Path.explode) (#3 (Thy_Header.read pos (Source.of_string_limited 8000 text)));
8.304 + fun init () =
8.305 + Thy_Load.begin_theory dir name parent_thys uses
8.306 + |> Present.begin_theory update_time dir uses
8.307 + |> Update_Time.put update_time;
8.308 +
8.309 + val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
8.310 +
8.311 + val parent_names = map Context.theory_name parent_thys;
8.312 + fun after_load' () =
8.313 + (after_load ();
8.314 + CRITICAL (fn () =>
8.315 + (change_thys (new_node name parent_names (SOME deps, SOME theory));
8.316 + perform Update name)));
8.317 +
8.318 + in (theory, after_load') end;
8.319 +
8.320 fun check_deps dir name =
8.321 (case lookup_deps name of
8.322 SOME NONE => (true, NONE, get_parents name)
8.323 | NONE =>
8.324 - let val {master, text, imports = parents, ...} = Thy_Load.deps_thy dir name
8.325 - in (false, init_deps (SOME master) text parents, parents) end
8.326 - | SOME (SOME {update_time, master, text, parents}) =>
8.327 - let
8.328 - val (thy_path, thy_id) = Thy_Load.check_thy dir name;
8.329 - val master' = SOME (thy_path, thy_id);
8.330 - in
8.331 - if Option.map #2 master <> SOME thy_id then
8.332 - let val {text = text', imports = parents', ...} = Thy_Load.deps_thy dir name;
8.333 - in (false, init_deps master' text' parents', parents') end
8.334 + let val {master, imports = parents, ...} = Thy_Load.deps_thy dir name
8.335 + in (false, init_deps master parents, parents) end
8.336 + | SOME (SOME {update_time, master, parents}) =>
8.337 + let val master' = Thy_Load.check_thy dir name in
8.338 + if #2 master <> #2 master' then
8.339 + let val {imports = parents', ...} = Thy_Load.deps_thy dir name;
8.340 + in (false, init_deps master' parents', parents') end
8.341 else
8.342 let
8.343 val current =
8.344 (case lookup_theory name of
8.345 NONE => false
8.346 | SOME theory => update_time >= 0 andalso Thy_Load.all_current theory);
8.347 - val update_time' = if current then update_time else ~1;
8.348 - val deps' = SOME (make_deps update_time' master' text parents);
8.349 + val update_time' = if current then update_time else serial ();
8.350 + val deps' = SOME (make_deps update_time' master' parents);
8.351 in (current, deps', parents) end
8.352 end);
8.353
8.354 -fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents}) =
8.355 - SOME (make_deps update_time master (File.read path) parents);
8.356 -
8.357 in
8.358
8.359 fun require_thys initiators dir strs tasks =
8.360 @@ -386,21 +356,22 @@
8.361 required_by "\n" initiators);
8.362 val parent_names = map base_name parents;
8.363
8.364 - val (parents_current, tasks_graph') =
8.365 + val (parents_current, tasks') =
8.366 require_thys (name :: initiators) (Path.append dir (master_dir' deps)) parents tasks;
8.367
8.368 val all_current = current andalso parents_current;
8.369 +
8.370 + (* FIXME ?? *)
8.371 val _ = if not all_current andalso known_thy name then outdate_thy name else ();
8.372 - val entry =
8.373 - if all_current then (deps, SOME (get_theory name))
8.374 - else (read_text deps, NONE);
8.375 - val _ = change_thys (new_deps name parent_names entry);
8.376
8.377 - val upd_time = serial ();
8.378 - val tasks_graph'' = tasks_graph' |> new_deps name parent_names
8.379 - (if all_current then Finished
8.380 - else Task (fn () => load_thy upd_time initiators name));
8.381 - in (all_current, tasks_graph'') end)
8.382 + val task =
8.383 + if all_current then Finished (get_theory name)
8.384 + else
8.385 + let
8.386 + val SOME {master = (thy_path, _), ...} = deps;
8.387 + val text = File.read thy_path;
8.388 + in Task (parent_names, load_thy initiators (the deps) text dir' name) end;
8.389 + in (all_current, new_node name parent_names task tasks') end)
8.390 end;
8.391
8.392 end;
8.393 @@ -417,56 +388,32 @@
8.394
8.395 (* begin theory *)
8.396
8.397 -fun check_unfinished name =
8.398 - if known_thy name andalso is_finished name then
8.399 - error (loader_msg "cannot update finished theory" [name])
8.400 - else ();
8.401 +fun toplevel_begin_theory name imports uses =
8.402 + let
8.403 + val dir = Thy_Load.get_master_path ();
8.404 + val _ = kill_thy name;
8.405 + val _ = use_thys_dir dir imports;
8.406 + val parents = map (get_theory o base_name) imports;
8.407 + in Thy_Load.begin_theory dir name parents uses end;
8.408
8.409 -fun begin_theory name parents uses int =
8.410 - let
8.411 - val parent_names = map base_name parents;
8.412 - val dir = master_dir'' (lookup_deps name);
8.413 - val _ = check_unfinished name;
8.414 - val _ = if int then use_thys_dir dir parents else ();
8.415
8.416 - val theory =
8.417 - Theory.begin_theory name (map get_theory parent_names)
8.418 - |> Thy_Load.init dir
8.419 - |> fold (Thy_Load.require o fst) uses;
8.420 -
8.421 - val deps =
8.422 - if known_thy name then get_deps name
8.423 - else init_deps NONE "" parents;
8.424 - val _ = change_thys (new_deps name parent_names (deps, NONE));
8.425 -
8.426 - val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
8.427 - val update_time = if update_time > 0 then update_time else serial ();
8.428 - val theory' = theory
8.429 - |> Management_Data.put (Future.worker_group (), update_time)
8.430 - |> Present.begin_theory update_time dir uses;
8.431 -
8.432 - val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
8.433 - val theory'' =
8.434 - fold (fn x => Context.theory_map (Thy_Load.exec_ml x) o Theory.checkpoint) uses_now theory';
8.435 - in theory'' end;
8.436 -
8.437 -
8.438 -(* register existing theories *)
8.439 +(* register theory *)
8.440
8.441 fun register_thy theory =
8.442 let
8.443 val name = Context.theory_name theory;
8.444 + (* FIXME kill_thy name (??) *)
8.445 val _ = priority ("Registering theory " ^ quote name);
8.446 val parent_names = map Context.theory_name (Theory.parents_of theory);
8.447 val _ = map get_theory parent_names;
8.448
8.449 val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
8.450 - val update_time = #2 (Management_Data.get theory);
8.451 + val update_time = Update_Time.get theory;
8.452 val parents =
8.453 (case lookup_deps name of
8.454 SOME (SOME {parents, ...}) => parents
8.455 | _ => parent_names);
8.456 - val deps = make_deps update_time (SOME master) "" parents;
8.457 + val deps = make_deps update_time master parents;
8.458 in
8.459 CRITICAL (fn () =>
8.460 (if known_thy name then
9.1 --- a/src/Pure/Thy/thy_load.ML Tue Jul 27 12:59:22 2010 +0200
9.2 +++ b/src/Pure/Thy/thy_load.ML Tue Jul 27 22:00:26 2010 +0200
9.3 @@ -17,8 +17,9 @@
9.4 signature THY_LOAD =
9.5 sig
9.6 include BASIC_THY_LOAD
9.7 + val set_master_path: Path.T -> unit
9.8 + val get_master_path: unit -> Path.T
9.9 val master_directory: theory -> Path.T
9.10 - val init: Path.T -> theory -> theory
9.11 val require: Path.T -> theory -> theory
9.12 val provide: Path.T * (Path.T * File.ident) -> theory -> theory
9.13 val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
9.14 @@ -31,6 +32,7 @@
9.15 val provide_file: Path.T -> theory -> theory
9.16 val use_ml: Path.T -> unit
9.17 val exec_ml: Path.T -> generic_theory -> generic_theory
9.18 + val begin_theory: Path.T -> string -> theory list -> (Path.T * bool) list -> theory
9.19 end;
9.20
9.21 structure Thy_Load: THY_LOAD =
9.22 @@ -61,7 +63,7 @@
9.23
9.24 val master_directory = #master_dir o Files.get;
9.25
9.26 -fun init master_dir = map_files (fn _ => (master_dir, [], []));
9.27 +fun master dir = map_files (fn _ => (dir, [], []));
9.28
9.29 fun require src_path =
9.30 map_files (fn (master_dir, required, provided) =>
9.31 @@ -76,9 +78,12 @@
9.32 else (master_dir, required, (src_path, path_info) :: provided));
9.33
9.34
9.35 -(* maintain load path *)
9.36 +(* maintain default paths *)
9.37
9.38 -local val load_path = Unsynchronized.ref [Path.current] in
9.39 +local
9.40 + val load_path = Unsynchronized.ref [Path.current];
9.41 + val master_path = Unsynchronized.ref Path.current;
9.42 +in
9.43
9.44 fun show_path () = map Path.implode (! load_path);
9.45
9.46 @@ -97,6 +102,9 @@
9.47 fun search_path dir path =
9.48 distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
9.49
9.50 +fun set_master_path path = master_path := path;
9.51 +fun get_master_path () = ! master_path;
9.52 +
9.53 end;
9.54
9.55
9.56 @@ -202,6 +210,16 @@
9.57
9.58 fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
9.59
9.60 +
9.61 +(* begin theory *)
9.62 +
9.63 +fun begin_theory dir name parents uses =
9.64 + Theory.begin_theory name parents
9.65 + |> master dir
9.66 + |> fold (require o fst) uses
9.67 + |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
9.68 + |> Theory.checkpoint;
9.69 +
9.70 end;
9.71
9.72 structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;