author  wenzelm 
Sat, 21 Jul 2007 17:40:40 +0200  
changeset 23893  8babfcaaf129 
parent 23886  f40fba467384 
child 23900  b25b1444a246 
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 

5209  9 
signature BASIC_THY_INFO = 
10 
sig 

11 
val theory: string > theory 

6241  12 
(*val use: string > unit*) (*exported later*) 
13 
val time_use: string > unit 

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

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

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

16 
val update_thy: string > unit 
6666  17 
val remove_thy: string > unit 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

19 
end; 
5209  20 

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

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

22 
sig 
5209  23 
include BASIC_THY_INFO 
7099  24 
datatype action = Update  Outdate  Remove 
25 
val str_of_action: action > string 

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

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

27 
val names: unit > string list 
7910  28 
val known_thy: string > bool 
7935  29 
val check_known_thy: string > bool 
30 
val if_known_thy: (string > unit) > string > unit 

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

32 
val get_theory: string > theory 
19547  33 
val the_theory: string > theory > theory 
23871  34 
val get_parents: string > string list 
7935  35 
val loaded_files: string > Path.T list 
7910  36 
val touch_child_thys: string > unit 
7099  37 
val touch_all_thys: unit > unit 
7941  38 
val load_file: bool > Path.T > unit 
6241  39 
val use: string > unit 
9822  40 
val pretend_use_thy_only: string > unit 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

41 
val begin_theory: (Path.T > string > string list > 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

42 
(Path.T * bool) list > theory > theory) > 
17365  43 
string > string list > (Path.T * bool) list > bool > theory 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

44 
val end_theory: theory > theory 
6666  45 
val finish: unit > unit 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

46 
val register_theory: theory > unit 
15633  47 
val pretty_theory: theory > Pretty.T 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

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

49 

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

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

52 

7099  53 
(** theory loader actions and hooks **) 
54 

55 
datatype action = Update  Outdate  Remove; 

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

57 

58 
local 

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

60 
in 

61 
fun add_hook f = hooks := f :: ! hooks; 

15570  62 
fun perform action name = List.app (fn f => (try (fn () => f action name) (); ())) (! hooks); 
7099  63 
end; 
64 

65 

66 

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

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

70 

23871  71 
fun loader_msg txt [] = "Theory loader: " ^ txt 
72 
 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

73 

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

74 
val show_path = space_implode " via " o map quote; 
9332  75 
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

76 

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

77 

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

79 

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

82 

7952  83 
fun upd_deps name entry G = 
19473  84 
fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G 
7952  85 
> Graph.map_node name (K entry); 
3976  86 

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

87 
fun update_node name parents entry G = 
7952  88 
(if can (Graph.get_node G) name then upd_deps name entry G else Graph.new_node (name, entry) G) 
89 
> add_deps name parents; 

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

90 

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

91 

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

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

93 

23871  94 
type master = (Path.T * File.ident) * (Path.T * File.ident) option; 
95 

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

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

97 
{present: bool, (*theory value present*) 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

98 
outdated: bool, (*entry considered outdated*) 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

99 
master: master option, (*master dependencies for thy + attached ML file*) 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

100 
parents: string list, (*source specification of parents (partially qualified)*) 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

101 
files: (*auxiliary files: source path, physical path + identifier*) 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

102 
(Path.T * (Path.T * File.ident) option) list}; 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

103 

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

104 
fun make_deps present outdated master parents files : deps = 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

105 
{present = present, outdated = outdated, master = master, parents = parents, files = files}; 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

106 

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

107 
fun init_deps master parents files = 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

108 
SOME (make_deps false true master parents (map (rpair NONE) files)); 
23871  109 

110 
fun master_idents (NONE: master option) = [] 

111 
 master_idents (SOME ((_, thy_id), NONE)) = [thy_id] 

112 
 master_idents (SOME ((_, thy_id), SOME (_, ml_id))) = [thy_id, ml_id]; 

113 

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

114 
fun master_dir (NONE: master option) = Path.current 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

115 
 master_dir (SOME ((path, _), _)) = Path.dir path; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

116 

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

117 
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

118 
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

119 

7211  120 

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

122 

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

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

125 
in 
6362  126 
fun get_thys () = ! database; 
9137  127 
val change_thys = Library.change database; 
3604
6bf9f09f3d61
Moved functions for theory information storage / retrieval
berghofe
parents:
diff
changeset

128 
end; 
5209  129 

130 

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

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

132 

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

133 
fun thy_graph f x = f (get_thys ()) x; 
9417  134 

135 
(*theory names in topological order*) 

136 
fun get_names () = 

137 
let val G = get_thys () 

14774  138 
in Graph.all_succs G (Graph.minimals G) end; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

