added cast rendering (used in check window by gTopLevel/matita)

[helm.git] / helm / gTopLevel / termViewer.ml

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 841c61edfb184dd2811a065af11401b1dbbc9c7a..8a7bb0901d09c511edf17b34430bb3a87bab404c 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -127,10 +127,8 @@ class sequent_viewer ~(mml_of_cic_sequent:mml_of_cic_sequent) obj =
    let sequent_mml,(ids_to_terms,ids_to_father_ids,ids_to_hypotheses) =
      mml_of_cic_sequent metasenv sequent
    in
-    self#load_doc ~dom:sequent_mml ;
-(*
-Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
-*)
+    self#load_root ~root:sequent_mml#get_documentElement ;
+ignore (Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml ());
      current_infos <-
       Some (ids_to_terms,ids_to_father_ids,ids_to_hypotheses)
  end
@@ -139,12 +137,12 @@ Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
 let sequent_viewer ~(mml_of_cic_sequent: mml_of_cic_sequent)
   ?hadjustment ?vadjustment ?font_size ?log_verbosity
 =
-  GtkBase.Container.make_params ~cont:(
+  GtkBase.Widget.size_params ~cont:(
   OgtkMathViewProps.pack_return
     (fun p ->
       OgtkMathViewProps.set_params
         (new sequent_viewer ~mml_of_cic_sequent
-          (GtkMathViewProps.MathView.create p))
+          (GtkMathViewProps.MathView_GMetaDOM.create p))
         ~font_size ~log_verbosity)) []
 ;;
 
@@ -238,10 +236,11 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
        (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses);
     (* self#load_doc ~dom:mml ;
        current_mml <- Some mml ; *)
+    ignore(Misc.domImpl#saveDocumentToFile ~name:"/tmp/prova" ~doc:mml ());
     (match current_mml with
       None ->
         let time1 = Sys.time () in
-        self#load_doc ~dom:mml ;
+        self#load_root ~root:mml#get_documentElement ;
         let time2 = Sys.time () in
         debug_print ("Loading and displaying the proof took " ^
           string_of_float (time2 -. time1) ^ "seconds") ;
@@ -265,12 +264,12 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
 let proof_viewer ~(mml_of_cic_object: mml_of_cic_object)
   ?hadjustment ?vadjustment ?font_size ?log_verbosity
 =
-  GtkBase.Container.make_params ~cont:(
+  GtkBase.Widget.size_params ~cont:(
   OgtkMathViewProps.pack_return
     (fun p ->
       OgtkMathViewProps.set_params
         (new proof_viewer ~mml_of_cic_object
-          (GtkMathViewProps.MathView.create p))
+          (GtkMathViewProps.MathView_GMetaDOM.create p))
         ~font_size ~log_verbosity)) []
 ;;