398 val initial' = initial andalso |
398 val initial' = initial andalso |
399 (case prev of |
399 (case prev of |
400 NONE => true |
400 NONE => true |
401 | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id)))); |
401 | SOME id => not (Keyword.is_theory_begin (#1 (the_command state id)))); |
402 in (visible', initial') end; |
402 in (visible', initial') end; |
403 fun get_common ((prev, id), opt_exec) (found, (_, flags)) = |
403 fun get_common ((prev, id), opt_exec) (same, (_, flags)) = |
404 if found then NONE |
404 if same then |
405 else |
405 let |
406 let val found' = |
406 val flags' = update_flags prev flags; |
407 (case opt_exec of |
407 val same' = |
408 NONE => true |
408 (case opt_exec of |
409 | SOME (exec_id, exec) => |
409 NONE => false |
410 (case lookup_entry node0 id of |
410 | SOME (exec_id, exec) => |
411 NONE => true |
411 (case lookup_entry node0 id of |
412 | SOME (exec_id0, _) => exec_id <> exec_id0) orelse not (stable_command exec)); |
412 NONE => false |
413 in SOME (found', (prev, update_flags prev flags)) end; |
413 | SOME (exec_id0, _) => exec_id = exec_id0 andalso stable_command exec)); |
414 val (found, (common, flags)) = |
414 in SOME (same', (prev, flags')) end |
415 iterate_entries get_common node (false, (NONE, (true, true))); |
415 else NONE; |
|
416 val (same, (common, flags)) = |
|
417 iterate_entries get_common node (true, (NONE, (true, true))); |
416 in |
418 in |
417 if found then (common, flags) |
419 if same then |
418 else |
|
419 let val last = Entries.get_after (get_entries node) common |
420 let val last = Entries.get_after (get_entries node) common |
420 in (last, update_flags last flags) end |
421 in (last, update_flags last flags) end |
|
422 else (common, flags) |
421 end; |
423 end; |
422 |
424 |
423 fun illegal_init () = error "Illegal theory header after end of theory"; |
425 fun illegal_init () = error "Illegal theory header after end of theory"; |
424 |
426 |
425 fun new_exec state proper_init command_id' (execs, command_exec, init) = |
427 fun new_exec state proper_init command_id' (execs, command_exec, init) = |