-
Johannes Kanig authored
When Why3 is run on a file where some theories have been suppressed, it will delete the corresponding theories from the session file. We now add an option keep_unmatched_theories to Session.update_session, which keeps all theories. In this commit, this option is always disabled. This is useful for SPARK, which sometimes only generates part of the Why3 file for efficiency reasons, but doesn't want the session file to be damaged because of that. * session.ml (import_theory) (import_goal) (import_proof_attempt) (import_transf): new functions to copy a session tree from an old session file (merge_file): keep old theories when keep_unmatched_theories is true * session_scheduler.ml (update_session): pass keep_unmatched_theories * why3session_lib.ml (read_update_session): pass keep_unmatched_theories
4c744eba