author  wenzelm 
Tue, 12 Aug 2008 21:28:05 +0200  
changeset 27843  0bd68bf0cbb8 
parent 27579  97ce525f664c 
child 28126  7332b623b569 
permissions  rwrr 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

1 
(* Title: Pure/Thy/thy_info.ML 
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

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

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

4 

15801  5 
Main part of theory loader database, including handling of theory and 
6 
file dependencies. 

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

8 

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

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

10 
sig 
7099  11 
datatype action = Update  Outdate  Remove 
12 
val str_of_action: action > string 

13 
val add_hook: (action > string > unit) > unit 

26614  14 
val get_names: unit > string list 
7910  15 
val known_thy: string > bool 
7935  16 
val check_known_thy: string > bool 
17 
val if_known_thy: (string > unit) > string > unit 

7288  18 
val lookup_theory: string > theory option 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

19 
val get_theory: string > theory 
19547  20 
val the_theory: string > theory > theory 
24563  21 
val is_finished: string > bool 
26983  22 
val master_directory: string > Path.T 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

23 
val loaded_files: string > Path.T list 
23871  24 
val get_parents: string > string list 
27495
d2bb5d61b392
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
wenzelm
parents:
27345
diff
changeset

25 
val touch_thy: string > unit 
7910  26 
val touch_child_thys: string > unit 
25013  27 
val provide_file: Path.T > string > unit 
7941  28 
val load_file: bool > Path.T > unit 
26494  29 
val exec_file: bool > Path.T > Context.generic > Context.generic 
6241  30 
val use: string > unit 
24057
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

31 
val time_use: string > unit 
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

32 
val use_thys: string list > unit 
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

33 
val use_thy: string > unit 
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

34 
val time_use_thy: string > unit 
27495
d2bb5d61b392
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
wenzelm
parents:
27345
diff
changeset

35 
val remove_thy: string > unit 
d2bb5d61b392
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
wenzelm
parents:
27345
diff
changeset

36 
val kill_thy: string > unit 
24563  37 
val thy_ord: theory * theory > order 
23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

38 
val begin_theory: string > string list > (Path.T * bool) list > bool > theory 
27579  39 
val end_theory: theory > unit 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

40 
val register_thy: string > unit 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

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

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

44 

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

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

47 

7099  48 
(** theory loader actions and hooks **) 
49 

50 
datatype action = Update  Outdate  Remove; 

51 
val str_of_action = fn Update => "Update"  Outdate => "Outdate"  Remove => "Remove"; 

52 

53 
local 

54 
val hooks = ref ([]: (action > string > unit) list); 

55 
in 

23939  56 
fun add_hook f = CRITICAL (fn () => change hooks (cons f)); 
15570  57 
fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks); 
7099  58 
end; 
59 

60 

61 

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

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

63 

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

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

65 

23871  66 
fun loader_msg txt [] = "Theory loader: " ^ txt 
67 
 loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names; 

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

68 

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

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

71 

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

72 

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

74 

9327  75 
fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G 
9332  76 
handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess)); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

77 

7952  78 
fun upd_deps name entry G = 
19473  79 
fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G 
7952  80 
> Graph.map_node name (K entry); 
3976  81 

23967  82 
fun new_deps name parents entry G = 
7952  83 
(if can (Graph.get_node G) name then upd_deps name entry G else Graph.new_node (name, entry) G) 
84 
> add_deps name parents; 

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

85 

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

86 

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

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

88 

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

89 
type deps = 
24190  90 
{update_time: int, (*symbolic time of update; negative value means outdated*) 
91 
master: (Path.T * File.ident) option, (*master dependencies for thy file*) 

92 
text: string list, (*source text for thy*) 

93 
parents: string list, (*source specification of parents (partially qualified)*) 

94 
(*auxiliary files: source path, physical path + identifier*) 

95 
files: (Path.T * (Path.T * File.ident) option) list}; 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

96 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

97 
fun make_deps update_time master text parents files : deps = 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

98 
{update_time = update_time, master = master, text = text, parents = parents, files = files}; 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

99 

24068  100 
fun init_deps master text parents files = 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

101 
SOME (make_deps ~1 master text parents (map (rpair NONE) files)); 
23871  102 

