author  wenzelm 
Tue, 18 Apr 2017 16:34:58 +0200  
changeset 65505  741fad555d82 
parent 65459  da59e8e0a663 
child 65532  febfd9f78bd4 
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 
26614  10 
val get_names: unit > string list 
7288  11 
val lookup_theory: string > theory option 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

12 
val get_theory: string > theory 
60937  13 
val pure_theory: unit > theory 
26983  14 
val master_directory: string > Path.T 
29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

15 
val remove_thy: string > unit 
59366
e94df7f6b608
clarified build_theories: proper protocol handler;
wenzelm
parents:
59364
diff
changeset

16 
val use_theories: 
61381  17 
{document: bool, 
18 
symbols: HTML.symbols, 

65058
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64574
diff
changeset

19 
last_timing: Toplevel.transition > Time.time, 
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

20 
qualifier: string, 
61381  21 
master_dir: Path.T} > (string * Position.T) list > unit 
65444  22 
val use_thy: string > unit 
58856  23 
val script_thy: Position.T > string > theory > theory 
37954
a2e73df0b1e0
simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
wenzelm
parents:
37953
diff
changeset

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

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

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

27 

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

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

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

30 

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

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

32 

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

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

34 

55797  35 
val show_path = space_implode " via " o map quote; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

36 

55797  37 
fun cycle_msg names = "Cyclic dependency of " ^ show_path names; 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

38 

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

39 

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

41 

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

42 
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

43 
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

44 

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

45 
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

46 
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

47 

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

48 

