+*)
+ let sequent = CicUtil.lookup_meta metano metasenv in
+ let (mathml,(_,(ids_to_terms, ids_to_father_ids, ids_to_hypotheses,_))) =
+ ApplyTransformation.mml_of_cic_sequent metasenv sequent
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
+ debug_print "load_sequent: dumping MathML to ./prova";
+ ignore (Misc.domImpl#saveDocumentToFile ~name:"./prova" ~doc:mathml ());
+ self#load_root ~root:mathml#get_documentElement
+ end
+
+
+class sequents_viewer ~(notebook:GPack.notebook)
+ ~(sequent_viewer:sequent_viewer) ~set_goal ()
+=
+ let tab_label metano =
+ (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
+ in
+ object (self)
+ val mutable pages = 0
+ val mutable switch_page_callback = None
+ val mutable page2goal = [] (* associative list: page no -> goal no *)
+ val mutable goal2page = [] (* the other way round *)
+ val mutable goal2win = [] (* associative list: goal no -> scrolled win *)
+ val mutable _metasenv = []
+
+ method reset =
+ for i = 1 to pages do notebook#remove_page 0 done;
+ pages <- 0;
+ page2goal <- [];
+ goal2page <- [];
+ goal2win <- [];
+ _metasenv <- [];
+ (match switch_page_callback with
+ | Some id ->
+ GtkSignal.disconnect notebook#as_widget id;
+ switch_page_callback <- None
+ | None -> ())
+
+ method load_sequents metasenv =
+ let sequents_no = List.length metasenv in
+ _metasenv <- metasenv;
+ pages <- sequents_no;
+ let win metano =
+ let w =
+ GBin.scrolled_window ~hpolicy:`AUTOMATIC ~vpolicy:`AUTOMATIC
+ ~shadow_type:`IN ~show:true ()
+ in
+ let reparent () =
+ match sequent_viewer#misc#parent with
+ | None -> w#add sequent_viewer#coerce
+ | Some _ -> sequent_viewer#misc#reparent w#coerce
+ in
+ goal2win <- (metano, reparent) :: goal2win;
+ w#coerce
+ in
+ let page = ref 0 in
+ List.iter
+ (fun (metano, _, _) ->
+ page2goal <- (!page, metano) :: page2goal;
+ goal2page <- (metano, !page) :: goal2page;
+ incr page;
+ notebook#append_page ~tab_label:(tab_label metano) (win metano))
+ metasenv;
+ switch_page_callback <-
+ Some (notebook#connect#switch_page ~callback:(fun page ->
+ let goal =
+ try
+ List.assoc page page2goal
+ with Not_found -> assert false
+ in
+ set_goal goal;
+ self#render_page ~page ~goal))
+
+ method private render_page ~page ~goal =
+ sequent_viewer#load_sequent _metasenv goal;
+ try
+ List.assoc goal goal2win ();
+ sequent_viewer#set_selection None
+ with Not_found -> assert false
+
+ method goto_sequent goal =
+ let page =
+ try
+ List.assoc goal goal2page
+ with Not_found -> assert false
+ in
+ notebook#goto_page page;
+ self#render_page page goal;
+