139 

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

140 

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

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

142 

7935  143 
fun lookup_thy name = 
15531  144 
SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE; 
7935  145 

16047  146 
val known_thy = is_some o lookup_thy; 
7935  147 
fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false); 
148 
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

149 

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

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

151 
(case lookup_thy name of 
15531  152 
SOME thy => thy 
153 
 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

154 

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

155 
fun change_thy name f = (get_thy name; change_thys (Graph.map_node name f)); 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

156 

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

157 

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

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

159 

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

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

162 
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

163 

6666  164 
fun is_finished name = is_none (get_deps name); 
15531  165 
fun get_files name = (case get_deps name of SOME {files, ...} => files  _ => []); 
7191  166 

167 
fun loaded_files name = 

168 
(case get_deps name of 

15531  169 
NONE => [] 
170 
 SOME {master, files, ...} => 

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

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

173 

23871  174 
fun get_parents name = 
9327  175 
(thy_graph Graph.imm_preds name) handle Graph.UNDEF _ => 
6654  176 
error (loader_msg "nothing known about theory" [name]); 
177 

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

178 

16047  179 
(* pretty printing a theory *) 
180 

181 
local 

15633  182 

16047  183 
fun relevant_names names = 
184 
let 

185 
val (finished, unfinished) = 

19305  186 
List.filter (fn name => name = Context.draftN orelse known_thy name) names 
187 
> List.partition (fn name => name <> Context.draftN andalso is_finished name); 

16047  188 
in (if not (null finished) then [List.last finished] else []) @ unfinished end; 
15633  189 

16047  190 
in 
15633  191 

16454  192 
fun pretty_theory thy = 
193 
Pretty.str_list "{" "}" (relevant_names (Context.names_of thy)); 

15633  194 

16047  195 
end; 
196 

15633  197 

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

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

199 

7687  200 
fun lookup_theory name = 
201 
(case lookup_thy name of 

15531  202 
SOME (_, SOME thy) => SOME thy 
203 
 _ => NONE); 

7288  204 

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

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

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

209 

19547  210 
fun the_theory name thy = 
211 
if Context.theory_name thy = name then thy 

212 
else get_theory name; 

213 

15531  214 
fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory)); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

215 

22137  216 
val _ = ML_Context.value_antiq "theory" 
217 
(Scan.lift Args.name 

218 
>> (fn name => (name ^ "_thy", "ThyInfo.theory " ^ ML_Syntax.print_string name)) 

22148  219 
 Scan.succeed ("thy", "ML_Context.the_context ()")); 
22137  220 

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

221 

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

222 

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

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

224 

6241  225 
(* maintain 'outdated' flag *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

226 

7099  227 
local 
228 

6241  229 
fun is_outdated name = 
230 
(case lookup_deps name of 

15531  231 
SOME (SOME {outdated, ...}) => outdated 
6241  232 
 _ => false); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

233 

6241  234 
fun outdate_thy name = 
7099  235 
if is_finished name orelse is_outdated name then () 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

236 
else (change_deps name (Option.map (fn {present, outdated = _, master, parents, files} => 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

237 
make_deps present true master parents files)); perform Outdate name); 
7099  238 

7910  239 
fun check_unfinished name = 
15531  240 
if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE) 
241 
else SOME name; 

7910  242 

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

244 

7910  245 
fun touch_thys names = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

246 
List.app outdate_thy (thy_graph Graph.all_succs (map_filter check_unfinished names)); 
7910  247 

248 
fun touch_thy name = touch_thys [name]; 

249 
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

250 

15570  251 
fun touch_all_thys () = List.app outdate_thy (get_names ()); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

252 

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

254 

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

255 

7244  256 
(* check 'finished' state *) 
257 

258 
fun check_unfinished fail name = 

7910  259 
if known_thy name andalso is_finished name then 
7288  260 
fail (loader_msg "cannot update finished theory" [name]) 
7244  261 
else (); 
262 

263 

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

265 

7191  266 
local 
267 

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

268 
fun provide path name info (deps as SOME {present, outdated, master, parents, files}) = 
23871  269 
(if AList.defined (op =) files path then () 
7941  270 
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

271 
" on file: " ^ quote (Path.implode path)); 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

272 
SOME (make_deps present outdated master parents 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

273 
(AList.update (op =) (path, SOME info) files))) 
15531  274 
 provide _ _ _ NONE = NONE; 
7941  275 

276 
fun run_file path = 

22095
07875394618e
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
22086
diff
changeset

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

278 
NONE => (ThyLoad.load_ml Path.current path; ()) 
23871  279 
 SOME name => 
