12 val get_names: unit -> string list |
12 val get_names: unit -> string list |
13 val lookup_theory: string -> theory option |
13 val lookup_theory: string -> theory option |
14 val get_theory: string -> theory |
14 val get_theory: string -> theory |
15 val master_directory: string -> Path.T |
15 val master_directory: string -> Path.T |
16 val remove_thy: string -> unit |
16 val remove_thy: string -> unit |
17 val use_theories: |
17 type context = |
18 {document: bool, |
18 {options: Options.T, |
19 symbols: HTML.symbols, |
19 symbols: HTML.symbols, |
20 bibtex_entries: string list, |
20 bibtex_entries: string list, |
21 last_timing: Toplevel.transition -> Time.time, |
21 last_timing: Toplevel.transition -> Time.time} |
22 qualifier: string, |
22 val use_theories: context -> string -> Path.T -> (string * Position.T) list -> unit |
23 master_dir: Path.T} -> (string * Position.T) list -> unit |
|
24 val use_thy: string -> unit |
23 val use_thy: string -> unit |
25 val script_thy: Position.T -> string -> theory -> theory |
24 val script_thy: Position.T -> string -> theory -> theory |
26 val register_thy: theory -> unit |
25 val register_thy: theory -> unit |
27 val finish: unit -> unit |
26 val finish: unit -> unit |
28 end; |
27 end; |
151 val thys' = remove name thys; |
150 val thys' = remove name thys; |
152 val _ = map (get thys') parents; |
151 val _ = map (get thys') parents; |
153 in new_entry name parents (SOME deps, SOME theory) thys' end; |
152 in new_entry name parents (SOME deps, SOME theory) thys' end; |
154 |
153 |
155 fun update_thy deps theory = change_thys (update deps theory); |
154 fun update_thy deps theory = change_thys (update deps theory); |
|
155 |
|
156 |
|
157 (* context *) |
|
158 |
|
159 type context = |
|
160 {options: Options.T, |
|
161 symbols: HTML.symbols, |
|
162 bibtex_entries: string list, |
|
163 last_timing: Toplevel.transition -> Time.time}; |
|
164 |
|
165 fun default_context (): context = |
|
166 {options = Options.default (), |
|
167 symbols = HTML.no_symbols, |
|
168 bibtex_entries = [], |
|
169 last_timing = K Time.zeroTime}; |
156 |
170 |
157 |
171 |
158 (* scheduling loader tasks *) |
172 (* scheduling loader tasks *) |
159 |
173 |
160 datatype result = |
174 datatype result = |
257 fold_map element_result elements (Toplevel.toplevel, Position.none); |
271 fold_map element_result elements (Toplevel.toplevel, Position.none); |
258 |
272 |
259 val thy = Toplevel.end_theory end_pos end_state; |
273 val thy = Toplevel.end_theory end_pos end_state; |
260 in (results, thy) end; |
274 in (results, thy) end; |
261 |
275 |
262 fun eval_thy {document, symbols, bibtex_entries, last_timing} update_time master_dir header |
276 fun eval_thy (context: context) update_time master_dir header text_pos text parents = |
263 text_pos text parents = |
277 let |
264 let |
278 val {options, symbols, bibtex_entries, last_timing} = context; |
265 val (name, _) = #name header; |
279 val (name, _) = #name header; |
266 val keywords = |
280 val keywords = |
267 fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents |
281 fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents |
268 (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); |
282 (Keyword.add_keywords (#keywords header) Keyword.empty_keywords); |
269 |
283 |
286 val _ = apply_presentation thy; |
300 val _ = apply_presentation thy; |
287 in |
301 in |
288 if exists (Toplevel.is_skipped_proof o #result_state) segments then () |
302 if exists (Toplevel.is_skipped_proof o #result_state) segments then () |
289 else |
303 else |
290 let val body = Thy_Output.present_thy thy segments; |
304 let val body = Thy_Output.present_thy thy segments; |
291 in if document then Present.theory_output text_pos thy body else () end |
305 in if Present.document_enabled options then Present.theory_output text_pos thy body else () end |
292 end; |
306 end; |
293 in (thy, present, size text) end; |
307 in (thy, present, size text) end; |
294 |
308 |
295 |
309 |
296 (* require_thy -- checking database entries wrt. the file-system *) |
310 (* require_thy -- checking database entries wrt. the file-system *) |
399 end; |
413 end; |
400 |
414 |
401 |
415 |
402 (* use theories *) |
416 (* use theories *) |
403 |
417 |
404 fun use_theories {document, symbols, bibtex_entries, last_timing, qualifier, master_dir} imports = |
418 fun use_theories context qualifier master_dir imports = |
405 let |
419 let val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty |
406 val context = |
|
407 {document = document, symbols = symbols, bibtex_entries = bibtex_entries, |
|
408 last_timing = last_timing}; |
|
409 val (_, tasks) = require_thys context [] qualifier master_dir imports String_Graph.empty; |
|
410 in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; |
420 in if Multithreading.max_threads () > 1 then schedule_futures tasks else schedule_seq tasks end; |
411 |
421 |
412 fun use_thy name = |
422 fun use_thy name = |
413 use_theories |
423 use_theories (default_context ()) Resources.default_qualifier |
414 {document = false, symbols = HTML.no_symbols, bibtex_entries = [], |
424 Path.current [(name, Position.none)]; |
415 last_timing = K Time.zeroTime, qualifier = Resources.default_qualifier, |
|
416 master_dir = Path.current} |
|
417 [(name, Position.none)]; |
|
418 |
425 |
419 |
426 |
420 (* toplevel scripting -- without maintaining database *) |
427 (* toplevel scripting -- without maintaining database *) |
421 |
428 |
422 fun script_thy pos txt thy = |
429 fun script_thy pos txt thy = |