X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FtexTermEditor.ml;h=c89fe04b2da80a94b53d0d38f4b425b1e040b354;hb=970ba0021a992efe25ec374875dc127ff236cc74;hp=d97eb51c46addf97deff9a7d64141b724b421696;hpb=bac72fcaa876137ab7a5630e0c1badc2a627dce8;p=helm.git diff --git a/helm/gTopLevel/texTermEditor.ml b/helm/gTopLevel/texTermEditor.ml index d97eb51c4..c89fe04b2 100644 --- a/helm/gTopLevel/texTermEditor.ml +++ b/helm/gTopLevel/texTermEditor.ml @@ -123,9 +123,14 @@ module Make(C:Disambiguate.Callbacks) = mmlwidget#thaw end else if key = GdkKeysyms._BackSpace then - Mathml_editor.drop tex_editor false ; - mmlwidget#thaw ; - false) in + Mathml_editor.drop tex_editor + (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 + mmlwidget#thaw ; + adj#set_value adj#upper ; + false) in let id_to_uris = match share_id_to_uris_with with None -> ref empty_id_to_uris @@ -153,6 +158,19 @@ module Make(C:Disambiguate.Callbacks) = ~useCapture:false in object(self) + + initializer + ignore (mmlwidget#misc#connect#selection_received + ~callback: (fun selection_data ~time -> + let input = try selection_data#data with Gpointer.Null -> "" in + mmlwidget#freeze ; + ignore (Mathml_editor.freeze tex_editor) ; + for i = 0 to String.length input - 1 do + Mathml_editor.push tex_editor input.[i] + done; + ignore (Mathml_editor.thaw tex_editor) ; + mmlwidget#thaw)) + method coerce = mmlwidget#coerce method reset = mmlwidget#freeze ;