X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGtkMisc.ml;h=2022704309e77c21f732386a67606c5b0b0b3247;hb=f34f2623a3133e235331d0c0c1830ec213dd09f1;hp=23b427c5a1c0637477daebcfffff7459fc946e17;hpb=f03ff6e69b44a4e89b92b21251cce9d247c4a4e4;p=helm.git

diff --git a/matita/matita/matitaGtkMisc.ml b/matita/matita/matitaGtkMisc.ml
index 23b427c5a..202270430 100644
--- a/matita/matita/matitaGtkMisc.ml
+++ b/matita/matita/matitaGtkMisc.ml
@@ -78,13 +78,6 @@ let toggle_win ?(check: GMenu.check_menu_item option) (win: GWindow.window) () =
 let toggle_callback ~callback ~(check: GMenu.check_menu_item) =
   ignore (check#connect#toggled (fun _ -> callback check#active))
   
-let add_key_binding key callback (evbox: GBin.event_box) =
-  ignore (evbox#event#connect#key_press (function
-    | key' when GdkEvent.Key.keyval key' = key ->
-        callback ();
-        false
-    | _ -> false))
-
 class multiStringListModel ~cols (tree_view: GTree.view) =
   let column_list = new GTree.column_list in
   let text_columns = 
@@ -261,16 +254,16 @@ class type gui =
 let popup_message 
   ~title ~message ~buttons ~callback
   ?(message_type=`QUESTION) ?parent ?(use_markup=true)
-  ?(destroy_with_parent=true) ?(allow_grow=false) ?(allow_shrink=false)
-  ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint
-  ?(position=`CENTER_ON_PARENT) ?wm_name ?wm_class ?border_width ?width 
+  ?(destroy_with_parent=true) ?icon ?(modal=true) ?(resizable=false)
+  ?screen ?type_hint
+  ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width 
   ?height ?(show=true) ()
 =
   let m = 
     GWindow.message_dialog 
       ~message ~use_markup ~message_type ~buttons ?parent ~destroy_with_parent 
-      ~title ~allow_grow ~allow_shrink ?icon ~modal ~resizable ?screen 
-      ?type_hint ~position ?wm_name ?wm_class ?border_width ?width ?height 
+      ~title ?icon ~modal ~resizable ?screen 
+      ?type_hint ~position ?wmclass ?border_width ?width ?height 
       ~show () 
   in 
   ignore(m#connect#response 
@@ -282,17 +275,17 @@ let popup_message
 
 let popup_message_lowlevel
   ~title ~message ?(no_separator=true) ~callback ~message_type ~buttons
-  ?parent  ?(destroy_with_parent=true) ?(allow_grow=false) ?(allow_shrink=false)
+  ?parent  ?(destroy_with_parent=true)
   ?icon ?(modal=true) ?(resizable=false) ?screen ?type_hint
-  ?(position=`CENTER_ON_PARENT) ?wm_name ?wm_class ?border_width ?width 
+  ?(position=`CENTER_ON_PARENT) ?wmclass ?border_width ?width 
   ?height ?(show=true) ()
 =
   let m = 
     GWindow.dialog 
       ~no_separator 
       ?parent ~destroy_with_parent 
-      ~title ~allow_grow ~allow_shrink ?icon ~modal ~resizable ?screen 
-      ?type_hint ~position ?wm_name ?wm_class ?border_width ?width ?height 
+      ~title ?icon ~modal ~resizable ?screen 
+      ?type_hint ~position ?wmclass ?border_width ?width ?height 
       ~show:false () 
   in
   let stock = 
@@ -422,7 +415,7 @@ let escape_pango_markup text =
 
 let matita_lang =
  let source_language_manager =
-  GSourceView2.source_language_manager ~default:true in
+  GSourceView3.source_language_manager ~default:true in
  source_language_manager#set_search_path
   (BuildTimeConf.runtime_base_dir ::
     source_language_manager#search_path);