author  wenzelm 
Mon, 04 Mar 2013 11:36:16 +0100  
changeset 51331  e7fab0b5dbe7 
parent 51330  f249bd08d851 
child 51423  e5f9a6d9ca82 
permissions  rwrr 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

1 
(* Title: Pure/Thy/thy_info.ML 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

2 
Author: Markus Wenzel, TU Muenchen 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

3 

37978
548f3f165d05
simplified Thy_Header.read  include Source.of_string_limited here;
wenzelm
parents:
37977
diff
changeset

4 
Global theory info database, with autoloading according to theory and 
15801  5 
file dependencies. 
3976  6 
*) 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

7 

6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

8 
signature THY_INFO = 
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

9 
sig 
37981
9a15982f41fe
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
wenzelm
parents:
37980
diff
changeset

10 
datatype action = Update  Remove 
7099  11 
val add_hook: (action > string > unit) > unit 
26614  12 
val get_names: unit > string list 
7288  13 
val lookup_theory: string > theory option 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

14 
val get_theory: string > theory 
24563  15 
val is_finished: string > bool 
26983  16 
val master_directory: string > Path.T 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

17 
val loaded_files: string > Path.T list 
29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

18 
val remove_thy: string > unit 
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

19 
val kill_thy: string > unit 
51228  20 
val use_theories: {last_timing: Toplevel.transition > Time.time, master_dir: Path.T} > 
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

21 
(string * Position.T) list > unit 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

22 
val use_thys: (string * Position.T) list > unit 
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

23 
val use_thy: string * Position.T > unit 
46938
cda018294515
some support for outer syntax keyword declarations within theory header;
wenzelm
parents:
46774
diff
changeset

24 
val toplevel_begin_theory: Path.T > Thy_Header.header > theory 
37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset

25 
val register_thy: theory > unit 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

26 
val finish: unit > unit 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

27 
end; 
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

28 

37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
36953
diff
changeset

29 
structure Thy_Info: THY_INFO = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

30 
struct 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

31 

7099  32 
(** theory loader actions and hooks **) 
33 

37981
9a15982f41fe
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
wenzelm
parents:
37980
diff
changeset

34 
datatype action = Update  Remove; 
7099  35 

36 
local 

43640  37 
val hooks = Synchronized.var "Thy_Info.hooks" ([]: (action > string > unit) list); 
7099  38 
in 
43640  39 
fun add_hook f = Synchronized.change hooks (cons f); 
40 
fun perform action name = 

41 
List.app (fn f => (try (fn () => f action name) (); ())) (Synchronized.value hooks); 

7099  42 
end; 
43 

44 

45 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

46 
(** thy database **) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

47 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

