-let new_proof proof =
- (* TODO Zack: high level function which create a new proof object and register
- * to it the widgets which must be refreshed upon status changes *)
-(* proof#status#attach ... *)
- proof#status#notify ();
+let new_proof (proof: MatitaTypes.proof) =
+ let xmldump_observer _ _ = print_endline proof#toString in
+ let proof_observer _ (status, ()) =
+ debug_print "proof_observer";
+ let ((uri_opt, _, _, _), _) = status in
+ let uri = MatitaTypes.unopt_uri uri_opt in
+ debug_print "apply transformation";
+ proof_viewer#load_proof status;
+ debug_print "/proof_observer"
+ in
+ let sequents_observer _ (((_, metasenv, _, _), goal_opt), ()) =
+ sequents_viewer#reset;
+ (match goal_opt with
+ | None -> ()
+ | Some goal ->
+ sequents_viewer#load_sequents metasenv;
+ sequents_viewer#goto_sequent goal)
+ in
+ ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
+ sequents_observer);
+ ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
+ proof_observer);
+ ignore (proof#attach_observer ~interested_in:StatefulProofEngine.all_events
+ xmldump_observer);
+ proof#notify;