self#script#setGoal (Some (goal_of_switch goal_switch));
self#render_page ~page ~goal_switch))
- method nload_sequents (status : NTacStatus.tac_status) =
+ method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
+ = fun status ->
let _,_,metasenv,subst,_ = status#obj in
_metasenv <- `New (metasenv,subst);
pages <- 0;
method private home () =
self#_showMath;
- match self#script#grafite_status.proof_status with
+ match self#script#grafite_status#proof_status with
| Proof (uri, metasenv, _subst, bo, ty, attrs) ->
let name = UriManager.name_of_uri (HExtlib.unopt uri) in
let obj =
in
self#_loadObj obj
| _ ->
- match self#script#grafite_status.ng_status with
- ProofMode tstatus -> self#_loadNObj tstatus#obj
+ match self#script#grafite_status#ng_mode with
+ `ProofMode -> self#_loadNObj self#script#grafite_status#obj
| _ -> self#blank ()
(** loads a cic uri from the environment