+ | No_proof ->
+ (match grafite_status.ng_status with
+ ProofMode nstatus ->
+ sequents_viewer#nload_sequents nstatus;
+ (try
+ script#setGoal (Some (Continuationals.Stack.find_goal nstatus.NTacStatus.gstatus));
+ let goal =
+ match script#goal with
+ None -> assert false
+ | Some n -> n
+ in
+ sequents_viewer#goto_sequent goal
+ with Failure _ -> script#setGoal None);
+ | CommandMode _ -> sequents_viewer#load_logo
+ )