Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg

7 files changed, 174 insertions, 213 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 8b1fa0a3..07f0ece8 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -191,11 +191,29 @@ let coqtop_zombies () =
 
     Note: we use Unix.stderr in Unix.create_process to get debug
     messages from the coqtop's Ide_slave loop.
+
+    NB: it's important to close coqide's descriptors (ide2top_w and top2ide_r)
+    in coqtop. We do this indirectly via [Unix.set_close_on_exec].
+    This way, coqide has the only remaining copies of these descriptors,
+    and closing them later will have visible effects in coqtop. Cf man 7 pipe :
+
+    - If  all file descriptors referring to the write end of a pipe have been
+      closed, then an attempt to read(2) from the pipe will see end-of-file
+      (read(2) will return 0).
+    - If all file descriptors referring to the read end of a pipe have been
+      closed, then a write(2) will cause a SIGPIPE signal to be generated for
+      the calling process. If the calling process is ignoring this signal,
+      then write(2) fails with the error EPIPE.
+
+    Symmetrically, coqtop's descriptors (ide2top_r and top2ide_w) should be
+    closed in coqide.
 *)
 
 let open_process_pid prog args =
   let (ide2top_r,ide2top_w) = Unix.pipe () in
   let (top2ide_r,top2ide_w) = Unix.pipe () in
+  Unix.set_close_on_exec ide2top_w;
+  Unix.set_close_on_exec top2ide_r;
   let pid = Unix.create_process prog args ide2top_r top2ide_w Unix.stderr in
   assert (pid <> 0);
   Unix.close ide2top_r;
@@ -250,7 +268,7 @@ let eval_call coqtop (c:'a Ide_intf.call) =
   Xml_utils.print_xml coqtop.cin (Ide_intf.of_call c);
   flush coqtop.cin;
   let xml = Xml_parser.parse p (Xml_parser.SChannel coqtop.cout) in
-  (Ide_intf.to_answer xml : 'a Interface.value)
+  (Ide_intf.to_answer xml c : 'a Interface.value)
 
 let interp coqtop ?(raw=false) ?(verbose=true) s =
   eval_call coqtop (Ide_intf.interp (raw,verbose,s))
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 1bd490ab..07de4daf 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -41,14 +41,9 @@ object
   val mutable read_only : bool
   val mutable filename : string option
   val mutable stats : Unix.stats option
-  val mutable detached_views : GWindow.window list
   method without_auto_complete : 'a 'b. ('a -> 'b) -> 'a -> 'b
   method set_auto_complete : bool -> unit
 
-  method kill_detached_views : unit -> unit
-  method add_detached_view : GWindow.window -> unit
-  method remove_detached_view : GWindow.window -> unit
-
   method filename : string option
   method stats :  Unix.stats option
   method update_stats : unit
@@ -104,7 +99,10 @@ type viewable_script =
     }
 
 let kill_session s =
-  s.analyzed_view#kill_detached_views ();
+  (* To close the detached views of this script, we call manually
+     [destroy] on it, triggering some callbacks in [detach_view].
+     In a more modern lablgtk, rather use the page-removed signal ? *)
+  s.script#destroy ();
   Coq.kill_coqtop !(s.toplvl)
 
 let build_session s =
@@ -442,6 +440,7 @@ let remove_tags (buffer:GText.buffer) from upto =
       Tags.Script.proof_decl; Tags.Script.qed ]
 
 (** Cut a part of the buffer in sentences and tag them.
+    Invariant: either this slice ends the buffer, or it ends with ".".
     May raise [Coq_lex.Unterminated] when the zone ends with
     an unterminated sentence. *)
 
@@ -480,14 +479,18 @@ let is_char s c = s#char = Char.code c
 
 (** Search backward the first character of a sentence, starting at [iter]
     and going at most up to [soi] (meant to be the end of the locked zone).
-    Raise [Not_found] when no proper sentence start has been found,
-    in particular when the final "." of the locked zone is followed
-    by a non-blank character outside the locked zone. This non-blank
-    character will be signaled as erroneous in [tag_on_insert] below. *)
+    Raise [StartError] when no proper sentence start has been found.
+    A character following a ending "." is considered as a sentence start
+    only if this character is a blank. In particular, when a final "."
+    at the end of the locked zone isn't followed by a blank, then this
+    non-blank character will be signaled as erroneous in [tag_on_insert] below.
+*)
+
+exception StartError
 
 let grab_sentence_start (iter:GText.iter) soi =
   let cond iter =
