method set_href_callback f = href_callback <- f
val mutable _cic_info = None
- val mutable _ncic_info = None
method private set_cic_info info = _cic_info <- info
method private cic_info = _cic_info
- method private set_ncic_info info = _ncic_info <- info
- method private ncic_info = _ncic_info
val normal_cursor = Gdk.Cursor.create `LEFT_PTR
val href_cursor = Gdk.Cursor.create `HAND2
info, (~-1, [], t) (* dummy sequent for obj *)
| None -> assert false
- method private get_ncic_info id =
- match self#ncic_info with
- | Some info -> info
- | None -> assert false
-
method private sequent_of_id ~(paste_kind:paste_kind) id =
let cic_info, unsh_sequent = self#get_cic_info id in
let cic_sequent =
method nload_sequent metasenv subst metano =
let sequent = List.assoc metano metasenv in
- let mathml,ids_to_father_ids =
+ let mathml =
ApplyTransformation.nmml_of_cic_sequent metasenv subst (metano,sequent)
in
- self#set_ncic_info (Some ids_to_father_ids);
if BuildTimeConf.debug then begin
let name =
"/tmp/sequent_viewer_" ^ string_of_int (Unix.getuid ()) ^ ".xml" in
current_mathml <- Some mathml);
method load_nobject obj =
- let mathml,ids_to_father_ids = ApplyTransformation.nmml_of_cic_object obj in
- self#set_ncic_info (Some ids_to_father_ids);
+ let mathml = ApplyTransformation.nmml_of_cic_object obj in
(*
+ self#set_cic_info
+ (Some (None, ids_to_terms, ids_to_hypotheses, ids_to_father_ids, ids_to_inner_types, Some annobj));
(match current_mathml with
| Some current_mathml when use_diff ->
self#freeze;
self#script#setGoal (Some (goal_of_switch goal_switch));
self#render_page ~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 =
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 ->
- let nobj = tstatus.NTacStatus.istatus.NTacStatus.pstatus in
- self#_loadNObj nobj
+ 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