280 
(case lookup_deps name of 

281 
SOME deps => 

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

282 
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

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

284 

7191  285 
in 
286 

18721  287 
fun load_file time path = Output.toplevel_errors (fn () => 
7941  288 
if time then 
21858
05f57309170c
avoid conflict with Alice keywords: renamed pack > implode, unpack > explode, any > many, avoided assert;
wenzelm
parents:
20664
diff
changeset

289 
let val name = Path.implode path in 
7244  290 
timeit (fn () => 
9778  291 
(priority ("\n**** Starting file " ^ quote name ^ " ****"); 
9036  292 
run_file path; 
9778  293 
priority ("**** Finished file " ^ quote name ^ " ****\n"))) 
7244  294 
end 
18721  295 
else run_file path) (); 
7941  296 

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

297 
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

298 
val time_use = load_file true o Path.explode; 
7191  299 

300 
end; 

6233  301 

302 

7099  303 
(* load_thy *) 
304 

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

7099  307 

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

308 
fun load_thy really ml time initiators dir name = 
7099  309 
let 
9822  310 
val _ = 
311 
if really then priority ("Loading theory " ^ quote name ^ required_by " " initiators) 

312 
else priority ("Registering theory " ^ quote name); 

7099  313 

314 
val _ = touch_thy name; 

9822  315 
val master = 
23886
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

316 
if really then ThyLoad.load_thy dir name ml time 
f40fba467384
simplified ThyLoad interfaces: only one additional directory;
wenzelm
parents:
23871
diff
changeset

317 
else #1 (ThyLoad.deps_thy dir name ml); 
7099  318 

319 
val files = get_files name; 

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

320 
val missing_files = map_filter (fn (path, NONE) => SOME (Path.implode path)  _ => NONE) files; 
7099  321 
in 
322 
if null missing_files then () 

323 
else warning (loader_msg "unresolved dependencies of theory" [name] ^ 

7223  324 
" on file(s): " ^ commas_quote missing_files); 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

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

326 
(Option.map (fn {parents, ...} => make_deps true false (SOME master) parents files)); 
7099  327 
perform Update name 
328 
end; 

329 

330 

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

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

332 

23871  333 
fun base_name s = Path.implode (Path.base (Path.explode s)); 
15065  334 

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

336 

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

337 
fun check_ml master (src_path, info) = 
23871  338 
let val info' = 
339 
(case info of NONE => NONE 

340 
 SOME (_, id) => 

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

341 
(case ThyLoad.check_ml (master_dir master) src_path of NONE => NONE 
23871  342 
 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

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

344 

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

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

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

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

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

349 
let val (master, (parents, files)) = ThyLoad.deps_thy dir name ml 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

350 
in (false, init_deps (SOME master) parents files, parents) end 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

351 
 SOME (deps as SOME {present, outdated, master, parents, files}) => 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

352 
if present andalso not strict then (true, deps, parents) 
23871  353 
else 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

354 
let val master' = SOME (ThyLoad.check_thy dir name ml) in 
23871  355 
if master_idents master <> master_idents master' 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

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

357 
let val (parents', files') = #2 (ThyLoad.deps_thy dir name ml) 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

358 
in (false, init_deps master' parents' files', parents') end 
23871  359 
else 
360 
let 

361 
val checked_files = map (check_ml master') files; 

362 
val current = not outdated andalso forall (is_some o snd) checked_files; 

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

363 
val deps' = SOME (make_deps present (not current) master' parents checked_files); 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

364 
in (current, deps', parents) end 
23871  365 
end); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

366 

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

367 
fun require_thys really ml time strict keep_strict initiators dir strs visited = 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

368 
fold_map (require_thy really ml time strict keep_strict initiators dir) strs visited 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

369 
and require_thy really ml time strict keep_strict initiators dir str visited = 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

371 
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

372 
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

373 
val dir' = Path.append dir (Path.dir path); 
23871  374 
val _ = member (op =) initiators name andalso error (cycle_msg initiators); 
7066  375 
in 
23871  376 
if known_thy name andalso is_finished name orelse member (op =) visited name 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

377 
then (true, visited) 
7066  378 
else 
379 
let 

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

380 
val (current, deps, parents) = check_deps ml strict dir' name 
18678  381 
handle ERROR msg => cat_error msg 
382 
(loader_msg "the error(s) above occurred while examining theory" [name] ^ 

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

383 
required_by "\n" initiators); 
23871  384 

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

385 
val (parents_current, visited') = 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

386 
require_thys true true time (strict andalso keep_strict) keep_strict 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

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

388 

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

389 
val all_current = current andalso forall I parents_current; 
23871  390 
val thy = if all_current orelse not really then SOME (get_theory name) else NONE; 
391 
val _ = change_thys (update_node name (map base_name parents) (deps, thy)); 

392 
val _ = 

393 
if all_current then () 

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

394 
else load_thy really ml (time orelse ! Output.timing) initiators dir' name; 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

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

397 

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

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

399 
Output.toplevel_errors (fn () => (req [] dir arg []; ())) (); 
6241  400 

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

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

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

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

404 
gen_use_thy' req Path.current str; 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

405 
ML_Context.set_context (SOME (Context.Theory (get_theory name))) 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

406 
end; 
7244  407 

7211  408 
in 
409 

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

410 
val quiet_update_thys = gen_use_thy' (require_thys true true false true true); 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

411 
val pretend_use_thy_only = gen_use_thy' (require_thy false false false true false) Path.current; 
7244  412 

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

413 
val use_thy = gen_use_thy (require_thy true true false true false); 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

414 
val time_use_thy = gen_use_thy (require_thy true true true true false); 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

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

416 

7211  417 
end; 
418 

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

419 

6666  420 
(* remove_thy *) 
421 

422 
fun remove_thy name = 

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

9778  426 
priority (loader_msg "removing" succs); 
15570  427 
List.app (perform Remove) succs; 
7191  428 
change_thys (Graph.del_nodes succs) 
6666  429 
end; 
430 

431 

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

433 

17365  434 
fun check_uses name uses = 
23871  435 
let val illegal = map (fn ext => Path.ext ext (Path.basic name)) ("" :: ThyLoad.ml_exts) in 
17365  436 
(case find_first (member (op =) illegal o Path.base o Path.expand o #1) uses of 
437 
NONE => () 

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

438 
 SOME (path, _) => error ("Illegal use of theory ML file: " ^ quote (Path.implode path))) 
17365  439 
end; 
440 

441 
fun begin_theory present name parents uses int = 

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

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

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

444 
val dir = master_dir'' (lookup_deps name); 
7244  445 
val _ = check_unfinished error name; 
23893
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

446 
val _ = if int then quiet_update_thys dir parents else (); 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

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

448 
val _ = ML_Context.set_context (SOME (Context.Theory (get_theory (List.last parent_names)))); 
17365  449 
val _ = check_uses name uses; 
450 

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

451 
val theory = Theory.begin_theory name (map get_theory parent_names); 
7952  452 
val deps = 
453 
if known_thy name then get_deps name 

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

454 
else init_deps NONE parents (map #1 uses); 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19473
diff
changeset

455 
val uses_now = map_filter (fn (x, true) => SOME x  _ => NONE) uses; 
9451  456 

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

457 
val _ = change_thys (update_node name parent_names (deps, SOME (Theory.copy theory))); 
8babfcaaf129
deps: maintain source specification of parents (prevents repeated ThyLoad.deps_thy);
wenzelm
parents:
23886
diff
changeset

458 
val theory' = theory > present dir name parent_names uses; 
9451  459 
val _ = put_theory name (Theory.copy theory'); 
22086  460 
val ((), theory'') = 
22095
07875394618e
moved ML context stuff to from Context to ML_Context;
wenzelm
parents:
22086
diff
changeset

461 
ML_Context.pass_context (Context.Theory theory') (List.app (load_file false)) uses_now 
22086  462 
> Context.the_theory; 
9451  463 
val _ = put_theory name (Theory.copy theory''); 
8805  464 
in theory'' end; 
7244  465 

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

466 
fun end_theory theory = 
7099  467 
let 
16454  468 
val name = Context.theory_name theory; 
16504  469 
val theory' = Theory.end_theory theory; 
7099  470 
in put_theory name theory'; theory' end; 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

471 

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

472 

6666  473 
(* finish all theories *) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

474 

15531  475 
fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry))); 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

476 

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

477 

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

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

479 

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

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

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

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

485 

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

486 
fun err txt bads = 
23871  487 
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

488 

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

490 
fun get_variant (x, y_name) = 
15531  491 
if Theory.eq_thy (x, get_theory y_name) then NONE 
492 
else SOME y_name; 

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

493 
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

494 

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

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

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

499 
in 
6666  500 
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

501 
else if not (null variants) then err "different versions of parent theories" variants 
7099  502 
else (change_thys register; perform Update name) 
6211
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

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

504 

15801  505 
val _ = register_theory ProtoPure.thy; 
506 

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

507 
(*final declarations of this structure*) 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

508 
val theory = get_theory; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

509 
val names = get_names; 
43d0efafa025
Theory loader database: theory and file dependencies, theory values
wenzelm
parents:
5211
diff
changeset

510 

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

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

512 

5209  513 
structure BasicThyInfo: BASIC_THY_INFO = ThyInfo; 
514 
open BasicThyInfo; 