-    if iter#compare soi < 0 then raise Not_found;
+    if iter#compare soi < 0 then raise StartError;
     let prev = iter#backward_char in
     is_sentence_end prev &&
       (not (is_char prev '.') ||
@@ -509,42 +512,35 @@ let rec grab_ending_dot (start:GText.iter) =
 
 (** Retag a zone that has been edited *)
 
-let tag_on_insert =
-  (* possible race condition here : editing two buffers with a timedelta smaller
-   * than 1.5s might break the error recovery mechanism. *)
-  let skip_last = ref (ref true) in (* ref to the mutable flag created on last call *)
-  fun buffer ->
-    try
-      (* the start of the non-locked zone *)
-      let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
-      (* the inserted zone is between [prev_insert] and [insert] *)
-      let insert = buffer#get_iter_at_mark `INSERT in
-      let prev_insert = buffer#get_iter_at_mark (`NAME "prev_insert") in
-      (* [prev_insert] is normally always before [insert] even when deleting.
-	 Let's check this nonetheless *)
-      let prev_insert =
-	if insert#compare prev_insert < 0 then insert else prev_insert
-      in
-      let start = grab_sentence_start prev_insert soi in
-      (** The status of "{" "}" as sentence delimiters is too fragile.
-	  We retag up to the next "." instead. *)
-      let stop = grab_ending_dot insert in
-      let skip_curr = ref true in (* shall the callback be skipped ? by default yes*)
-      (!skip_last) := true; (* skip the previously created callback *)
-      skip_last := skip_curr;
-      try split_slice_lax buffer start stop
-      with Coq_lex.Unterminated ->
-        skip_curr := false;
-	let callback () =
-	  if not !skip_curr then begin
-	    try split_slice_lax buffer start buffer#end_iter
-	    with Coq_lex.Unterminated -> ()
-	  end; false
-	in
-	ignore (Glib.Timeout.add ~ms:1500 ~callback)
-    with Not_found ->
-      let err_pos = buffer#get_iter_at_mark (`NAME "start_of_input") in
-      buffer#apply_tag Tags.Script.error ~start:err_pos ~stop:err_pos#forward_char
+let tag_on_insert buffer =
+  (* the start of the non-locked zone *)
+  let soi = buffer#get_iter_at_mark (`NAME "start_of_input") in
+  (* the inserted zone is between [prev_insert] and [insert] *)
+  let insert = buffer#get_iter_at_mark `INSERT in
+  let prev = buffer#get_iter_at_mark (`NAME "prev_insert") in
+  (* [prev] is normally always before [insert] even when deleting.
+     Let's check this nonetheless *)
+  let prev, insert =
+    if insert#compare prev < 0 then insert, prev else prev, insert
+  in
+  try
+    let start = grab_sentence_start prev soi in
+    (** The status of "{" "}" as sentence delimiters is too fragile.
+	We retag up to the next "." instead. *)
+    let stop = grab_ending_dot insert in
+    try split_slice_lax buffer start stop
+    with Coq_lex.Unterminated ->
+      (* This shouldn't happen frequently. Either:
+         - we are at eof, with indeed an unfinished sentence.
+         - we have just inserted an opening of comment or string.
+         - the inserted text ends with a "." that interacts with the "."
+         found by [grab_ending_dot] to form a non-ending "..".
+         In any case, we retag up to eof, since this isn't that costly. *)
+      if not stop#is_end then
+        try split_slice_lax buffer start buffer#end_iter
+        with Coq_lex.Unterminated -> ()
+  with StartError ->
+    buffer#apply_tag Tags.Script.error ~start:soi ~stop:soi#forward_char
 
 let force_retag buffer =
   try split_slice_lax buffer buffer#start_iter buffer#end_iter
@@ -591,7 +587,6 @@ object(self)
   val mutable stats = None
   val mutable last_modification_time = 0.
   val mutable last_auto_save_time = 0.
-  val mutable detached_views = []
   val mutable find_forward_instead_of_backward = false
 
   val mutable auto_complete_on = !current.auto_complete
@@ -606,14 +601,6 @@ object(self)
     let y = f x in
     self#set_auto_complete old;
     y
-  method add_detached_view (w:GWindow.window) =
-    detached_views <- w::detached_views
-  method remove_detached_view (w:GWindow.window) =
-    detached_views <- List.filter (fun e -> w#misc#get_oid<>e#misc#get_oid) detached_views
-
-  method kill_detached_views () =
-    List.iter (fun w -> w#destroy ()) detached_views;
-    detached_views <- []
 
   method filename = filename
   method stats = stats
@@ -820,7 +807,7 @@ object(self)
     begin
       let menu_callback = if !current.contextual_menus_on_goal then
           (fun s () -> ignore (self#insert_this_phrase_on_success
-                                 true true false ("progress "^s) s))
+				 true true false ("progress "^s) s))
         else
           (fun _ _ -> ()) in
       try
@@ -1007,6 +994,7 @@ object(self)
       if stop#starts_line then
         input_buffer#insert ~iter:stop insertphrase
       else input_buffer#insert ~iter:stop ("\n"^insertphrase);
+      tag_on_insert input_buffer;
       let start = self#get_start_of_input in
       input_buffer#move_mark ~where:stop (`NAME "start_of_input");
       input_buffer#apply_tag (safety_tag safe) ~start ~stop;
@@ -1231,7 +1219,7 @@ object(self)
       (List.exists
          (fun p ->
            self#insert_this_phrase_on_success true false false
-             ("progress "^p^".\n") (p^".\n")) l)
+             ("progress "^p^".") (p^".")) l)
 
   method active_keypress_handler k =
     let state = GdkEvent.Key.state k in
@@ -1382,23 +1370,15 @@ object(self)
     );
     ignore (input_buffer#connect#begin_user_action
 	      ~callback:(fun () ->
-		           let here = input_buffer#get_iter_at_mark `INSERT in
-			   input_buffer#move_mark (`NAME "prev_insert") here
-	      )
+                let where = self#get_insert in
+                input_buffer#move_mark (`NAME "prev_insert") ~where;
+                let start = self#get_start_of_input in
+                let stop = input_buffer#end_iter in
+                input_buffer#remove_tag Tags.Script.error ~start ~stop)
     );
     ignore (input_buffer#connect#end_user_action
               ~callback:(fun () ->
                 last_modification_time <- Unix.time ();
-                let r = input_view#visible_rect in
-                let stop =
-                  input_view#get_iter_at_location
-                    ~x:(Gdk.Rectangle.x r + Gdk.Rectangle.width r)
-                    ~y:(Gdk.Rectangle.y r + Gdk.Rectangle.height r)
-                in
-                input_buffer#remove_tag
-                  Tags.Script.error
-                  ~start:self#get_start_of_input
-                  ~stop;
                 tag_on_insert input_buffer
               )
     );
@@ -1795,6 +1775,8 @@ let forbid_quit_to_save () =
 	end
 	else false)
 
