(* End of the list utility functions *)
-(*
class sequent_viewer obj =
object(self)
| None -> assert false (* "ERROR: No current term!!!" *)
) selections
- method load_sequent metasenv sequent =
- let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
- mml_of_cic_sequent metasenv sequent
- in
- self#load_root ~root:sequent_mml#get_documentElement ;
- current_infos <-
- Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
+ method load_sequent (mml:Gdome.document) (metadata:MatitaTypes.hist_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)
+ with Not_found -> assert false
+ in
+ current_infos <- Some (ids_to_terms, ids_to_father_ids, ids_to_hypotheses);
+ self#load_root ~root:mml#get_documentElement
end
-*)
class proof_viewer obj =
object(self)
method load_proof (mml:Gdome.document) (metadata:MatitaTypes.hist_metadata) =
let (acic, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- metadata
+ (fst metadata)
in
current_infos <-
Some
(** constructors *)
-(*
let sequent_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
GtkBase.Widget.size_params
~cont:(OgtkMathViewProps.pack_return (fun p ->
(new sequent_viewer (GtkMathViewProps.MathView_GMetaDOM.create p))
~font_size ~log_verbosity))
[]
-*)
let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
GtkBase.Widget.size_params