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
+ match self#script#grafite_status#ng_status with
ProofMode tstatus -> self#_loadNObj tstatus#obj
| _ -> self#blank ()