Commit fa85d779 authored by MARCHE Claude's avatar MARCHE Claude

call callbacks in right order in schedule_proof_attempt

parent 2b0dd662
......@@ -426,13 +426,14 @@ let schedule_proof_attempt_r ?proof_script c id pr ~counterexmp ~limit ~callback
let schedule_proof_attempt ?proof_script c id pr
~counterexmp ~limit ~callback ~notification =
let callback panid s = callback panid s;
let callback panid s =
(match s with
| Scheduled | Running -> update_goal_node notification c.controller_session id
| Done res ->
update_proof_attempt ~obsolete:false c.controller_session id pr res;
update_goal_node notification c.controller_session id
| _ -> ())
| _ -> ());
callback panid s
(* proof_script is specific to interactive manual provers *)
let session_dir = Session_itp.get_dir c.controller_session in
......@@ -769,6 +769,8 @@ let update_theory_node notification s th =
let proved = List.for_all (pn_proved s) goals in
if proved <> th_proved s th then
Debug.dprintf debug "[Session] setting theory %s to status proved=%b@."
th.theory_name.Ident.id_string proved;
Hid.replace s.th_state (theory_name th) proved;
notification (ATh th);
try let p = theory_parent s th in
......@@ -784,6 +786,8 @@ let rec update_goal_node notification s id =
let proved = List.exists (tn_proved s) tr_list || List.exists pa_ok pa_list in
if proved <> pn_proved s id then
Debug.dprintf debug "[Session] setting goal node %a to status proved=%b@."
print_proofNodeID id proved;
Hpn.replace s.pn_state id proved;
notification (APn id);
match get_proof_parent s id with
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment