Mathml_editor.drop tex_editor
(List.mem `CONTROL (GdkEvent.Key.state e))
else if key = GdkKeysyms._v then
- ignore (mmlwidget#misc#convert_selection "STRING" `PRIMARY);
+ ignore (mmlwidget#misc#convert_selection "STRING" Gdk.Atom.primary);
let adj = mmlwidget#get_hadjustment in
mmlwidget#thaw ;
adj#set_value adj#upper ;