X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtexTermEditor.ml;h=1ea429926519bd688c3126e6374075efaf7c75ed;hb=ebc089606ccbb3e9dbde142542a1f98f5020b4dd;hp=b89974d7152ff94b2a8e7f8a0e4c32d43bfced7e;hpb=63f211d673ba5a9eb05b0bdad2585e2b251f2baa;p=helm.git diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index b89974d71..1ea429926 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -23,6 +23,9 @@ * http://cs.unibo.it/helm/. *) +let debug = true +let debug_print s = if debug then prerr_endline s + (******************************************************************************) (* *) (* PROJECT HELM *) @@ -63,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 = @@ -79,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 ; @@ -91,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 ; @@ -100,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 ; @@ -125,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 @@ -206,10 +216,14 @@ module Make(C:DisambiguateTypes.Callbacks) = | None -> None ) context in -prerr_endline ("###CSC: " ^ (Mathml_editor.get_tex tex_editor)) ; + debug_print ("TexTermEditor: Raw Tex: " ^ (Mathml_editor.get_tex tex_editor)) ; let environment',metasenv,expr = - Disambiguate'.disambiguate_term mqi_handle - context metasenv (Mathml_editor.get_tex tex_editor) !environment + match + Disambiguate'.disambiguate_term mqi_handle + context metasenv (Mathml_editor.get_tex tex_editor) !environment + with + [environment',metasenv,expr] -> environment',metasenv,expr + | _ -> assert false in environment := environment' ; metasenv,expr