From f36273550bc0538ea194cf0dee32ec608a6790f7 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 9 Sep 2004 16:00:40 +0000 Subject: [PATCH] ported to latest lablgtkmathview --- helm/gTopLevel/gTopLevel.ml | 4 ++-- helm/gTopLevel/termViewer.ml | 12 ++++++------ helm/gTopLevel/termViewer.mli | 2 -- helm/gTopLevel/texTermEditor.ml | 19 +++++++++++++------ 4 files changed, 21 insertions(+), 16 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index eeb6053aa..197b6f1ee 100644 --- 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 841c61edf..913cc9529 100644 --- 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 8fa37e531..71ab63bc0 100644 --- 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 e06950508..1ea429926 100644 --- 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 -- 2.39.2