+class sequents_viewer ~(notebook:GPack.notebook)
+ ~(sequent_viewer:MatitaTypes.sequent_viewer) ~set_goal ()
+=
+ 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 _metasenv = []
+
+ method reset =
+ for i = 1 to pages do notebook#remove_page 0 done;
+ pages <- 0;
+ page2goal <- [];
+ goal2page <- [];
+ _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;
+ debug_print (sprintf "sequents no: %d" sequents_no);
+ pages <- sequents_no;
+ let widget = sequent_viewer#coerce in
+ let page = ref 0 in
+ List.iter
+ (fun (metano, _, _) ->
+ page2goal <- (!page, metano) :: page2goal;
+ goal2page <- (metano, !page) :: goal2page;
+ incr page;
+ let tab_label =
+ (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
+ in
+ notebook#append_page ~tab_label widget)
+ metasenv;
+ switch_page_callback <-
+ (* TODO Zack the "#after" may probably be removed after Luca's fix for
+ * widget not loading documents before being realized *)
+ Some (notebook#connect#after#switch_page ~callback:(fun page ->
+ debug_print "switch_page callback";
+ let goal =
+ try
+ List.assoc page page2goal
+ with Not_found -> assert false
+ in
+ set_goal goal;
+ self#render_page goal))
+
+ method private render_page goal =
+ sequent_viewer#load_sequent _metasenv goal
+
+ method goto_sequent goal =
+ let page =
+ try
+ List.assoc goal goal2page
+ with Not_found -> assert false
+ in
+ notebook#goto_page page;
+ self#render_page goal