15 val is_finished: string -> bool |
15 val is_finished: string -> bool |
16 val master_directory: string -> Path.T |
16 val master_directory: string -> Path.T |
17 val loaded_files: string -> Path.T list |
17 val loaded_files: string -> Path.T list |
18 val remove_thy: string -> unit |
18 val remove_thy: string -> unit |
19 val kill_thy: string -> unit |
19 val kill_thy: string -> unit |
20 val use_theories: {last_timing: Toplevel.transition -> Time.time, master_dir: Path.T} -> |
20 val use_theories: {last_timing: Toplevel.transition -> Time.time option, master_dir: Path.T} -> |
21 (string * Position.T) list -> unit |
21 (string * Position.T) list -> unit |
22 val use_thys: (string * Position.T) list -> unit |
22 val use_thys: (string * Position.T) list -> unit |
23 val use_thy: string * Position.T -> unit |
23 val use_thy: string * Position.T -> unit |
24 val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory |
24 val toplevel_begin_theory: Path.T -> Thy_Header.header -> theory |
25 val register_thy: theory -> unit |
25 val register_thy: theory -> unit |
172 fun result_theory (Result {theory, ...}) = theory; |
172 fun result_theory (Result {theory, ...}) = theory; |
173 fun result_present (Result {present, ...}) = present; |
173 fun result_present (Result {present, ...}) = present; |
174 fun result_commit (Result {commit, ...}) = commit; |
174 fun result_commit (Result {commit, ...}) = commit; |
175 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); |
175 fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); |
176 |
176 |
177 fun join_proofs (Result {theory, id, present, ...}) = |
177 fun join_proofs (Result {theory, id, ...}) = |
178 let |
178 let |
179 val result1 = Exn.capture Thm.join_theory_proofs theory; |
179 val result1 = Exn.capture Thm.join_theory_proofs theory; |
180 val results2 = Future.join_results (Goal.peek_futures id); |
180 val results2 = Future.join_results (Goal.peek_futures id); |
181 in result1 :: results2 end; |
181 in result1 :: results2 end; |
182 |
182 |
349 (* use_thy *) |
349 (* use_thy *) |
350 |
350 |
351 fun use_theories {last_timing, master_dir} imports = |
351 fun use_theories {last_timing, master_dir} imports = |
352 schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty)); |
352 schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty)); |
353 |
353 |
354 val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current}; |
354 val use_thys = use_theories {last_timing = K NONE, master_dir = Path.current}; |
355 val use_thy = use_thys o single; |
355 val use_thy = use_thys o single; |
356 |
356 |
357 |
357 |
358 (* toplevel begin theory -- without maintaining database *) |
358 (* toplevel begin theory -- without maintaining database *) |
359 |
359 |
360 fun toplevel_begin_theory master_dir (header: Thy_Header.header) = |
360 fun toplevel_begin_theory master_dir (header: Thy_Header.header) = |
361 let |
361 let |
362 val {name = (name, _), imports, ...} = header; |
362 val {name = (name, _), imports, ...} = header; |
363 val _ = kill_thy name; |
363 val _ = kill_thy name; |
364 val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports; |
364 val _ = use_theories {last_timing = K NONE, master_dir = master_dir} imports; |
365 val _ = Thy_Header.define_keywords header; |
365 val _ = Thy_Header.define_keywords header; |
366 val parents = map (get_theory o base_name o fst) imports; |
366 val parents = map (get_theory o base_name o fst) imports; |
367 in Thy_Load.begin_theory master_dir header parents end; |
367 in Thy_Load.begin_theory master_dir header parents end; |
368 |
368 |
369 |
369 |