+let logfile = ref None
+
 let main files =
 
   (* Main window *)
@@ -2354,7 +2336,7 @@ let main files =
   let tactic_shortcut s sc = GAction.add_action s ~label:("_"^s)
     ~accel:(!current.modifier_for_tactics^sc)
     ~callback:(do_if_active (fun a -> a#insert_command
-			       ("progress "^s^".\n") (s^".\n"))) in
+			       ("progress "^s^".") (s^"."))) in
   let query_callback command _ =
     let word = get_current_word () in
     if not (word = "") then
@@ -2381,6 +2363,24 @@ let main files =
 	|Some ac -> GAction.add_action name ~label ~callback ~accel:(!current.modifier_for_templates^ac)
 	|None -> GAction.add_action name ~label ~callback ?accel:None
   in
+  let detach_view _ =
+    (* Open a separate window containing the current buffer *)
+    let trm = session_notebook#current_term in
+    let w = GWindow.window ~show:true
+      ~width:(!current.window_width*2/3)
+      ~height:(!current.window_height*2/3)
+      ~position:`CENTER
+      ~title:(if trm.filename = "" then "*scratch*" else trm.filename)
+      ()
+    in
+    let sb = GBin.scrolled_window ~packing:w#add ()
+    in
+    let nv = GText.view ~buffer:trm.script#buffer ~packing:sb#add ()
+    in
+    nv#misc#modify_font !current.text_font;
+    (* If the buffer in the main window is closed, destroy this detached view *)
+    ignore (trm.script#connect#destroy ~callback:w#destroy)
+  in
     GAction.add_actions file_actions [
       GAction.add_action "File" ~label:"_File";
       GAction.add_action "New" ~callback:new_f ~stock:`NEW;
