summaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq.ml20
-rw-r--r--ide/coqide.ml183
-rw-r--r--ide/coqide.mli3
-rw-r--r--ide/coqide_main.ml482
-rw-r--r--ide/ide_mac_stubs.c85
-rw-r--r--ide/preferences.ml4
-rw-r--r--ide/utils/okey.ml10
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;