diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 20 | ||||
| -rw-r--r-- | ide/coqide.ml | 183 | ||||
| -rw-r--r-- | ide/coqide.mli | 3 | ||||
| -rw-r--r-- | ide/coqide_main.ml4 | 82 | ||||
| -rw-r--r-- | ide/ide_mac_stubs.c | 85 | ||||
| -rw-r--r-- | ide/preferences.ml | 4 | ||||
| -rw-r--r-- | ide/utils/okey.ml | 10 |
7 files changed, 174 insertions, 213 deletions
@@ -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; |