| None -> self#set_selection None
end
+let clickable_math_view =
+ GtkBase.Widget.size_params
+ ~cont:(OgtkMathViewProps.pack_return (fun p ->
+ OgtkMathViewProps.set_params
+ (new clickable_math_view (GtkMathViewProps.MathView_GMetaDOM.create p))
+ ~font_size:None ~log_verbosity:None))
+ []
+let clickable_math_view () = clickable_math_view ()
+
class proof_viewer obj =
- object(self)
+ object (self)
inherit clickable_math_view obj
val mutable current_mathml = None
method load_proof ((uri_opt, _, _, _) as proof, (goal_opt: int option)) =
- let (annobj, ids_to_terms, ids_to_father_ids, ids_to_inner_sorts,
- ids_to_inner_types, ids_to_conjectures, ids_to_hypotheses) =
- Cic2acic.acic_object_of_cic_object (cicCurrentProof proof)
+ let uri = unopt_uri uri_opt in
+ let obj = cicCurrentProof proof in
+ let (mathml, (ids_to_terms, ids_to_father_ids, ids_to_conjectures,
+ ids_to_hypotheses)) =
+ ApplyTransformation.mml_of_cic_object uri obj
in
current_infos <- Some (ids_to_terms, ids_to_father_ids,
ids_to_conjectures, ids_to_hypotheses);
- let mathml =
- ApplyTransformation.mml_of_cic_object ~explode_all:true
- (unopt_uri uri_opt) annobj ids_to_inner_sorts ids_to_inner_types
- in
debug_print "load_proof: dumping MathML to ./proof";
ignore (Misc.domImpl#saveDocumentToFile ~name:"./proof" ~doc:mathml ());
match current_mathml with
~font_size ~log_verbosity))
[]
+class cicBrowser =
+ object (self)
+ val widget =
+ let gui = MatitaGui.instance () in
+ sequent_viewer ~show:true ~packing:gui#browser#scrolledBrowser#add ()
+
+ initializer
+ widget#set_href_callback (Some (fun uri -> self#load_uri uri))
+
+ method load_uri uri = ()
+ end
+
let proof_viewer ?hadjustment ?vadjustment ?font_size ?log_verbosity =
GtkBase.Widget.size_params
~cont:(OgtkMathViewProps.pack_return (fun p ->
) in
fun () -> Lazy.force instance
-let sequents_viewer ~(notebook:GPack.notebook)
- ~(sequent_viewer:sequent_viewer) ~set_goal ()
-=
- new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
-
class mathViewer =
let href_callback: (UriManager.uri -> unit) option ref = ref None in
object
method unload () = (proof_viewer_instance ())#unload
end
+let sequents_viewer ~(notebook:GPack.notebook)
+ ~(sequent_viewer:sequent_viewer) ~set_goal ()
+=
+ new sequents_viewer ~notebook ~sequent_viewer ~set_goal ()
+
let mathViewer () = new mathViewer
+let cicBrowser () = new cicBrowser
+