59178  49 
(* global thys *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

50 

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

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

52 
{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

53 
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

54 

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

55 
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

56 

65454  57 
fun master_dir_deps (d: deps option) = 
59178  58 
the_default Path.current (Option.map (Path.dir o #1 o #master) d); 
59 

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

60 
local 
59178  61 
val global_thys = 
62 
Synchronized.var "Thy_Info.thys" 

63 
(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

64 
in 
59178  65 
fun get_thys () = Synchronized.value global_thys; 
66 
fun change_thys f = Synchronized.change global_thys f; 

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

67 
end; 
5209  68 

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

69 
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

70 

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

71 

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

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

73 

59178  74 
fun lookup thys name = try (String_Graph.get_node thys) name; 
75 
fun lookup_thy name = lookup (get_thys ()) name; 

7935  76 

59178  77 
fun get thys name = 
78 
(case lookup thys name of 

15531  79 
SOME thy => thy 
55797  80 
 NONE => error ("Theory loader: nothing known about theory " ^ quote name)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

81 

59178  82 
fun get_thy name = get (get_thys ()) name; 
83 

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

84 

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

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

86 

15570  87 
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

88 

65454  89 
val master_directory = master_dir_deps o #1 o get_thy; 
7191  90 

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 
(* access theory *) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

93 

7687  94 
fun lookup_theory name = 
95 
(case lookup_thy name of 

38142  96 
SOME (_, SOME theory) => SOME theory 
15531  97 
 _ => NONE); 
7288  98 

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

99 
fun get_theory name = 
7288  100 
(case lookup_theory name of 
23871  101 
SOME theory => theory 
55797  102 
 _ => error ("Theory loader: undefined entry for theory " ^ quote name)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

103 

62942  104 
fun pure_theory () = get_theory Context.PureN; 
60937  105 

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

107 

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

108 

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

109 

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

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

111 

59178  112 
(* remove *) 
29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

113 

59178  114 
fun remove name thys = 
115 
(case lookup thys name of 

116 
NONE => thys 

117 
 SOME (NONE, _) => error ("Cannot update finished theory " ^ quote name) 

118 
 SOME _ => 

119 
let 

120 
val succs = String_Graph.all_succs thys [name]; 

121 
val _ = writeln ("Theory loader: removing " ^ commas_quote succs); 

122 
in fold String_Graph.del_node succs thys end); 

29421
db532e37cda2
use_thys: perform consolidate_thy on loaded theories, which removes failed nodes in posthoc fashion;
wenzelm
parents:
29118
diff
changeset

123 

59178  124 
val remove_thy = change_thys o remove; 
125 

7099  126 

59178  127 
(* update *) 
128 

129 
fun update deps theory thys = 

43640  130 
let 
65459
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
65455
diff
changeset

131 
val name = Context.theory_long_name theory; 
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
65455
diff
changeset

132 
val parents = map Context.theory_long_name (Theory.parents_of theory); 
59178  133 

134 
val thys' = remove name thys; 

135 
val _ = map (get thys') parents; 

136 
in new_entry name parents (SOME deps, SOME theory) thys' end; 

137 

138 
fun update_thy deps theory = change_thys (update deps theory); 

43640  139 

7099  140 

24209  141 
(* scheduling loader tasks *) 
142 

51330  143 
datatype result = 
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

144 
Result of {theory: theory, exec_id: Document_ID.exec, 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

145 
present: unit > unit, commit: unit > unit, weight: int}; 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

146 

53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

147 
fun theory_result theory = 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

148 
Result {theory = theory, exec_id = Document_ID.none, present = I, commit = I, weight = 0}; 
51330  149 

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

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

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

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

153 
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

154 

53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

155 
fun join_theory (Result {theory, exec_id, ...}) = 
54370
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

156 
let 
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

157 
(*toplevel proofs and diags*) 
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

158 
val _ = Future.join_tasks (maps Future.group_snapshot (Execution.peek exec_id)); 
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

159 
(*fully nested proofs*) 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
62942
diff
changeset

160 
val res = Exn.capture Thm.consolidate_theory theory; 
54370
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

161 
in res :: map Exn.Exn (maps Task_Queue.group_status (Execution.peek exec_id)) end; 
43641
081e009549dc
uniform finish_thy  always Global_Theory.join_proofs, even with sequential scheduling;
wenzelm
parents:
43640
diff
changeset

162 

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

163 
datatype task = 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

164 
Task of Path.T * 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

165 
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

166 

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

167 
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

168 
 task_finished (Finished _) = true; 
24209  169 

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

29118  172 
local 
173 

44162  174 
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

175 
String_Graph.schedule (fn deps => fn (_, task) => 
44162  176 
(case task of 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

177 
Task (_, parents, body) => 
51331
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 result = body (task_parents deps parents); 
53190
5d92649a310e
simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
wenzelm
parents:
51661
diff
changeset

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

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

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

183 
in result_theory result end 
44162  184 
 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

185 

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

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

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

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

190 
(case task of 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

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

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

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

194 
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

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

196 
(case filter (not o can Future.join o #2) deps of 
51330  197 
[] => 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

198 
 bad => 
55797  199 
error 
200 
("Failed to load theory " ^ quote name ^ 

201 
" (unresolved " ^ commas_quote (map #1 bad) ^ ")"))) 

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

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

203 

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

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

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

206 
(case Future.join_result future of 
53190
5d92649a310e
simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
wenzelm
parents:
51661
diff
changeset

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

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

209 

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

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

211 
> 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

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

213 
> 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

214 

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

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

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

217 
> 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

218 

54370
39ac1a02c60c
join all theory body forks, notably Toplevel.atom_result (diagnostic commands), before peeking at full status;
wenzelm
parents:
53375
diff
changeset

219 
(* FIXME avoid global Execution.reset (!??) *) 
53192  220 
val results4 = map Exn.Exn (maps Task_Queue.group_status (Execution.reset ())); 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51228
diff
changeset

221 

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

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

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

224 

24209  225 
in 
226 

32794  227 
fun schedule_tasks tasks = 
59180
c0fa3b3bdabd
discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
wenzelm
parents:
59178
diff
changeset

228 
if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks; 
24209  229 

230 
end; 

231 

232 

65505  233 
(* eval theory *) 
234 

235 
fun excursion keywords master_dir last_timing init elements = 

236 
let 

237 
fun prepare_span st span = 

238 
Command_Span.content span 

239 
> Command.read keywords (Command.read_thy st) master_dir init ([], ~1) 

240 
> (fn tr => Toplevel.put_timing (last_timing tr) tr); 

241 

242 
fun element_result span_elem (st, _) = 

243 
let 

244 
val elem = Thy_Syntax.map_element (prepare_span st) span_elem; 

245 
val (results, st') = Toplevel.element_result keywords elem st; 

246 
val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem); 

247 
in (results, (st', pos')) end; 

248 

249 
val (results, (end_state, end_pos)) = 

250 
fold_map element_result elements (Toplevel.toplevel, Position.none); 

251 

252 
val thy = Toplevel.end_theory end_pos end_state; 

253 
in (results, thy) end; 

254 

255 
fun eval_thy document symbols last_timing update_time master_dir header text_pos text parents = 

256 
let 

257 
val (name, _) = #name header; 

258 
val keywords = 

259 
fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents 

260 
(Keyword.add_keywords (#keywords header) Keyword.empty_keywords); 

261 

262 
val toks = Token.explode keywords text_pos text; 

263 
val spans = Outer_Syntax.parse_spans toks; 

264 
val elements = Thy_Syntax.parse_elements keywords spans; 

265 

266 
fun init () = 

267 
Resources.begin_theory master_dir header parents 

268 
> Present.begin_theory update_time 

269 
(fn () => implode (map (HTML.present_span symbols keywords) spans)); 

270 

271 
val (results, thy) = 

272 
cond_timeit true ("theory " ^ quote name) 

273 
(fn () => excursion keywords master_dir last_timing init elements); 

274 

275 
fun present () = 

276 
let 

277 
val res = filter_out (Toplevel.is_ignored o #1) (maps Toplevel.join_results results); 

278 
in 

279 
if exists (Toplevel.is_skipped_proof o #2) res then 

280 
warning ("Cannot present theory with skipped proofs: " ^ quote name) 

281 
else 

282 
let val tex_source = Thy_Output.present_thy thy res toks > Buffer.content; 

283 
in if document then Present.theory_output thy tex_source else () end 

284 
end; 

285 

286 
in (thy, present, size text) end; 

287 

288 

23967  289 
(* require_thy  checking database entries wrt. the filesystem *) 
15065  290 

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

292 

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

293 
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

294 
 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

295 

61381  296 
fun load_thy document symbols last_timing 
297 
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

298 
let 
59178  299 
val _ = remove_thy name; 
58843  300 
val _ = writeln ("Loading theory " ^ quote name ^ required_by " " initiators); 
56333
38f1422ef473
support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents:
56208
diff
changeset

301 
val _ = Output.try_protocol_message (Markup.loading_theory name) []; 
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

302 

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

303 
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

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

305 
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

306 

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

307 
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

308 

53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

309 
val exec_id = Document_ID.make (); 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

310 
val _ = 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

311 
Execution.running Document_ID.none exec_id [] orelse 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

312 
raise Fail ("Failed to register execution: " ^ Document_ID.print exec_id); 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

313 

78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

314 
val text_pos = Position.put_id (Document_ID.print exec_id) (Path.position thy_path); 
51331
e7fab0b5dbe7
join all proofs before scheduling present phase (ordered according to weight);
wenzelm
parents:
51330
diff
changeset

315 
val (theory, present, weight) = 
65505  316 
eval_thy document symbols last_timing update_time dir header text_pos text 
62876  317 
(if name = Context.PureN then [Context.the_global_context ()] else parents); 
43640  318 
fun commit () = update_thy deps theory; 
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

319 
in 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

320 
Result {theory = theory, exec_id = exec_id, present = present, commit = commit, weight = weight} 
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

321 
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

322 

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

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

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

325 
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

326 
 NONE => 
56208  327 
let val {master, text, theory_pos, imports, keywords} = Resources.check_thy dir name 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

328 
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

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

330 
let 
48928  331 
val {master = master', text = text', theory_pos = theory_pos', imports = imports', 
56208  332 
keywords = keywords'} = Resources.check_thy dir name; 
42003
6e45dc518ebb
replaced File.check by specific File.check_file, File.check_dir;
wenzelm
parents:
41955
diff
changeset

333 
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

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

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

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

337 
NONE => false 
56208  338 
 SOME theory => Resources.loaded_files_current theory); 
51293
05b1bbae748d
discontinued obsolete 'uses' within theory header;
wenzelm
parents:
51284
diff
changeset

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

340 

23967  341 
in 
342 

65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

343 
fun require_thys document symbols last_timing initiators qualifier dir strs tasks = 
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

344 
fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks 
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

345 
>> forall I 
65454  346 
and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

347 
let 
65454  348 
val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s; 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

349 
fun check_entry (Task (node_name', _, _)) = 
60975
5f3d6e16ea78
avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
wenzelm
parents:
60937
diff
changeset

350 
if op = (apply2 File.platform_path (node_name, node_name')) 
5f3d6e16ea78
avoid ambiguities on native Windows, such as / vs. /cygdrive/c/cygwin;
wenzelm
parents:
60937
diff
changeset

351 
then () 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

352 
else 
65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

353 
error ("Incoherent imports for theory " ^ quote theory_name ^ 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

354 
Position.here require_pos ^ ":\n" ^ 
55488
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
55461
diff
changeset

355 
" " ^ Path.print node_name ^ "\n" ^ 
60c159d490a2
more integrity checks of theory names vs. full node names;
wenzelm
parents:
55461
diff
changeset

356 
" " ^ Path.print node_name') 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

357 
 check_entry _ = (); 
7066  358 
in 
65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

359 
(case try (String_Graph.get_node tasks) theory_name of 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

360 
SOME task => (check_entry task; (task_finished task, tasks)) 
23967  361 
 NONE => 
362 
let 

65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

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

364 

65454  365 
val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name 
55797  366 
handle ERROR msg => 
367 
cat_error msg 

65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

368 
("The error(s) above occurred for theory " ^ quote theory_name ^ 
55797  369 
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

370 

65455  371 
val qualifier' = Resources.theory_qualifier theory_name; 
372 
val dir' = Path.append dir (master_dir_deps (Option.map #1 deps)); 

373 

374 
val parents = map (#theory_name o Resources.import_name qualifier' dir' 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

375 
val (parents_current, tasks') = 
65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

376 
require_thys document symbols last_timing (theory_name :: initiators) 
65455  377 
qualifier' dir' imports tasks; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

378 

23967  379 
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

380 
val task = 
65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

381 
if all_current then Finished (get_theory theory_name) 
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

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

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

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

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

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

387 
val update_time = serial (); 
48928  388 
val load = 
61381  389 
load_thy document symbols last_timing initiators update_time dep 
65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

390 
text (theory_name, theory_pos) keywords; 
55461
ce676a750575
more integrity checks of theory names vs. full node names  at least for the scope of a single use_thys (or "theories" section in ROOT);
wenzelm
parents:
54722
diff
changeset

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

392 

65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

393 
val tasks'' = new_entry theory_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

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

396 

23967  397 
end; 
398 

399 

65444  400 
(* use theories *) 
23967  401 

65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

402 
fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports = 
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

403 
let 
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

404 
val (_, tasks) = 
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

405 
require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty; 
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

406 
in schedule_tasks tasks end; 
23967  407 

65444  408 
fun use_thy name = 
61381  409 
use_theories 
65058
3e9f382fb67e
absent timing information means zero, according to 0070053570c4, f235646b1b73;
wenzelm
parents:
64574
diff
changeset

410 
{document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime, 
65445
e9e7f5f5794c
more qualifier treatment, but in the end it is still ignored;
wenzelm
parents:
65444
diff
changeset

411 
qualifier = Resources.default_qualifier (), master_dir = Path.current} 
65444  412 
[(name, Position.none)]; 
7211  413 

59364  414 

57626  415 
(* toplevel scripting  without maintaining database *) 
416 

58856  417 
fun script_thy pos txt thy = 
57626  418 
let 
58856  419 
val trs = 
58928
23d0ffd48006
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
wenzelm
parents:
58856
diff
changeset

420 
Outer_Syntax.parse thy pos txt 
58856  421 
> map (Toplevel.modify_init (K thy)); 
57626  422 
val end_pos = if null trs then pos else Toplevel.pos_of (List.last trs); 
423 
val end_state = fold (Toplevel.command_exception true) trs Toplevel.toplevel; 

424 
in Toplevel.end_theory end_pos end_state end; 

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

425 

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

426 

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

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

428 

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

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

430 
let 
65459
da59e8e0a663
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);
wenzelm
parents:
65455
diff
changeset

431 
val name = Context.theory_long_name theory; 
56208  432 
val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; 
433 
val imports = Resources.imports_of theory; 

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

434 
in 
59178  435 
change_thys (fn thys => 
436 
let 

437 
val thys' = remove name thys; 

438 
val _ = writeln ("Registering theory " ^ quote name); 

439 
in update (make_deps master imports) theory thys' end) 

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

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

441 

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

442 

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

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

444 

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

445 
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

446 

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

447 
end; 
62847  448 

65444  449 
fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name); 