24190  103 
fun master_dir NONE = Path.current 
104 
 master_dir (SOME (path, _)) = Path.dir path; 

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

105 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

106 
fun master_dir' (d: deps option) = the_default Path.current (Option.map (master_dir o #master) d); 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

107 
fun master_dir'' d = the_default Path.current (Option.map master_dir' d); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

108 

23967  109 
fun base_name s = Path.implode (Path.base (Path.explode s)); 
110 

7211  111 

6362  112 
type thy = deps option * theory option; 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

113 

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

114 
local 
6362  115 
val database = ref (Graph.empty: thy Graph.T); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

116 
in 
6362  117 
fun get_thys () = ! database; 
23939  118 
fun change_thys f = CRITICAL (fn () => Library.change database f); 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

119 
end; 
5209  120 

121 

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

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

123 

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

124 
fun thy_graph f x = f (get_thys ()) x; 
9417  125 

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

127 

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

128 

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

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

130 

7935  131 
fun lookup_thy name = 
15531  132 
SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE; 
7935  133 

16047  134 
val known_thy = is_some o lookup_thy; 
7935  135 
fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false); 
136 
fun if_known_thy f name = if check_known_thy name then f name else (); 

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

137 

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

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

139 
(case lookup_thy name of 
15531  140 
SOME thy => thy 
141 
 NONE => error (loader_msg "nothing known about theory" [name])); 

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

142 

23939  143 
fun change_thy name f = CRITICAL (fn () => 
144 
(get_thy name; change_thys (Graph.map_node name f))); 

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

145 

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

146 

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

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

148 

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

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

151 
fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x)); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

152 

26983  153 
val is_finished = is_none o get_deps; 
154 
val master_directory = master_dir' o get_deps; 

7191  155 

156 
fun loaded_files name = 

157 
(case get_deps name of 

15531  158 
NONE => [] 
159 
 SOME {master, files, ...} => 

24190  160 
(case master of SOME (thy_path, _) => [thy_path]  NONE => []) @ 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

161 
(map_filter (Option.map #1 o #2) files)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

162 

23871  163 
fun get_parents name = 
23967  164 
thy_graph Graph.imm_preds name handle Graph.UNDEF _ => 
6654  165 
error (loader_msg "nothing known about theory" [name]); 
166 

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

167 

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

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

169 

7687  170 
fun lookup_theory name = 
171 
(case lookup_thy name of 

15531  172 
SOME (_, SOME thy) => SOME thy 
173 
 _ => NONE); 

7288  174 

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

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

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

179 

19547  180 
fun the_theory name thy = 
181 
if Context.theory_name thy = name then thy 

182 
else get_theory name; 

183 

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

184 

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

185 

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

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

187 

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

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

189 

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

190 
fun check_unfinished fail name = 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

191 
if known_thy name andalso is_finished name then 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

192 
fail (loader_msg "cannot update finished theory" [name]) 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

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

194 

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

195 
fun check_files name = 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

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

197 
val files = (case get_deps name of SOME {files, ...} => files  NONE => []); 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

198 
val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path)  _ => NONE) files; 
24190  199 
val _ = null missing_files orelse 
200 
error (loader_msg "unresolved dependencies of theory" [name] ^ 

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

201 
" on file(s): " ^ commas_quote missing_files); 
24190  202 
in () end; 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

203 

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

204 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

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

206 

7099  207 
local 
208 

6241  209 
fun is_outdated name = 
210 
(case lookup_deps name of 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

211 
SOME (SOME {update_time, ...}) => update_time < 0 
6241  212 
 _ => false); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

213 

25013  214 
fun unfinished name = 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

215 
if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE) 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

216 
else SOME name; 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

217 

d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

218 
in 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

219 

6241  220 
fun outdate_thy name = 
7099  221 
if is_finished name orelse is_outdated name then () 
23939  222 
else CRITICAL (fn () => 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

223 
(change_deps name (Option.map (fn {master, text, parents, files, ...} => 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

224 
make_deps ~1 master text parents files)); perform Outdate name)); 
7099  225 

7910  226 
fun touch_thys names = 
25013  227 
List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names)); 
7910  228 

229 
fun touch_thy name = touch_thys [name]; 