48 
(* messages *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

49 

23871  50 
fun loader_msg txt [] = "Theory loader: " ^ txt 
51 
 loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names; 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

52 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

53 
val show_path = space_implode " via " o map quote; 
9332  54 
fun cycle_msg names = loader_msg ("cyclic dependency of " ^ show_path names) []; 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

55 

6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

56 

6666  57 
(* derived graph operations *) 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

58 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

59 
fun add_deps name parents G = String_Graph.add_deps_acyclic (name, parents) G 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

60 
handle String_Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

61 

37984
f26352bd82cf
clarified register_thy: clean slate via kill_thy, more precise CRITICAL section;
wenzelm
parents:
37981
diff
changeset

62 
fun new_entry name parents entry = 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

63 
String_Graph.new_node (name, entry) #> add_deps name parents; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

64 

3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

65 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

66 
(* thy database *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

67 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

68 
type deps = 
41955
703ea96b13c6
files are identified via SHA1 digests  discontinued ISABELLE_FILE_IDENT;
wenzelm
parents:
41678
diff
changeset

69 
{master: (Path.T * SHA1.digest), (*master dependencies for thy file*) 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

70 
imports: (string * Position.T) list}; (*source specification of imports (partially qualified)*) 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

71 

38148
d2f3c8d4a89f
uniform naming of imports (source specification) vs. parents (thy node names) vs. parent_thys (theory values);
wenzelm
parents:
38147
diff
changeset

72 
fun make_deps master imports : deps = {master = master, imports = imports}; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

73 

37980
b8c3d4dc1e3e
avoid repeated File.read for theory text (as before);
wenzelm
parents:
37979
diff
changeset

74 
fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d); 
44225
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset

75 
fun base_name s = Path.implode (Path.base (Path.explode s)); 
23967  76 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

77 
local 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

78 
val database = 
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

79 
Unsynchronized.ref (String_Graph.empty: (deps option * theory option) String_Graph.T); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

80 
in 
6362  81 
fun get_thys () = ! database; 
38145
675827e61eb9
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
wenzelm
parents:
38143
diff
changeset

82 
fun change_thys f = NAMED_CRITICAL "Thy_Info" (fn () => Unsynchronized.change database f); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

83 
end; 
5209  84 

85 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

86 
(* access thy graph *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

87 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

88 
fun thy_graph f x = f (get_thys ()) x; 
9417  89 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

90 
fun get_names () = String_Graph.topological_order (get_thys ()); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

91 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

92 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

93 
(* access thy *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

94 

7935  95 
fun lookup_thy name = 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

96 
SOME (thy_graph String_Graph.get_node name) handle String_Graph.UNDEF _ => NONE; 
7935  97 

16047  98 
val known_thy = is_some o lookup_thy; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

99 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

100 
fun get_thy name = 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

101 
(case lookup_thy name of 
15531  102 
SOME thy => thy 
103 
 NONE => error (loader_msg "nothing known about theory" [name])); 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

104 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

105 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

106 
(* access deps *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

107 

15570  108 
val lookup_deps = Option.map #1 o lookup_thy; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

109 
val get_deps = #1 o get_thy; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

110 

26983  111 
val is_finished = is_none o get_deps; 
37980
b8c3d4dc1e3e
avoid repeated File.read for theory text (as before);
wenzelm
parents:
37979
diff
changeset

112 
val master_directory = master_dir o get_deps; 
7191  113 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

114 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

115 
(* access theory *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

116 

7687  117 
fun lookup_theory name = 
118 
(case lookup_thy name of 

38142  119 
SOME (_, SOME theory) => SOME theory 
15531  120 
 _ => NONE); 
7288  121 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

122 
fun get_theory name = 
7288  123 
(case lookup_theory name of 
23871  124 
SOME theory => theory 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

125 
 _ => error (loader_msg "undefined theory entry for" [name])); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

126 

44337
d453faed4815
clarified get_imports  should not rely on accidental order within graph;
wenzelm
parents:
44302
diff
changeset

127 
val get_imports = Thy_Load.imports_of o get_theory; 
d453faed4815
clarified get_imports  should not rely on accidental order within graph;
wenzelm
parents:
44302
diff
changeset

128 

38145
675827e61eb9
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
wenzelm
parents:
38143
diff
changeset

129 
fun loaded_files name = NAMED_CRITICAL "Thy_Info" (fn () => 
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37942
diff
changeset

130 
(case get_deps name of 
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37942
diff
changeset

131 
NONE => [] 
38145
675827e61eb9
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
wenzelm
parents:
38143
diff
changeset

132 
 SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name))); 
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37942
diff
changeset

133 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

134 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

135 

43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

136 
(** thy operations **) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

137 

43640  138 
(* main loader actions *) 
29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

139 

38145
675827e61eb9
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
wenzelm
parents:
38143
diff
changeset

140 
fun remove_thy name = NAMED_CRITICAL "Thy_Info" (fn () => 
37979  141 
if is_finished name then error (loader_msg "attempt to change finished theory" [name]) 
29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

142 
else 
29434  143 
let 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

144 
val succs = thy_graph String_Graph.all_succs [name]; 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39557
diff
changeset

145 
val _ = Output.urgent_message (loader_msg "removing" succs); 
38142  146 
val _ = List.app (perform Remove) succs; 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

147 
val _ = change_thys (fold String_Graph.del_node succs); 
38142  148 
in () end); 
29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

149 

38145
675827e61eb9
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
wenzelm
parents:
38143
diff
changeset

150 
fun kill_thy name = NAMED_CRITICAL "Thy_Info" (fn () => 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

151 
if known_thy name then remove_thy name 
38142  152 
else ()); 
7099  153 

43640  154 
fun update_thy deps theory = NAMED_CRITICAL "Thy_Info" (fn () => 
155 
let 

156 
val name = Context.theory_name theory; 

157 
val parents = map Context.theory_name (Theory.parents_of theory); 

158 
val _ = kill_thy name; 

159 
val _ = map get_theory parents; 

160 
val _ = change_thys (new_entry name parents (SOME deps, SOME theory)); 

161 
val _ = perform Update name; 

162 
in () end); 

163 

7099  164 

24209  165 
(* scheduling loader tasks *) 
166 

51330  167 
datatype result = 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

168 
Result of {theory: theory, id: serial, present: unit > unit, commit: unit > unit, weight: int}; 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

169 

e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

170 
fun theory_result theory = Result {theory = theory, id = 0, present = I, commit = I, weight = 0}; 
51330  171 

172 
fun result_theory (Result {theory, ...}) = theory; 

51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

173 
fun result_present (Result {present, ...}) = present; 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

174 
fun result_commit (Result {commit, ...}) = commit; 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

175 
fun result_ord (Result {weight = i, ...}, Result {weight = j, ...}) = int_ord (j, i); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

176 

e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

177 
fun join_proofs (Result {theory, id, present, ...}) = 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

178 
let 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

179 
val result1 = Exn.capture Thm.join_theory_proofs theory; 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

180 
val results2 = Future.join_results (Goal.peek_futures id); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

181 
in result1 :: results2 end; 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

182 

43641
081e009549dc
uniform finish_thy  always Global_Theory.join_proofs, even with sequential scheduling;
wenzelm
parents:
43640
diff
changeset

183 

37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

184 
datatype task = 
43641
081e009549dc
uniform finish_thy  always Global_Theory.join_proofs, even with sequential scheduling;
wenzelm
parents:
43640
diff
changeset

185 
Task of string list * (theory list > result)  
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

186 
Finished of theory; 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

187 

3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

188 
fun task_finished (Task _) = false 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

189 
 task_finished (Finished _) = true; 
24209  190 

44162  191 
fun task_parents deps (parents: string list) = map (the o AList.lookup (op =) deps) parents; 
192 

29118  193 
local 
194 

44162  195 
val schedule_seq = 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

196 
String_Graph.schedule (fn deps => fn (_, task) => 
44162  197 
(case task of 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

198 
Task (parents, body) => 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

199 
let 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

200 
val result = body (task_parents deps parents); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

201 
val _ = Par_Exn.release_all (join_proofs result); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

202 
val _ = result_present result (); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

203 
val _ = result_commit result (); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

204 
in result_theory result end 
44162  205 
 Finished thy => thy)) #> ignore; 
29000
5e03bc760355
improved future_schedule: more robust handling of failed parents (explicit join), final join of all futures, including Exn.release_all;
wenzelm
parents:
28980
diff
changeset

206 

51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

207 
val schedule_futures = uninterruptible (fn _ => fn tasks => 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

208 
let 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

209 
val futures = tasks 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

210 
> String_Graph.schedule (fn deps => fn (name, task) => 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

211 
(case task of 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

212 
Task (parents, body) => 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

213 
(singleton o Future.forks) 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

214 
{name = "theory:" ^ name, group = NONE, 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

215 
deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true} 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

216 
(fn () => 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

217 
(case filter (not o can Future.join o #2) deps of 
51330  218 
[] => body (map (result_theory o Future.join) (task_parents deps parents)) 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

219 
 bad => 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

220 
error (loader_msg ("failed to load " ^ quote name ^ 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

221 
" (unresolved " ^ commas_quote (map #1 bad) ^ ")") []))) 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

222 
 Finished theory => Future.value (theory_result theory))); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

223 

e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

224 
val results1 = futures 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

225 
> maps (fn future => 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

226 
(case Future.join_result future of 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

227 
Exn.Res result => join_proofs result 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

228 
 Exn.Exn exn => [Exn.Exn exn])); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

229 

e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

230 
val results2 = futures 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

231 
> map_filter (Exn.get_res o Future.join_result) 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

232 
> sort result_ord 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

233 
> Par_List.map (fn result => Exn.capture (result_present result) ()); 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

234 

e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

235 
(* FIXME more precise commit order (!?) *) 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

236 
val results3 = futures 
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

237 
> map (fn future => Exn.capture (fn () => result_commit (Future.join future) ()) ()); 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

238 

59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

239 
(* FIXME avoid global reset_futures (!??) *) 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

240 
val results4 = map Exn.Exn (map_filter Task_Queue.group_status (Goal.reset_futures ())); 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

241 

51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

242 
val _ = Par_Exn.release_all (results1 @ results2 @ results3 @ results4); 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

243 
in () end); 
29429
a6c641f08af7
schedule_futures: tuned final consolidation, explicit after_load phase;
wenzelm
parents:
29421
diff
changeset

244 

24209  245 
in 
246 

32794  247 
fun schedule_tasks tasks = 
29118  248 
if not (Multithreading.enabled ()) then schedule_seq tasks 
249 
else if Multithreading.self_critical () then 

24209  250 
(warning (loader_msg "no multithreading within critical section" []); 
251 
schedule_seq tasks) 

29118  252 
else schedule_futures tasks; 
24209  253 

254 
end; 

255 

256 

23967  257 
(* require_thy  checking database entries wrt. the filesystem *) 
15065  258 

7211  259 
local 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

260 

37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

261 
fun required_by _ [] = "" 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

262 
 required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

263 

51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

264 
fun load_thy last_timing initiators update_time deps text (name, pos) keywords parents = 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

265 
let 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

266 
val _ = kill_thy name; 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39557
diff
changeset

267 
val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators); 
50845  268 
val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => (); 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

269 

41548
bd0bebf93fa6
Thy_Load.begin_theory: maintain source specification of imports;
wenzelm
parents:
41536
diff
changeset

270 
val {master = (thy_path, _), imports} = deps; 
38134
3de75ca6f166
load_thy: refer to physical master directory (not accumulated source import directory) and enable loading files relatively to that;
wenzelm
parents:
37985
diff
changeset

271 
val dir = Path.dir thy_path; 
51294
0850d43cb355
discontinued obsolete header "files"  these are loaded explicitly after exploring dependencies;
wenzelm
parents:
51293
diff
changeset

272 
val header = Thy_Header.make (name, pos) imports keywords; 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

273 

ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

274 
val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

275 

51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

276 
val id = serial (); 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

277 
val text_pos = Position.put_id (Markup.print_int id) (Path.position thy_path); 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

278 
val (theory, present, weight) = 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

279 
Thy_Load.load_thy last_timing update_time dir header text_pos text 
48638  280 
(if name = Context.PureN then [ML_Context.the_global_context ()] else parents); 
43640  281 
fun commit () = update_thy deps theory; 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

282 
in Result {theory = theory, id = id, present = present, commit = commit, weight = weight} end; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

283 

48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

284 
fun check_deps dir name = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

285 
(case lookup_deps name of 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

286 
SOME NONE => (true, NONE, Position.none, get_imports name, []) 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

287 
 NONE => 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

288 
let val {master, text, theory_pos, imports, keywords} = Thy_Load.check_thy dir name 
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

289 
in (false, SOME (make_deps master imports, text), theory_pos, imports, keywords) end 
42129
c17508a61f49
present theory content as future, depending on intermediate proof state futures  potential to reduce memory requirements and improve parallelization;
wenzelm
parents:
42003
diff
changeset

290 
 SOME (SOME {master, ...}) => 
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

291 
let 
48928  292 
val {master = master', text = text', theory_pos = theory_pos', imports = imports', 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

293 
keywords = keywords'} = Thy_Load.check_thy dir name; 
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

294 
val deps' = SOME (make_deps master' imports', text'); 
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

295 
val current = 
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

296 
#2 master = #2 master' andalso 
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

297 
(case lookup_theory name of 
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

298 
NONE => false 
48886
9604c6563226
discontinued separate list of required files  maintain only provided files as they occur at runtime;
wenzelm
parents:
48876
diff
changeset

299 
 SOME theory => Thy_Load.load_current theory); 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

300 
in (current, deps', theory_pos', imports', keywords') end); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

301 

23967  302 
in 
303 

51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

304 
fun require_thys last_timing initiators dir strs tasks = 
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

305 
fold_map (require_thy last_timing initiators dir) strs tasks >> forall I 
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

306 
and require_thy last_timing initiators dir (str, require_pos) tasks = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

307 
let 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

308 
val path = Path.expand (Path.explode str); 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

309 
val name = Path.implode (Path.base path); 
7066  310 
in 
50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

311 
(case try (String_Graph.get_node tasks) name of 
48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

312 
SOME task => (task_finished task, tasks) 
23967  313 
 NONE => 
314 
let 

43651
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
43641
diff
changeset

315 
val dir' = Path.append dir (Path.dir path); 
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
43641
diff
changeset

316 
val _ = member (op =) initiators name andalso error (cycle_msg initiators); 
511df47bcadc
some support for theory files within Isabelle/Scala session;
wenzelm
parents:
43641
diff
changeset

317 

51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

318 
val (current, deps, theory_pos, imports, keywords) = check_deps dir' name 
23967  319 
handle ERROR msg => cat_error msg 
320 
(loader_msg "the error(s) above occurred while examining theory" [name] ^ 

48992  321 
Position.here require_pos ^ required_by "\n" initiators); 
37981
9a15982f41fe
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);
wenzelm
parents:
37980
diff
changeset

322 

48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

323 
val parents = map (base_name o #1) imports; 
48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

324 
val (parents_current, tasks') = 
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

325 
require_thys last_timing (name :: initiators) 
48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

326 
(Path.append dir (master_dir (Option.map #1 deps))) imports tasks; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

327 

23967  328 
val all_current = current andalso parents_current; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

329 
val task = 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

330 
if all_current then Finished (get_theory name) 
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

331 
else 
37980
b8c3d4dc1e3e
avoid repeated File.read for theory text (as before);
wenzelm
parents:
37979
diff
changeset

332 
(case deps of 
b8c3d4dc1e3e
avoid repeated File.read for theory text (as before);
wenzelm
parents:
37979
diff
changeset

333 
NONE => raise Fail "Malformed deps" 
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

334 
 SOME (dep, text) => 
48876
157dd47032e0
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
wenzelm
parents:
48874
diff
changeset

335 
let 
157dd47032e0
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
wenzelm
parents:
48874
diff
changeset

336 
val update_time = serial (); 
48928  337 
val load = 
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

338 
load_thy last_timing initiators update_time dep 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

339 
text (name, theory_pos) keywords; 
48876
157dd47032e0
more standard Thy_Load.check_thy for Pure.thy, relying on its header;
wenzelm
parents:
48874
diff
changeset

340 
in Task (parents, load) end); 
48874
ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48710
diff
changeset

341 

ff9cd47be39b
refined Thy_Load.check_thy: find more uses in body text, based on keywords;
wenzelm
parents:
48710
diff
changeset

342 
val tasks'' = new_entry name parents task tasks'; 
48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

343 
in (all_current, tasks'') end) 
7066  344 
end; 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

345 

23967  346 
end; 
347 

348 

37979  349 
(* use_thy *) 
23967  350 

51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

351 
fun use_theories {last_timing, master_dir} imports = 
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
50862
diff
changeset

352 
schedule_tasks (snd (require_thys last_timing [] master_dir imports String_Graph.empty)); 
23967  353 

51228  354 
val use_thys = use_theories {last_timing = K Time.zeroTime, master_dir = Path.current}; 
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37942
diff
changeset

355 
val use_thy = use_thys o single; 
7211  356 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

357 

37979  358 
(* toplevel begin theory  without maintaining database *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

359 

48888  360 
fun toplevel_begin_theory master_dir (header: Thy_Header.header) = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

361 
let 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

362 
val {name = (name, _), imports, ...} = header; 
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

363 
val _ = kill_thy name; 
51228  364 
val _ = use_theories {last_timing = K Time.zeroTime, master_dir = master_dir} imports; 
46958
0ec8f04e753a
define keywords early when processing the theory header, before running the body commands;
wenzelm
parents:
46938
diff
changeset

365 
val _ = Thy_Header.define_keywords header; 
48927
ef462b5558eb
theory def/ref position reports, which enable hyperlinks etc.;
wenzelm
parents:
48898
diff
changeset

366 
val parents = map (get_theory o base_name o fst) imports; 
48888  367 
in Thy_Load.begin_theory master_dir header parents end; 
7244  368 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

369 

37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37955
diff
changeset

370 
(* register theory *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

371 

37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset

372 
fun register_thy theory = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

373 
let 
16454  374 
val name = Context.theory_name theory; 
48898
9fc880720663
simplified Thy_Load.check_thy (again)  no need to pass keywords nor find files in body text;
wenzelm
parents:
48888
diff
changeset

375 
val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name; 
41548
bd0bebf93fa6
Thy_Load.begin_theory: maintain source specification of imports;
wenzelm
parents:
41536
diff
changeset

376 
val imports = Thy_Load.imports_of theory; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

377 
in 
38145
675827e61eb9
more precise CRITICAL sections, using NAMED_CRITICAL uniformly;
wenzelm
parents:
38143
diff
changeset

378 
NAMED_CRITICAL "Thy_Info" (fn () => 
38142  379 
(kill_thy name; 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39557
diff
changeset

380 
Output.urgent_message ("Registering theory " ^ quote name); 
43640  381 
update_thy (make_deps master imports) theory)) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

382 
end; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

383 

24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

384 

8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

385 
(* finish all theories *) 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

386 

50862
5fc8b83322f5
more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
wenzelm
parents:
50845
diff
changeset

387 
fun finish () = change_thys (String_Graph.map (fn _ => fn (_, entry) => (NONE, entry))); 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

388 

6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

389 
end; 