ported to latest lablgtkmathview

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index eeb6053aa2615b86a75efc5723d7193894896f3b..197b6f1ee305b6db4d121934f19f228bd8d57795 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -892,7 +892,7 @@ let
       in
        window#set_title (UriManager.string_of_uri uri) ;
        window#misc#hide () ; window#show () ;
-       mmlwidget#load_doc mml ;
+       mmlwidget#load_root mml#get_documentElement ;
     with
      e ->
       HelmLogger.log
@@ -902,7 +902,7 @@ let
    let obj = CicEnvironment.get_obj uri in
     show_in_show_window_obj uri obj
   in
-   let show_in_show_window_callback mmlwidget (n : Gdome.element option) _ =
+   let show_in_show_window_callback mmlwidget ((n : Gdome.element option),_,_,_) =
     match n with
        None -> ()
      | Some n' ->

diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml
index 841c61edfb184dd2811a065af11401b1dbbc9c7a..913cc95292023719004c229025e7692551b00283 100644 (file)
--- a/helm/gTopLevel/termViewer.ml
+++ b/helm/gTopLevel/termViewer.ml
@@ -127,7 +127,7 @@ 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 ;
+    self#load_root ~root:sequent_mml#get_documentElement ;
 (*
 Misc.domImpl#saveDocumentToFile ~name:"/tmp/pippo" ~doc:sequent_mml () ;
 *)
@@ -139,12 +139,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)) []
 ;;
 
@@ -241,7 +241,7 @@ class proof_viewer ~(mml_of_cic_object:mml_of_cic_object) obj =
     (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 +265,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)) []
 ;;
 

diff --git a/helm/gTopLevel/termViewer.mli b/helm/gTopLevel/termViewer.mli
index 8fa37e53193f2e19ed4f56cf10c696bc106a8159..71ab63bc0e0ca9c861bc84d16b037115957fafb5 100644 (file)
--- a/helm/gTopLevel/termViewer.mli
+++ b/helm/gTopLevel/termViewer.mli
@@ -73,7 +73,6 @@ val sequent_viewer :
   ?vadjustment:GData.adjustment ->
   ?font_size:int ->
   ?log_verbosity:int ->
-  ?border_width:int ->
   ?width:int ->
   ?height:int ->
   ?packing:(GObj.widget -> unit) ->
@@ -111,7 +110,6 @@ val proof_viewer :
   ?vadjustment:GData.adjustment ->
   ?font_size:int ->
   ?log_verbosity:int ->
-  ?border_width:int ->
   ?width:int ->
   ?height:int ->
   ?packing:(GObj.widget -> unit) ->

diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml
index e06950508c72ec5570e6667b33fb1fe9def8df97..1ea429926519bd688c3126e6374075efaf7c75ed 100644 (file)
--- a/helm/gTopLevel/texTermEditor.ml
+++ b/helm/gTopLevel/texTermEditor.ml
@@ -66,9 +66,11 @@ module Make(C:DisambiguateTypes.Callbacks) =
     let mmlwidget =
      GMathViewAux.single_selection_math_view
       ?packing ?width ?height () in
+(*
     let drawing_area = mmlwidget#get_drawing_area in
     let _ = drawing_area#misc#set_can_focus true in
     let _ = drawing_area#misc#grab_focus () in
+*)
     let logger =
      fun l s -> prerr_endline ("TERM_EDITOR (" ^ string_of_int l ^ "): " ^ s) in
     let tex_editor =
@@ -82,11 +84,14 @@ module Make(C:DisambiguateTypes.Callbacks) =
       ~tml_uri:"/usr/share/editex/tml-litex.xsl"
       ~log:logger
     in
+(*
     let _ =
      (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#button_press
       ~callback:(fun _ -> drawing_area#misc#grab_focus () ; true) in
+*)
     let _ =
-     (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_in
+(*      (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_in *)
+     (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#focus_in
        ~callback:
          (fun _ ->
            mmlwidget#freeze ;
@@ -94,7 +99,8 @@ module Make(C:DisambiguateTypes.Callbacks) =
            mmlwidget#thaw ;
            true) in
     let _ =
-     (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out
+(*      (new GObj.event_ops drawing_area#coerce#as_widget)#connect#focus_out *)
+     (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#focus_out
        ~callback:
          (fun _ ->
            mmlwidget#freeze ;
@@ -103,9 +109,10 @@ module Make(C:DisambiguateTypes.Callbacks) =
            true) in
     let _ = Mathml_editor.push tex_editor '$' in
     let dom_tree = Mathml_editor.get_mml tex_editor in
-    let _ = mmlwidget#load_doc dom_tree in
+    let _ = mmlwidget#load_root dom_tree#get_documentElement in
     let _ = 
-     drawing_area#event#connect#key_press
+(*      drawing_area#event#connect#key_press *)
+     (new GObj.event_ops mmlwidget#coerce#as_widget)#connect#key_press
       (function e ->
         let key = GdkEvent.Key.keyval e in
          mmlwidget#freeze ;
@@ -128,9 +135,9 @@ module Make(C:DisambiguateTypes.Callbacks) =
            (List.mem `CONTROL (GdkEvent.Key.state e))
          else if key = GdkKeysyms._v then
            ignore (mmlwidget#misc#convert_selection "STRING" Gdk.Atom.primary);
-         let adj = mmlwidget#get_hadjustment in
+         let hadj, _ = mmlwidget#get_adjustments in
           mmlwidget#thaw ;
-          adj#set_value adj#upper ;
+          hadj#set_value hadj#upper ;
           false) in
     let environment =
      match share_environment_with with