@@ -2568,33 +2568,7 @@ let main files =
     ];
     GAction.add_actions windows_actions [
       GAction.add_action "Windows" ~label:"_Windows";
-      GAction.add_action "Detach View" ~label:"Detach _View"
-	~callback:(fun _ -> do_if_not_computing "detach view"
-		     (function {script=v;analyzed_view=av} ->
-			let w = GWindow.window ~show:true
-			  ~width:(!current.window_width*2/3)
-			  ~height:(!current.window_height*2/3)
-			  ~position:`CENTER
-			  ~title:(match av#filename with
-				    | None -> "*Unnamed*"
-				    | Some f -> f)
-			  ()
-			in
-			let sb = GBin.scrolled_window
-			  ~packing:w#add ()
-			in
-			let nv = GText.view
-			  ~buffer:v#buffer
-			  ~packing:sb#add
-			  ()
-			in
-			  nv#misc#modify_font
-			    !current.text_font;
-			  ignore (w#connect#destroy
-				    ~callback:
-				    (fun () -> av#remove_detached_view w));
-			  av#add_detached_view w)
-		     [session_notebook#current_term]);
+      GAction.add_action "Detach View" ~label:"Detach _View" ~callback:detach_view
     ];
     GAction.add_actions help_actions [
       GAction.add_action "Help" ~label:"_Help";
@@ -2846,12 +2820,17 @@ let main files =
      \n-------------------\
      \n"
   in
+  let display_log_file (b:GText.buffer) =
+    if !debug then
+      let file = match !logfile with None -> "stderr" | Some f -> f in
+      b#insert ("Debug mode is on, log file is "^file)
+  in
   let initial_about (b:GText.buffer) =
     let initial_string =
       "Welcome to CoqIDE, an Integrated Development Environment for Coq\n"
     in
     let coq_version = Coq.short_version () in
-    b#insert ~iter:b#start_iter "\n\n";
+    display_log_file b;
     if Glib.Utf8.validate ("You are running " ^ coq_version) then
       b#insert ~iter:b#start_iter ("You are running " ^ coq_version);
     if Glib.Utf8.validate initial_string then
@@ -2881,8 +2860,8 @@ let main files =
     then b#insert about_full_string;
     let coq_version = Coq.version () in
     if Glib.Utf8.validate coq_version
-    then b#insert coq_version
-
+    then b#insert coq_version;
+    display_log_file b;
   in
   (* Remove default pango menu for textviews *)
   w#show ();
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 18df1f6a..44de77f7 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -12,6 +12,9 @@
     no /bin/sh when using create_process instead of open_process. *)
 val sup_args : string list ref
 
+(** In debug mode under win32, messages are written to a log file *)
+val logfile : string option ref
+
 (** Filter the argv from coqide specific options, and set
     Minilib.coqtop_path accordingly *)
 val read_coqide_args : string list -> string list
diff --git a/ide/coqide_main.ml4 b/ide/coqide_main.ml4
index f5138311..ebcecc17 100644
--- a/ide/coqide_main.ml4
+++ b/ide/coqide_main.ml4
@@ -6,18 +6,37 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-IFDEF QUARTZ THEN
-external gtk_mac_init : (string -> unit) -> (unit -> bool) -> unit
-  = "caml_gtk_mac_init"
+let _ = Coqide.ignore_break ()
+let _ = GtkMain.Main.init ()
 
-external gtk_mac_ready :  ([> Gtk.widget ] as 'a) Gtk.obj -> ([> Gtk.widget ] as 'a) Gtk.obj ->
-                          ([> Gtk.widget ] as 'a) Gtk.obj -> unit
-  = "caml_gtk_mac_ready"
-END
+(* We handle Gtk warning messages ourselves :
+   - on win32, we don't want them to end on a non-existing console
+   - we display critical messages via pop-ups *)
 
-let initmac () = IFDEF QUARTZ THEN gtk_mac_init Coqide.do_load Coqide.forbid_quit_to_save ELSE () END
+let catch_gtk_messages () =
+  let all_levels =
+    [`FLAG_RECURSION;`FLAG_FATAL;`ERROR;`CRITICAL;`WARNING;
+     `MESSAGE;`INFO;`DEBUG]
+  in
+  let handler ~level msg =
+    let header = "Coqide internal error: " in
+    let level_is tag = (level land Glib.Message.log_level tag) <> 0 in
+    if level_is `ERROR then
+      let () = GToolbox.message_box ~title:"Error" (header ^ msg) in
+      Coqide.crash_save 1
+    else if level_is `CRITICAL then
+      GToolbox.message_box ~title:"Error" (header ^ msg)
+    else if level_is `DEBUG || Sys.os_type = "Win32" then
+      Ideutils.prerr_endline msg (* no-op unless in debug mode *)
+    else
+      Printf.eprintf "%s\n" msg
+  in
+  let catch domain =
+    ignore (Glib.Message.set_log_handler ~domain ~levels:all_levels handler)
+  in
+  List.iter catch ["GLib";"Gtk";"Gdk";"Pango"]
 
-let macready x y z = IFDEF QUARTZ THEN gtk_mac_ready x#as_widget y#as_widget z#as_widget ELSE ()  END
+let () = catch_gtk_messages ()
 
 (* On win32, we add the directory of coqide to the PATH at launch-time
    (this used to be done in a .bat script). *)
@@ -33,12 +52,18 @@ let set_win32_path () =
 *)
 
 let reroute_stdout_stderr () =
+  (* We anticipate a bit the argument parsing and look for -debug *)
+  let debug = List.mem "-debug" (Array.to_list Sys.argv) in
+  Ideutils.debug := debug;
   let out_descr =
-    if !Ideutils.debug then
-      Unix.descr_of_out_channel (snd (Filename.open_temp_file "coqide_" ".log"))
+    if debug then
+      let (name,chan) = Filename.open_temp_file "coqide_" ".log" in
+      Coqide.logfile := Some name;
+      Unix.descr_of_out_channel chan
     else
       snd (Unix.pipe ())
   in
+  Unix.set_close_on_exec out_descr;
   Unix.dup2 out_descr Unix.stdout;
   Unix.dup2 out_descr Unix.stderr
 
@@ -64,10 +89,17 @@ let () =
   reroute_stdout_stderr ()
 END
 
+IFDEF QUARTZ THEN
+  let osx = GosxApplication.osxapplication ()
+
+  let _ =
+    osx#connect#ns_application_open_file ~callback:(fun x -> Coqide.do_load x; true) in
+  let _ =
+    osx#connect#ns_application_block_termination ~callback:Coqide.forbid_quit_to_save in
+  ()
+END
+
 let () =
-  Coqide.ignore_break ();
-  ignore (GtkMain.Main.init ());
-  initmac () ;
   (try
      let gtkrcdir = List.find
        (fun x -> Sys.file_exists (Filename.concat x "coqide-gtk2rc"))
@@ -82,13 +114,6 @@ let () =
   end;
 (*    GtkData.AccelGroup.set_default_mod_mask
       (Some [`CONTROL;`SHIFT;`MOD1;`MOD3;`MOD4]);*)
-    ignore (
-	     Glib.Message.set_log_handler ~domain:"Gtk" ~levels:[`ERROR;`FLAG_FATAL;
-								 `WARNING;`CRITICAL]
-	       (fun ~level msg ->
-		  if level land Glib.Message.log_level `WARNING <> 0
-		  then Printf.eprintf "Warning: %s\n" msg
-		  else failwith ("Coqide internal error: " ^ msg)));
   let argl = Array.to_list Sys.argv in
   let argl = Coqide.read_coqide_args argl in
   let files = Coq.filter_coq_opts (List.tl argl) in
@@ -96,9 +121,18 @@ let () =
   Coq.check_connection args;
   Coqide.sup_args := args;
   Coqide.main files;
-    if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ());
-    macready (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar") (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")
-             (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help/Abt");
+    if !Coq_config.with_geoproof then ignore (Thread.create Coqide.check_for_geoproof_input ())
+
+IFDEF QUARTZ THEN
+  let () =
+    GtkosxApplication.Application.set_menu_bar osx#as_osxapplication (GtkMenu.MenuShell.cast (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar")#as_widget) in
+  let () =
+    GtkosxApplication.Application.insert_app_menu_item osx#as_osxapplication (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Edit/Prefs")#as_widget 1 in
+  let () =
+    GtkosxApplication.Application.set_help_menu osx#as_osxapplication (Some (GtkMenu.MenuItem.cast (Coqide_ui.ui_m#get_widget "/CoqIde MenuBar/Help")#as_widget)) in
+  osx#ready ()
+END
+
     while true do
       try
 	GtkThread.main ()
diff --git a/ide/ide_mac_stubs.c b/ide/ide_mac_stubs.c
deleted file mode 100644
index 2aeb2bf4..00000000
--- a/ide/ide_mac_stubs.c
+++ /dev/null
@@ -1,85 +0,0 @@
-#include <caml/mlvalues.h>
-#include <caml/alloc.h>
-#include <caml/memory.h>
-#include <caml/callback.h>
-#include <caml/fail.h>
-
-#include <gtk/gtk.h>
-#include <lablgtk2/wrappers.h>
-#include <lablgtk2/ml_glib.h>
-#include <lablgtk2/ml_gobject.h>
-#include <gtkmacintegration/gtkosxapplication.h>
-
-GtkOSXApplication *theApp;
-value open_file_fun, forbid_quit_fun, themenubar, pref_item, about_item;
-
-static void osx_accel_map_foreach_lcb(gpointer data,const gchar *accel_path,
-				      guint accel_key, GdkModifierType accel_mods,
-				      gboolean changed) {
-  if (accel_mods & GDK_CONTROL_MASK) {
-    accel_mods |= GDK_META_MASK;
-    accel_mods &= (accel_mods & GDK_MOD1_MASK) ? ~GDK_MOD1_MASK : ~GDK_CONTROL_MASK;
-    if (!gtk_accel_map_change_entry(accel_path,accel_key,accel_mods,FALSE)) {
-      g_print("could not change accelerator %s\n",accel_path);
-    }
-  }
-  if (accel_mods & GDK_MOD1_MASK) {
-    accel_mods &= ~ GDK_MOD1_MASK;
-    accel_mods |= GDK_CONTROL_MASK;
-    if (!gtk_accel_map_change_entry(accel_path,accel_key,accel_mods,FALSE)) {
-      g_print("could not change accelerator %s\n",accel_path);
-    }
-  }
-}
-
-static gboolean deal_with_open(GtkOSXApplication *app, gchar *path, gpointer user_data)
-{
-  CAMLparam0();
-  CAMLlocal2(string_path, res);
-  string_path = caml_copy_string(path);
-  res = caml_callback_exn(open_file_fun,string_path);
-  gboolean truc = !(Is_exception_result(res));
-  CAMLreturnT(gboolean, truc);
-}
-
-static gboolean deal_with_quit(GtkOSXApplication *app, gpointer user_data)
-{
-  CAMLparam0();
-  CAMLlocal1(res);
-  res = caml_callback_exn(forbid_quit_fun,Val_unit);
-  gboolean truc = (Bool_val(res))||((Is_exception_result(res)));
-  CAMLreturnT(gboolean, truc);
-}
-
-CAMLprim value caml_gtk_mac_init(value open_file_the_fun, value forbid_quit_the_fun)
-{
-  CAMLparam2(open_file_the_fun,forbid_quit_the_fun);
-  open_file_fun = open_file_the_fun;
-  caml_register_generational_global_root(&open_file_fun);
-  forbid_quit_fun = forbid_quit_the_fun;
-  caml_register_generational_global_root(&forbid_quit_fun);
-  theApp = g_object_new(GTK_TYPE_OSX_APPLICATION, NULL);
-  g_signal_connect(theApp, "NSApplicationOpenFile", G_CALLBACK(deal_with_open), NULL);
-  g_signal_connect(theApp, "NSApplicationBlockTermination", G_CALLBACK(deal_with_quit), NULL);
-  CAMLreturn (Val_unit);
-}
-
-CAMLprim value caml_gtk_mac_ready(value menubar, value prefs, value about)
-{
-  GtkOSXApplicationMenuGroup * pref_grp, * about_grp;
-  CAMLparam3(menubar,prefs,about);
-  themenubar = menubar;
-  pref_item = prefs;
-  about_item = about;
-  caml_register_generational_global_root(&themenubar);
-  caml_register_generational_global_root(&pref_item);
-  caml_register_generational_global_root(&about_item);
-  /*  gtk_accel_map_foreach(NULL, osx_accel_map_foreach_lcb);*/
-  gtk_osxapplication_set_menu_bar(theApp,check_cast(GTK_MENU_SHELL,themenubar));
-  gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,about_item),1);
-  gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),2);
-  gtk_osxapplication_insert_app_menu_item(theApp,check_cast(GTK_WIDGET,pref_item),3);
-  gtk_osxapplication_insert_app_menu_item(theApp,gtk_separator_menu_item_new(),4);
-  gtk_osxapplication_ready(theApp);
-  CAMLreturn(Val_unit);
-}
diff --git a/ide/preferences.ml b/ide/preferences.ml
index 17216b92..2fb5023f 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -35,6 +35,10 @@ let mod_to_str (m:Gdk.Tags.modifier) =
     | `MOD5 -> "<Mod5>"
     | `CONTROL -> "<Control>"
     | `SHIFT -> "<Shift>"
+    | `HYPER -> "<Hyper>"
+    | `META -> "<Meta>"
+    | `RELEASE -> ""
+    | `SUPER -> "<Super>"
     |  `BUTTON1| `BUTTON2| `BUTTON3| `BUTTON4| `BUTTON5| `LOCK -> ""
 
 let mod_list_to_str l = List.fold_left (fun s m -> (mod_to_str m)^s) "" l
diff --git a/ide/utils/okey.ml b/ide/utils/okey.ml
index 57939266..905c3485 100644
--- a/ide/utils/okey.ml
+++ b/ide/utils/okey.ml
@@ -47,6 +47,10 @@ let int_of_modifier = function
   | `BUTTON3 -> 1024
   | `BUTTON4 -> 2048
   | `BUTTON5 -> 4096
+  | `HYPER -> 1 lsl 22
+  | `META -> 1 lsl 20
+  | `RELEASE -> 1 lsl 30
+  | `SUPER -> 1 lsl 21
 
 let print_modifier l =
   List.iter
@@ -65,7 +69,11 @@ let print_modifier l =
 	  | `BUTTON2 -> "B2"
 	  | `BUTTON3 -> "B3"
 	  | `BUTTON4 -> "B4"
-	  | `BUTTON5 -> "B5")
+	  | `BUTTON5 -> "B5"
+          | `HYPER -> "HYPER"                                                                                                     
+          | `META -> "META"                                                                                                       
+          | `RELEASE -> ""                                                                                                        
+          | `SUPER -> "SUPER")
 	    m)^" ")
     )
     l;