end;
self#load_root ~root:mathml#get_documentElement
- method nload_sequent metasenv subst metano =
+ method nload_sequent:
+ 'status. #NCicCoercion.status as 'status -> NCic.metasenv ->
+ NCic.substitution -> int -> unit
+ = fun status metasenv subst metano ->
let sequent = List.assoc metano metasenv in
let mathml =
- ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent)
+ ApplyTransformation.nmml_of_cic_sequent status metasenv subst
+ (metano,sequent)
in
if BuildTimeConf.debug then begin
let name =
self#load_root ~root:mathml#get_documentElement;
current_mathml <- Some mathml);
- method load_nobject obj =
- let mathml = ApplyTransformation.nmml_of_cic_object obj in
+ method load_nobject :
+ 'status. #NCicCoercion.status as 'status -> NCic.obj -> unit
+ = fun status obj ->
+ let mathml = ApplyTransformation.nmml_of_cic_object status obj in
(*
self#set_cic_info
(Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
_metasenv <- `Old [];
self#script#setGoal None
- method load_sequents
- { proof = (_,metasenv,_subst,_,_, _) as proof; stack = stack }
- =
+ method load_sequents : 'status. #NCicCoercion.status as 'status -> 'a
+ = fun status { proof= (_,metasenv,_subst,_,_, _) as proof; stack = stack }
+ ->
_metasenv <- `Old metasenv;
pages <- 0;
let win goal_switch =
try List.assoc page page2goal with Not_found -> assert false
in
self#script#setGoal (Some (goal_of_switch goal_switch));
- self#render_page ~page ~goal_switch))
+ self#render_page status ~page ~goal_switch))
- method nload_sequents
- { NTacStatus.istatus = { NTacStatus.pstatus = (_,_,metasenv,subst,_) }; gstatus = stack }
- =
+ method nload_sequents : 'status. #NTacStatus.tac_status as 'status -> unit
+ = fun status ->
+ let _,_,metasenv,subst,_ = status#obj in
_metasenv <- `New (metasenv,subst);
pages <- 0;
let win goal_switch =
w#coerce
in
assert (
- let stack_goals = Stack.open_goals stack in
+ let stack_goals = Stack.open_goals status#stack in
let proof_goals = List.map fst metasenv in
if
HExtlib.list_uniq (List.sort Pervasives.compare stack_goals)
match depth, pos with
| 0, 0 -> `Current (render_switch sw)
| 0, _ -> `Shift (pos, `Current (render_switch sw))
- | 1, pos when Stack.head_tag stack = `BranchTag ->
+ | 1, pos when Stack.head_tag status#stack = `BranchTag ->
`Shift (pos, render_switch sw)
| _ -> render_switch sw
in
add_tab markup sw)
~cont:add_switch ~todo:add_switch
- stack;
+ status#stack;
switch_page_callback <-
Some (notebook#connect#switch_page ~callback:(fun page ->
let goal_switch =
try List.assoc page page2goal with Not_found -> assert false
in
self#script#setGoal (Some (goal_of_switch goal_switch));
- self#render_page ~page ~goal_switch))
+ self#render_page status ~page ~goal_switch))
- method private render_page ~page ~goal_switch =
+ method private render_page:
+ 'status. #NCicCoercion.status as 'status -> page:int ->
+ goal_switch:Stack.switch -> unit
+ = fun status ~page ~goal_switch ->
(match goal_switch with
| Stack.Open goal ->
(match _metasenv with
`Old menv -> cicMathView#load_sequent menv goal
- | `New (menv,subst) -> cicMathView#nload_sequent menv subst goal)
+ | `New (menv,subst) ->
+ cicMathView#nload_sequent status menv subst goal)
| Stack.Closed goal ->
let doc = Lazy.force closed_goal_mathml in
cicMathView#load_root ~root:doc#get_documentElement);
List.assoc goal_switch goal2win ()
with Not_found -> assert false)
- method goto_sequent goal =
+ method goto_sequent: 'status. #NCicCoercion.status as 'status -> int -> unit
+ = fun status goal ->
let goal_switch, page =
try
List.find
with Not_found -> assert false
in
notebook#goto_page page;
- self#render_page page goal_switch
+ self#render_page status ~page ~goal_switch
end
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 = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
+ let name = UriManager.name_of_uri (HExtlib.unopt uri) in
+ let obj =
+ Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs)
+ in
self#_loadObj obj
| Incomplete_proof { proof = (uri, metasenv, _subst, bo, ty, attrs) } ->
- let name = UriManager.name_of_uri (HExtlib.unopt uri) in
- let obj = Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs) in
+ let name = UriManager.name_of_uri (HExtlib.unopt uri) in
+ let obj =
+ Cic.CurrentProof (name, metasenv, Lazy.force bo, ty, [], attrs)
+ in
self#_loadObj obj
- | _ -> self#blank ()
+ | _ ->
+ match self#script#grafite_status#ng_mode with
+ `ProofMode ->
+ self#_loadNObj self#script#grafite_status
+ self#script#grafite_status#obj
+ | _ -> self#blank ()
(** loads a cic uri from the environment
* @param uri UriManager.uri *)
method private _loadNReference (NReference.Ref (uri,_)) =
let obj = NCicEnvironment.get_checked_obj uri in
- self#_loadNObj obj
+ self#_loadNObj self#script#grafite_status obj
method private _loadUnivs uri =
let uri = UriManager.strip_xpointer uri in
self#_showMath;
mathView#load_object obj
- method private _loadNObj obj =
+ method private _loadNObj status obj =
(* showMath must be done _before_ loading the document, since if the
* widget is not mapped (hidden by the notebook) the document is not
* rendered *)
self#_showMath;
- mathView#load_nobject obj
+ mathView#load_nobject status obj
method private _loadTermCic term metasenv =
let context = self#script#proofContext in
projects / helm.git / blobdiff