107 fun get_result (Node {result, ...}) = result; |
107 fun get_result (Node {result, ...}) = result; |
108 fun set_result result = |
108 fun set_result result = |
109 map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); |
109 map_node (fn (header, perspective, entries, _) => (header, perspective, entries, result)); |
110 |
110 |
111 fun finished_theory node = |
111 fun finished_theory node = |
112 (case Exn.capture (Command.eval_result o the) (get_result node) of |
112 (case Exn.capture (Command.eval_result_state o the) (get_result node) of |
113 Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st |
113 Exn.Res st => can (Toplevel.end_theory Position.none) st |
114 | _ => false); |
114 | _ => false); |
115 |
115 |
116 fun get_node nodes name = String_Graph.get_node nodes name |
116 fun get_node nodes name = String_Graph.get_node nodes name |
117 handle String_Graph.UNDEF _ => empty_node; |
117 handle String_Graph.UNDEF _ => empty_node; |
118 fun default_node name = String_Graph.default_node (name, empty_node); |
118 fun default_node name = String_Graph.default_node (name, empty_node); |
345 imports |> map (fn (import, _) => |
345 imports |> map (fn (import, _) => |
346 (case Thy_Info.lookup_theory import of |
346 (case Thy_Info.lookup_theory import of |
347 SOME thy => thy |
347 SOME thy => thy |
348 | NONE => |
348 | NONE => |
349 Toplevel.end_theory (Position.file_only import) |
349 Toplevel.end_theory (Position.file_only import) |
350 (#state |
350 (Command.eval_result_state |
351 (Command.eval_result |
351 (the_default Command.no_eval |
352 (the_default Command.no_eval |
352 (get_result (snd (the (AList.lookup (op =) deps import)))))))); |
353 (get_result (snd (the (AList.lookup (op =) deps import))))))))); |
|
354 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); |
353 val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents); |
355 in Thy_Load.begin_theory master_dir header parents end; |
354 in Thy_Load.begin_theory master_dir header parents end; |
356 |
355 |
357 fun check_theory full name node = |
356 fun check_theory full name node = |
358 is_some (Thy_Info.lookup_theory name) orelse |
357 is_some (Thy_Info.lookup_theory name) orelse |
389 let val last = Entries.get_after (get_entries node) common |
388 let val last = Entries.get_after (get_entries node) common |
390 in (last, update_flags last flags) end |
389 in (last, update_flags last flags) end |
391 else (common, flags) |
390 else (common, flags) |
392 end; |
391 end; |
393 |
392 |
|
393 fun illegal_init _ = error "Illegal theory header after end of theory"; |
|
394 |
394 fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) = |
395 fun new_exec state proper_init command_visible command_id' (execs, command_exec, init) = |
395 if not proper_init andalso is_none init then NONE |
396 if not proper_init andalso is_none init then NONE |
396 else |
397 else |
397 let |
398 let |
|
399 val (_, (eval, _)) = command_exec; |
398 val (command_name, span) = the_command state command_id' ||> Lazy.force; |
400 val (command_name, span) = the_command state command_id' ||> Lazy.force; |
399 |
401 val init' = if Keyword.is_theory_begin command_name then NONE else init; |
400 fun illegal_init _ = error "Illegal theory header after end of theory"; |
402 val eval' = Command.eval (fn () => the_default illegal_init init span) span eval; |
401 val (modify_init, init') = |
|
402 if Keyword.is_theory_begin command_name then |
|
403 (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE) |
|
404 else (I, init); |
|
405 |
|
406 val exec_id' = Document_ID.make (); |
|
407 val eval_body' = |
|
408 Command.memo (fn () => |
|
409 let |
|
410 val eval_state = Command.exec_result (snd command_exec); |
|
411 val tr = |
|
412 Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id')) |
|
413 (fn () => |
|
414 Command.read span |
|
415 |> modify_init |
|
416 |> Toplevel.put_id exec_id') (); |
|
417 in Command.eval span tr eval_state end); |
|
418 val eval' = {exec_id = exec_id', eval = eval_body'}; |
|
419 val prints' = if command_visible then Command.print command_name eval' else []; |
403 val prints' = if command_visible then Command.print command_name eval' else []; |
420 val command_exec' = (command_id', (eval', prints')); |
404 val command_exec' = (command_id', (eval', prints')); |
421 in SOME (command_exec' :: execs, command_exec', init') end; |
405 in SOME (command_exec' :: execs, command_exec', init') end; |
422 |
406 |
423 fun update_prints state node command_id = |
407 fun update_prints state node command_id = |