sequents_viewer#reset;
match grafite_status#proof_status with
| Incomplete_proof ({ stack = stack } as incomplete_proof) ->
- sequents_viewer#load_sequents incomplete_proof;
+ sequents_viewer#load_sequents grafite_status incomplete_proof;
(try
script#setGoal (Some (Continuationals.Stack.find_goal stack));
let goal =
None -> assert false
| Some n -> n
in
- sequents_viewer#goto_sequent goal
+ sequents_viewer#goto_sequent grafite_status goal
with Failure _ -> script#setGoal None);
| Proof proof -> sequents_viewer#load_logo_with_qed
| No_proof ->
None -> assert false
| Some n -> n
in
- sequents_viewer#goto_sequent goal
+ sequents_viewer#goto_sequent grafite_status goal
with Failure _ -> script#setGoal None);
| `CommandMode -> sequents_viewer#load_logo
)