230 
fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name); 

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

231 

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

233 

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

234 

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

236 

7191  237 
local 
238 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

239 
fun provide path name info (deps as SOME {update_time, master, text, parents, files}) = 
23871  240 
(if AList.defined (op =) files path then () 
7941  241 
else warning (loader_msg "undeclared dependency of theory" [name] ^ 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

242 
" on file: " ^ quote (Path.implode path)); 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

243 
SOME (make_deps update_time master text parents 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

244 
(AList.update (op =) (path, SOME info) files))) 
15531  245 
 provide _ _ _ NONE = NONE; 
7941  246 

247 
fun run_file path = 

26415  248 
(case Option.map (Context.theory_name o Context.the_theory) (Context.thread_data ()) of 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

249 
NONE => (ThyLoad.load_ml Path.current path; ()) 
23871  250 
 SOME name => 
251 
(case lookup_deps name of 

252 
SOME deps => 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

253 
change_deps name (provide path name (ThyLoad.load_ml (master_dir' deps) path)) 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

254 
 NONE => (ThyLoad.load_ml Path.current path; ()))); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

255 

7191  256 
in 
257 

25013  258 
fun provide_file path name = 
259 
let 

26983  260 
val dir = master_directory name; 
25013  261 
val _ = check_unfinished error name; 
262 
in 

26983  263 
(case ThyLoad.check_file dir path of 
25013  264 
SOME path_info => change_deps name (provide path name path_info) 
265 
 NONE => error ("Could not find file " ^ quote (Path.implode path))) 

266 
end; 

267 

24057
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

268 
fun load_file time path = 
7941  269 
if time then 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

270 
let val name = Path.implode path in 
7244  271 
timeit (fn () => 
9778  272 
(priority ("\n**** Starting file " ^ quote name ^ " ****"); 
9036  273 
run_file path; 
9778  274 
priority ("**** Finished file " ^ quote name ^ " ****\n"))) 
7244  275 
end 
24057
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

276 
else run_file path; 
7941  277 

26494  278 
fun exec_file time path = ML_Context.exec (fn () => load_file time path); 
279 

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

280 
val use = load_file false o Path.explode; 
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

281 
val time_use = load_file true o Path.explode; 
7191  282 

283 
end; 

6233  284 

285 

7099  286 
(* load_thy *) 
287 

9490  288 
fun required_by _ [] = "" 
289 
 required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")"; 

7099  290 

27843  291 
fun load_thy time upd_time initiators name = 
7099  292 
let 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

293 
val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators); 
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

294 
val (pos, text, files) = 
24068  295 
(case get_deps name of 
24190  296 
SOME {master = SOME (master_path, _), text as _ :: _, files, ...} => 
26881  297 
(Path.position master_path, text, files) 
24068  298 
 _ => error (loader_msg "corrupted dependency information" [name])); 
299 
val _ = touch_thy name; 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

300 
val _ = CRITICAL (fn () => 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

301 
change_deps name (Option.map (fn {master, text, parents, files, ...} => 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

302 
make_deps upd_time master text parents files))); 
27843  303 
val _ = OuterSyntax.load_thy name pos text (time orelse ! Output.timing); 
7099  304 
in 
23939  305 
CRITICAL (fn () => 
306 
(change_deps name 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

307 
(Option.map (fn {update_time, master, parents, files, ...} => 
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

308 
make_deps update_time master [] parents files)); 
23939  309 
perform Update name)) 
7099  310 
end; 
311 

312 

24209  313 
(* scheduling loader tasks *) 
314 

315 
datatype task = Task of (unit > unit)  Finished  Running; 

316 
fun task_finished Finished = true  task_finished _ = false; 

317 

318 
local 

319 

24230  320 
fun max_task (name, (Task body, m)) NONE = SOME (name: string, (body, m)) 
24229
4b5306c36bd9
schedule_tasks: alphabetical order for equivalent tasks;
wenzelm
parents:
24209
diff
changeset

321 
 max_task (name, (Task body, m)) (task' as SOME (name', (_, m'))) = 
4b5306c36bd9
schedule_tasks: alphabetical order for equivalent tasks;
wenzelm
parents:
24209
diff
changeset

322 
if m > m' orelse m = m' andalso name < name' then SOME (name, (body, m)) else task' 
24209  323 
 max_task _ task' = task'; 
324 

325 
fun next_task G = 

326 
let 

327 
val tasks = Graph.minimals G > map (fn name => 

328 
(name, (Graph.get_node G name, length (Graph.imm_succs G name)))); 

329 
val finished = filter (task_finished o fst o snd) tasks; 

330 
in 

331 
if not (null finished) then next_task (Graph.del_nodes (map fst finished) G) 

332 
else if null tasks then (Multithreading.Terminate, G) 

333 
else 

334 
(case fold max_task tasks NONE of 

335 
NONE => (Multithreading.Wait, G) 

336 
 SOME (name, (body, _)) => 

25736  337 
(Multithreading.Task {body = PrintMode.closure body, 
338 
cont = Graph.del_nodes [name], fail = K Graph.empty}, 

24209  339 
Graph.map_node name (K Running) G)) 
340 
end; 

341 

342 
fun schedule_seq tasks = 

343 
Graph.topological_order tasks 

344 
> List.app (fn name => (case Graph.get_node tasks name of Task body => body ()  _ => ())); 

345 

346 
in 

347 

348 
fun schedule_tasks tasks n = 

25775
90525e67ede7
added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
wenzelm
parents:
25736
diff
changeset

349 
let val m = Multithreading.max_threads_value () in 
24209  350 
if m <= 1 orelse n <= 1 then schedule_seq tasks 
351 
else if Multithreading.self_critical () then 

352 
(warning (loader_msg "no multithreading within critical section" []); 

353 
schedule_seq tasks) 

354 
else 

355 
(case Multithreading.schedule (Int.min (m, n)) next_task tasks of 

356 
[] => () 

357 
 exns => raise Exn.EXCEPTIONS (exns, "")) 

358 
end; 

359 

360 
end; 

361 

362 

23967  363 
(* require_thy  checking database entries wrt. the filesystem *) 
15065  364 

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

366 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

367 
fun check_ml master (src_path, info) = 
23871  368 
let val info' = 
369 
(case info of NONE => NONE 

370 
 SOME (_, id) => 

23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

371 
(case ThyLoad.check_ml (master_dir master) src_path of NONE => NONE 
23871  372 
 SOME (path', id') => if id <> id' then NONE else SOME (path', id'))) 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

373 
in (src_path, info') end; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

374 

24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

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

376 
(case lookup_deps name of 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

377 
SOME NONE => (true, NONE, get_parents name) 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

378 
 NONE => 
24190  379 
let val {master, text, imports = parents, uses = files} = ThyLoad.deps_thy dir name 
24068  380 
in (false, init_deps (SOME master) text parents files, parents) end 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

381 
 SOME (deps as SOME {update_time, master, text, parents, files}) => 
24190  382 
let 
383 
val (thy_path, thy_id) = ThyLoad.check_thy dir name; 

384 
val master' = SOME (thy_path, thy_id); 

385 
in 

386 
if Option.map #2 master <> SOME thy_id then 

24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

387 
let val {text = text', imports = parents', uses = files', ...} = 
24190  388 
ThyLoad.deps_thy dir name; 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

389 
in (false, init_deps master' text' parents' files', parents') end 
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

390 
else 
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

391 
let 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

392 
val files' = map (check_ml master') files; 
24307
434c9fbc1787
check_deps: ensure that theory is actually present, not just update_time > 1;
wenzelm
parents:
24230
diff
changeset

393 
val current = update_time >= 0 andalso can get_theory name 
434c9fbc1787
check_deps: ensure that theory is actually present, not just update_time > 1;
wenzelm
parents:
24230
diff
changeset

394 
andalso forall (is_some o snd) files'; 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

395 
val update_time' = if current then update_time else ~1; 
25030  396 
val deps' = SOME (make_deps update_time' master' text parents files'); 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

397 
in (current, deps', parents) end 
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

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

399 

25030  400 
fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents, files}) = 
401 
SOME (make_deps update_time master (explode (File.read path)) parents files); 

402 

23967  403 
in 
404 

24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

405 
fun require_thys time initiators dir strs tasks = 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

406 
fold_map (require_thy time initiators dir) strs tasks >> forall I 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

407 
and require_thy time initiators dir str tasks = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

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

410 
val name = Path.implode (Path.base path); 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

411 
val dir' = Path.append dir (Path.dir path); 
23871  412 
val _ = member (op =) initiators name andalso error (cycle_msg initiators); 
7066  413 
in 
23974  414 
(case try (Graph.get_node (fst tasks)) name of 
24209  415 
SOME task => (task_finished task, tasks) 
23967  416 
 NONE => 
417 
let 

24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

418 
val (current, deps, parents) = check_deps dir' name 
23967  419 
handle ERROR msg => cat_error msg 
420 
(loader_msg "the error(s) above occurred while examining theory" [name] ^ 

421 
required_by "\n" initiators); 

422 
val parent_names = map base_name parents; 

23871  423 

23974  424 
val (parents_current, (tasks_graph', tasks_len')) = 
24175
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

425 
require_thys time (name :: initiators) 
38a15a3a1aad
theory loader: removed obsolete update_thy (coincides with use_thy);
wenzelm
parents:
24151
diff
changeset

426 
(Path.append dir (master_dir' deps)) parents tasks; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

427 

23967  428 
val all_current = current andalso parents_current; 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

429 
val _ = if not all_current andalso known_thy name then outdate_thy name else (); 
25030  430 
val entry = 
431 
if all_current then (deps, SOME (get_theory name)) 

432 
else (read_text deps, NONE); 

433 
val _ = change_thys (new_deps name parent_names entry); 

23967  434 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

435 
val upd_time = serial (); 
23974  436 
val tasks_graph'' = tasks_graph' > new_deps name parent_names 
24209  437 
(if all_current then Finished 
27843  438 
else Task (fn () => load_thy time upd_time initiators name)); 
23974  439 
val tasks_len'' = if all_current then tasks_len' else tasks_len' + 1; 
440 
in (all_current, (tasks_graph'', tasks_len'')) end) 

7066  441 
end; 
6484
3f098b0ec683
use_thy etc.: may specify path prefix, which is temporarily used as load path;
wenzelm
parents:
6389
diff
changeset

442 

23967  443 
end; 
444 

445 

24209  446 
(* use_thy etc. *) 
23967  447 

448 
local 

449 

24057
f42665561801
removed obsolete Output.ML_errors/toplevel_errors;
wenzelm
parents:
23982
diff
changeset

450 
fun gen_use_thy' req dir arg = 
24209  451 
let val (_, (tasks, n)) = req [] dir arg (Graph.empty, 0) 
452 
in schedule_tasks tasks n end; 

6241  453 

23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

454 
fun gen_use_thy req str = 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

455 
let val name = base_name str in 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

456 
check_unfinished warning name; 
25994  457 
gen_use_thy' req Path.current str 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

458 
end; 
7244  459 

7211  460 
in 
461 

24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

462 
val use_thys_dir = gen_use_thy' (require_thys false); 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

463 
val use_thys = use_thys_dir Path.current; 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

464 
val use_thy = gen_use_thy (require_thy false); 
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

465 
val time_use_thy = gen_use_thy (require_thy true); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

466 

7211  467 
end; 
468 

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

469 

27495
d2bb5d61b392
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
wenzelm
parents:
27345
diff
changeset

470 
(* remove theory *) 
6666  471 

472 
fun remove_thy name = 

7910  473 
if is_finished name then error (loader_msg "cannot remove finished theory" [name]) 
6666  474 
else 
475 
let val succs = thy_graph Graph.all_succs [name] in 

9778  476 
priority (loader_msg "removing" succs); 
23939  477 
CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs))) 
6666  478 
end; 
479 

27495
d2bb5d61b392
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
wenzelm
parents:
27345
diff
changeset

480 
val kill_thy = if_known_thy remove_thy; 
d2bb5d61b392
moved and renamed IsarCmd.kill_theory to ThyInfo.kill_thy;
wenzelm
parents:
27345
diff
changeset

481 

6666  482 

24563  483 
(* update_time *) 
484 

485 
structure UpdateTime = TheoryDataFun 

486 
( 

487 
type T = int; 

488 
val empty = 0; 

489 
val copy = I; 

490 
fun extend _ = empty; 

491 
fun merge _ _ = empty; 

492 
); 

493 

494 
val thy_ord = int_ord o pairself UpdateTime.get; 

495 

496 

7066  497 
(* begin / end theory *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

498 

23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

499 
fun begin_theory name parents uses int = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

500 
let 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

501 
val parent_names = map base_name parents; 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

502 
val dir = master_dir'' (lookup_deps name); 
7244  503 
val _ = check_unfinished error name; 
24186
d7f267b806c9
check_deps: really do reload the master text if required;
wenzelm
parents:
24175
diff
changeset

504 
val _ = if int then use_thys_dir dir parents else (); 
17365  505 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

506 
val theory = Theory.begin_theory name (map get_theory parent_names); 
23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

507 

7952  508 
val deps = 
509 
if known_thy name then get_deps name 

24068  510 
else init_deps NONE [] parents (map #1 uses); 
23967  511 
val _ = change_thys (new_deps name parent_names (deps, NONE)); 
9451  512 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

513 
val update_time = (case deps of NONE => 0  SOME {update_time, ...} => update_time); 
24563  514 
val update_time = if update_time > 0 then update_time else serial (); 
515 
val theory' = theory 

516 
> UpdateTime.put update_time 

517 
> Present.begin_theory update_time dir uses; 

24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

518 

23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

519 
val uses_now = map_filter (fn (x, true) => SOME x  _ => NONE) uses; 
26494  520 
val theory'' = fold (Context.theory_map o exec_file false) uses_now theory'; 
24151
255f76dcc16b
replaced outdated flag by update_time (multithreadingsafe presentation order);
wenzelm
parents:
24133
diff
changeset

521 
in theory'' end; 
7244  522 

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

523 
fun end_theory theory = 
7099  524 
let 
16454  525 
val name = Context.theory_name theory; 
24190  526 
val _ = check_files name; 
16504  527 
val theory' = Theory.end_theory theory; 
23900
b25b1444a246
begin_theory: simplified interface, keep thy info empty until end_theory;
wenzelm
parents:
23893
diff
changeset

528 
val _ = change_thy name (fn (deps, _) => (deps, SOME theory')); 
27579  529 
in () end; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

530 

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

531 

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

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

533 

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

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

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

536 
val _ = priority ("Registering theory " ^ quote name); 
24563  537 
val thy = get_theory name; 
24096  538 
val _ = map get_theory (get_parents name); 
539 
val _ = check_unfinished error name; 

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

540 
val _ = touch_thy name; 
24190  541 
val master = #master (ThyLoad.deps_thy Path.current name); 
24563  542 
val upd_time = UpdateTime.get thy; 
24080
8c67d869531b
added register_thy (replaces pretend_use_thy_only and really flag);
wenzelm
parents:
24071
diff
changeset

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

544 
CRITICAL (fn () => 
24190  545 
(change_deps name (Option.map 
546 
(fn {parents, files, ...} => make_deps upd_time (SOME master) [] parents files)); 

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

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

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

549 

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

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

551 
let 
16454  552 
val name = Context.theory_name theory; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

553 
val parents = Theory.parents_of theory; 
16454  554 
val parent_names = map Context.theory_name parents; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

555 

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

556 
fun err txt bads = 
23871  557 
error (loader_msg txt bads ^ "\ncannot register theory " ^ quote name); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

558 

6666  559 
val nonfinished = filter_out is_finished parent_names; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

560 
fun get_variant (x, y_name) = 
15531  561 
if Theory.eq_thy (x, get_theory y_name) then NONE 
562 
else SOME y_name; 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

563 
val variants = map_filter get_variant (parents ~~ parent_names); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

564 

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

565 
fun register G = 
15531  566 
(Graph.new_node (name, (NONE, SOME theory)) G 
9327  567 
handle Graph.DUP _ => err "duplicate theory entry" []) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

568 
> add_deps name parent_names; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

569 
in 
6666  570 
if not (null nonfinished) then err "nonfinished parent theories" nonfinished 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

571 
else if not (null variants) then err "different versions of parent theories" variants 
23939  572 
else CRITICAL (fn () => (change_thys register; perform Update name)) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

574 

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

575 

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

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

577 

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

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

579 

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

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

581 