author  wenzelm 
Fri, 08 Dec 2017 16:02:44 +0100  
changeset 67163  257bcd20eeec 
parent 66873  9953ae603a23 
child 67173  e746db6db903 
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 
66371
6ce1afc01040
more thorough Execution.join, under the assumption that nested Execution.fork only happens from given exed_ids;
wenzelm
parents:
66370
diff
changeset

157 
val _ = Execution.join [exec_id]; 
64574
1134e4d5e5b7
consolidate nested thms with persistent result, for improved performance;
wenzelm
parents:
62942
diff
changeset

158 
val res = Exn.capture Thm.consolidate_theory theory; 
66377  159 
val exns = maps Task_Queue.group_status (Execution.peek exec_id); 
160 
in res :: map Exn.Exn exns end; 

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

161 

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

162 
datatype task = 
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2)  qualified theory names are meant to cover this;
wenzelm
parents:
66377
diff
changeset

163 
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

164 
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

165 

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

167 
 task_finished (Finished _) = true; 
24209  168 

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

171 
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

172 
String_Graph.schedule (fn deps => fn (_, task) => 
44162  173 
(case task of 
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2)  qualified theory names are meant to cover this;
wenzelm
parents:
66377
diff
changeset

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

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

176 
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

177 
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

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

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

180 
in result_theory result end 
44162  181 
 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

182 

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

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

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

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

187 
(case task of 
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2)  qualified theory names are meant to cover this;
wenzelm
parents:
66377
diff
changeset

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

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

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

191 
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

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

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

195 
 bad => 
55797  196 
error 
197 
("Failed to load theory " ^ quote name ^ 

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

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

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

200 

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

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

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

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

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

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

206 

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

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

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

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

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

211 

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

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

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

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

215 

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

216 
(* FIXME avoid global Execution.reset (!??) *) 
53192  217 
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

218 

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

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

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

221 

24209  222 

65505  223 
(* eval theory *) 
224 

225 
fun excursion keywords master_dir last_timing init elements = 

226 
let 

227 
fun prepare_span st span = 

228 
Command_Span.content span 

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

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

231 

232 
fun element_result span_elem (st, _) = 

233 
let 

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

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

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

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

238 

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

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

241 

242 
val thy = Toplevel.end_theory end_pos end_state; 

243 
in (results, thy) end; 

244 

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

246 
let 

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

248 
val keywords = 

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

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

251 

252 
val toks = Token.explode keywords text_pos text; 

253 
val spans = Outer_Syntax.parse_spans toks; 

254 
val elements = Thy_Syntax.parse_elements keywords spans; 

255 

256 
fun init () = 

257 
Resources.begin_theory master_dir header parents 

258 
> Present.begin_theory update_time 

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

260 

261 
val (results, thy) = 

262 
cond_timeit true ("theory " ^ quote name) 

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

264 

265 
fun present () = 

266 
let 

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

268 
in 

67163  269 
if exists (Toplevel.is_skipped_proof o #2) res then () 
65505  270 
else 
271 
let val tex_source = Thy_Output.present_thy thy res toks > Buffer.content; 

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

273 
end; 

274 

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

276 

277 

23967  278 
(* require_thy  checking database entries wrt. the filesystem *) 
15065  279 

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

281 

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

282 
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

283 
 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

284 

61381  285 
fun load_thy document symbols last_timing 
286 
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

287 
let 
59178  288 
val _ = remove_thy name; 
58843  289 
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

290 
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

291 

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

292 
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

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

294 
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

295 

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

296 
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

297 

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

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

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

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

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

302 

66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66711
diff
changeset

303 
val timing_start = Timing.start (); 
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66711
diff
changeset

304 

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

305 
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

306 
val (theory, present, weight) = 
65505  307 
eval_thy document symbols last_timing update_time dir header text_pos text 
62876  308 
(if name = Context.PureN then [Context.the_global_context ()] else parents); 
66873
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66711
diff
changeset

309 

9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66711
diff
changeset

310 
val timing_result = Timing.result timing_start; 
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66711
diff
changeset

311 
val timing_props = [Markup.theory_timing, (Markup.nameN, name)]; 
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66711
diff
changeset

312 
val _ = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) [] 
9953ae603a23
provide theory timing information, similar to command timing but always considered relevant;
wenzelm
parents:
66711
diff
changeset

313 

43640  314 
fun commit () = update_thy deps theory; 
53375
78693e46a237
Execution.fork formally requires registered Execution.running;
wenzelm
parents:
53192
diff
changeset

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

316 
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

317 
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

318 

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

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

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

321 
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

322 
 NONE => 
56208  323 
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

324 
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

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

326 
let 
48928  327 
val {master = master', text = text', theory_pos = theory_pos', imports = imports', 
56208  328 
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

329 
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

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

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

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

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

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

336 

23967  337 
in 
338 

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

339 
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

340 
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

341 
>> forall I 
65454  342 
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

343 
let 
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2)  qualified theory names are meant to cover this;
wenzelm
parents:
66377
diff
changeset

344 
val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s; 
7066  345 
in 
65443
dccbfc715904
provide Resources.import_name in ML, similar to Scala version;
wenzelm
parents:
65058
diff
changeset

346 
(case try (String_Graph.get_node tasks) theory_name of 
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2)  qualified theory names are meant to cover this;
wenzelm
parents:
66377
diff
changeset

347 
SOME task => (task_finished task, tasks) 
23967  348 
 NONE => 
349 
let 

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

350 
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

351 

65454  352 
val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name 
55797  353 
handle ERROR msg => 
354 
cat_error msg 

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

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

357 

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

360 

361 
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

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

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

365 

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

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

368 
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

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

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

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

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

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

374 
val update_time = serial (); 
48928  375 
val load = 
61381  376 
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

377 
text (theory_name, theory_pos) keywords; 
66711
80fa1401cf76
discontinued extra checks (see ce676a750575 and 60c159d490a2)  qualified theory names are meant to cover this;
wenzelm
parents:
66377
diff
changeset

378 
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

379 

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

380 
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

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

383 

23967  384 
end; 
385 

386 

65444  387 
(* use theories *) 
23967  388 

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

389 
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

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

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

392 
require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty; 
66368  393 
in if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks end; 
23967  394 

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

397 
{document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime, 
65532  398 
qualifier = Resources.default_qualifier, master_dir = Path.current} 
65444  399 
[(name, Position.none)]; 
7211  400 

59364  401 

57626  402 
(* toplevel scripting  without maintaining database *) 
403 

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

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

411 
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

412 

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

413 

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

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

415 

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

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

417 
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

418 
val name = Context.theory_long_name theory; 
56208  419 
val {master, ...} = Resources.check_thy (Resources.master_directory theory) name; 
420 
val imports = Resources.imports_of theory; 

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

421 
in 
59178  422 
change_thys (fn thys => 
423 
let 

424 
val thys' = remove name thys; 

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

426 
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

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

428 

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

429 

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

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

431 

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

432 
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

433 

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

434 
end; 
62847  435 

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