(* *)
(***************************************************************************)
+open Printf
+
open MatitaTypes
(* List utility functions *)
| None -> assert false (* "ERROR: No current term!!!" *)
) selections
- method load_sequent (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata)
- sequent_no
+ method load_sequent (mml:Gdome.document)
+ (metadata:MatitaTypes.sequents_metadata) sequent_no
=
let (annconjecture, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_hypotheses)
=
try
- List.assoc sequent_no (snd metadata)
+ List.assoc sequent_no metadata
with Not_found -> assert false
in
current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
val mutable current_infos = None
val mutable current_mml = None
- method load_proof (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) =
+ method load_proof (mml:Gdome.document) (metadata:MatitaTypes.proof_metadata) =
let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- (fst metadata)
+ metadata
in
current_infos <-
Some
self#thaw
end
+class sequents_viewer ~(notebook:GPack.notebook)
+ ~(sequent_viewer:MatitaTypes.sequent_viewer) ()
+=
+ object (self)
+ val mutable pages = 0
+ val mutable switch_page_callback = None
+ val mutable mathmls = []
+ val mutable metadata = None
+ val mutable page2goal = [] (* associative list: page no -> goal no *)
+ val mutable goal2page = [] (* the other way round *)
+
+ method reset =
+ for i = 1 to pages do notebook#remove_page 0 done;
+ pages <- 0;
+ mathmls <- [];
+ metadata <- None;
+ page2goal <- [];
+ goal2page <- [];
+ (match switch_page_callback with
+ | Some id ->
+ GtkSignal.disconnect notebook#as_widget id;
+ switch_page_callback <- None
+ | None -> ())
+
+ method load_sequents (metadata': MatitaTypes.sequents_metadata) =
+ metadata <- Some metadata';
+ let sequents = metadata' in
+ let sequents_no = List.length sequents in
+ 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, (asequent, _, _, ids_to_inner_sorts, _)) ->
+ page2goal <- (!page, metano) :: page2goal;
+ goal2page <- (metano, !page) :: goal2page;
+ let tab_label =
+ (GMisc.label ~text:(sprintf "?%d" metano) ~show:true ())#coerce
+ in
+ notebook#append_page ~tab_label widget;
+ let mathml = lazy
+ (let content_sequent = Cic2content.map_sequent asequent in
+ let pres_sequent =
+ Sequent2pres.sequent2pres ~ids_to_inner_sorts content_sequent
+ in
+ let xmlpres = Box.document_of_box pres_sequent in
+ Xml2Gdome.document_of_xml Misc.domImpl xmlpres)
+ in
+ mathmls <- (metano, mathml) :: mathmls)
+ sequents;
+ mathmls <- List.rev mathmls;
+ 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";
+ self#render_page page))
+
+ 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
+
+ method private render_page page =
+ let metadata =
+ match metadata with Some metadata -> metadata | None -> assert false
+ in
+ let (metano, mathml) = List.nth mathmls page in
+ sequent_viewer#load_sequent (Lazy.force mathml) metadata metano
+
+ end
+
(** constructors *)
let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
~font_size ~log_verbosity))
[]
+let sequents_viewer ~(notebook:GPack.notebook)
+ ~(sequent_viewer:MatitaTypes.sequent_viewer) ()
+=
+ new sequents_viewer ~notebook ~sequent_viewer ()
+