sequents_viewer#goto_sequent goal
with Failure _ -> script#setGoal None);
| Proof proof -> sequents_viewer#load_logo_with_qed
- | No_proof -> sequents_viewer#load_logo
+ | 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
+ )
| Intermediate _ -> assert false (* only the engine may be in this state *)
in
script#addObserver sequents_observer;
(fun cmd ->
prerr_endline
(GrafiteAstPp.pp_command
- ~term_pp:(fun _ -> assert false)
+ ~term_pp:(fun t -> CicPp.ppterm t)
~obj_pp:(fun _ -> assert false)
cmd))
(List.rev moo));