From 29592216820248bfc78b137595fdd5e31d28f5b6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 26 Sep 2018 22:16:14 +0200 Subject: Indentation in configure.ml. --- configure.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/configure.ml b/configure.ml index cef4faaf1a..d7370b28c1 100644 --- a/configure.ml +++ b/configure.ml @@ -1200,8 +1200,8 @@ let write_macos_metadata exec = let () = close_out o in Unix.chmod f 0o444 -let () = if arch = "Darwin" then -List.iter write_macos_metadata distributed_exec +let () = + if arch = "Darwin" then List.iter write_macos_metadata distributed_exec let write_configpy f = safe_remove f; -- cgit v1.2.3 From 5b13384e1b5bd4f11f22036f4eb83c63a4ae88c2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 29 Oct 2018 15:48:47 +0100 Subject: Fixing #8269: adding callback on changed modifiers only after pref loading. Otherwise, probably for the reason suspected in [1], loading the preference file (coqiderc) is interpreted as a change of the modifiers, and this overrides what the more fine-grained preferences (coqide.keys) was telling. [1] https://github.com/coq/coq/issues/8269#issuecomment-415971367 --- ide/preferences.ml | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/ide/preferences.ml b/ide/preferences.ml index bf9fe8922a..ed51eb0b91 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -347,11 +347,15 @@ let modifier_for_display = let modifier_for_queries = new preference ~name:["modifier_for_queries"] ~init:"" ~repr:Repr.(string) -let _ = attach_modifiers modifier_for_navigation "/Navigation/" -let _ = attach_modifiers modifier_for_templates "/Templates/" -let _ = attach_modifiers modifier_for_tactics "/Tactics/" -let _ = attach_modifiers modifier_for_display "/View/" -let _ = attach_modifiers modifier_for_queries "/Queries/" +let attach_modifiers_callback () = + (* Tell to propagate changes done in preference menu to accel map *) + (* To be done after the preferences are loaded *) + let _ = attach_modifiers modifier_for_navigation "/Navigation/" in + let _ = attach_modifiers modifier_for_templates "/Templates/" in + let _ = attach_modifiers modifier_for_tactics "/Tactics/" in + let _ = attach_modifiers modifier_for_display "/View/" in + let _ = attach_modifiers modifier_for_queries "/Queries/" in + () let modifiers_valid = new preference ~name:["modifiers_valid"] ~init:"" ~repr:Repr.(string) @@ -665,6 +669,7 @@ let load_pref () = in Util.String.Map.iter iter m in (* Load file for bindings *) + attach_modifiers_callback () let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in () -- cgit v1.2.3 From 1503ab7737efb29bc17c22a242e9f66be50a0762 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 29 Oct 2018 16:03:44 +0100 Subject: Making a bit clearer that CoqIDE modifier menu is for global modifier change. Indeed, one can change each item locally, but the preference menu is only for changing the modifiers of a whole menu at once. --- ide/preferences.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/ide/preferences.ml b/ide/preferences.ml index ed51eb0b91..52122441a1 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -898,19 +898,19 @@ let configure ?(apply=(fun () -> ())) parent = in let project_file_name = pstring "Default name for project file" project_file_name in let modifier_for_tactics = - pmodifiers "Modifiers for Tactics Menu" modifier_for_tactics + pmodifiers "Global change of modifiers for Tactics Menu" modifier_for_tactics in let modifier_for_templates = - pmodifiers "Modifiers for Templates Menu" modifier_for_templates + pmodifiers "Global change of modifiers for Templates Menu" modifier_for_templates in let modifier_for_navigation = - pmodifiers "Modifiers for Navigation Menu" modifier_for_navigation + pmodifiers "Global change of modifiers for Navigation Menu" modifier_for_navigation in let modifier_for_display = - pmodifiers "Modifiers for View Menu" modifier_for_display + pmodifiers "Global change of modifiers for View Menu" modifier_for_display in let modifier_for_queries = - pmodifiers "Modifiers for Queries Menu" modifier_for_queries + pmodifiers "Global change of modifiers for Queries Menu" modifier_for_queries in let modifiers_valid = pmodifiers ~all:true "Allowed modifiers" modifiers_valid -- cgit v1.2.3 From 9ef674aff93396262966de8f9a583e1eae7889b9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 3 Nov 2018 15:41:30 +0100 Subject: CoqIDE: Letting flash notices being treated sequentially. --- ide/ideutils.ml | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 246254c6a5..4b156065f3 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -34,9 +34,38 @@ let push_info,pop_info,clear_info = (fun () -> decr size; status_context#pop ()), (fun () -> for _i = 1 to !size do status_context#pop () done; size := 0) +type 'a mlist = Nil | Cons of { hd : 'a ; mutable tl : 'a mlist } + +let enqueue a x = + let rec aux x = match x with + | Nil -> assert false + | Cons p -> + match p.tl with + | Nil -> p.tl <- Cons { hd = a ; tl = Nil } + | _ -> aux p.tl in + match !x with + | Nil -> x := Cons { hd = a ; tl = Nil } + | _ -> aux !x + +let pop = function + | Cons p -> p.tl + | Nil -> assert false + let flash_info = + let queue = ref Nil in let flash_context = status#new_context ~name:"Flash" in - (fun ?(delay=5000) s -> flash_context#flash ~delay s) + let rec process () = match !queue with + | Cons { hd = (delay,text) } -> + let msg = flash_context#push text in + ignore (Glib.Timeout.add ~ms:delay ~callback:(fun () -> + flash_context#remove msg; + queue := pop !queue; + process (); false)) + | Nil -> () in + fun ?(delay=5000) text -> + let processing = !queue <> Nil in + enqueue (delay,text) queue; + if not processing then process () (* Note: Setting the same attribute with two separate tags appears to use the first value applied and not the second. I saw this trying to set the background -- cgit v1.2.3 From 968f9b59f390182c3123217dd5b13f80a2ee08c2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 3 Nov 2018 15:52:23 +0100 Subject: Being more informative on the steps of selection of the preference file. --- ide/coqide_main.ml | 4 +-- ide/minilib.ml | 12 ++++++-- ide/minilib.mli | 15 ++++++++++ ide/preferences.ml | 83 ++++++++++++++++++++++++++++++++++++++--------------- ide/preferences.mli | 2 +- 5 files changed, 86 insertions(+), 30 deletions(-) diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml index f2ce2e8bd9..6f4c0ece31 100644 --- a/ide/coqide_main.ml +++ b/ide/coqide_main.ml @@ -49,9 +49,7 @@ let catch_gtk_messages () = let () = catch_gtk_messages () let load_prefs () = - try Preferences.load_pref () - with e -> Ideutils.flash_info - ("Could not load preferences ("^Printexc.to_string e^").") + Preferences.load_pref ~warn:(fun ~delay -> Ideutils.flash_info ~delay) let () = load_prefs (); diff --git a/ide/minilib.ml b/ide/minilib.ml index 09a7112098..04beb212ab 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -58,10 +58,16 @@ let coqide_data_dirs () = :: List.map coqify (Glib.get_system_data_dirs ()) @ [Envars.datadir ()] +let coqide_system_config_dirs () = + List.map coqify (Glib.get_system_config_dirs ()) + +let coqide_default_config_dir () = + Envars.configdir () + let coqide_config_dirs () = - coqide_config_home () - :: List.map coqify (Glib.get_system_config_dirs ()) - @ [Envars.configdir ()] + coqide_config_home () :: + coqide_system_config_dirs () @ + [coqide_default_config_dir ()] let is_prefix_of pre s = let i = ref 0 in diff --git a/ide/minilib.mli b/ide/minilib.mli index c5849cc2c9..7022d7d256 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -27,7 +27,22 @@ val debug : bool ref val log_pp : ?level:level -> Pp.t -> unit val log : ?level:level -> string -> unit +(* The directory where user config files are conventionally *) +(* installed on the current platform (as given by Glib) *) val coqide_config_home : unit -> string + +(* The directories where system-wide config files are conventionally *) +(* installed on the current platform (as given by Glib) *) +val coqide_system_config_dirs : unit -> string list + +(* The directory where default config files are installed at installation time *) +val coqide_default_config_dir : unit -> string + +(* The ordered list of directories where a config file is searched by default *) val coqide_config_dirs : unit -> string list + +(* The ordered list of directories where a data file is searched by default *) val coqide_data_dirs : unit -> string list + +(* Misc *) val is_prefix_of : string -> string -> bool diff --git a/ide/preferences.ml b/ide/preferences.ml index 52122441a1..10d779263b 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -10,8 +10,6 @@ open Configwin -let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc" -let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys" let lang_manager = GSourceView3.source_language_manager ~default:true let () = lang_manager#set_search_path ((Minilib.coqide_data_dirs ())@lang_manager#search_path) @@ -235,22 +233,13 @@ end end -let get_config_file name = +let get_config_file dirs name = let find_config dir = Sys.file_exists (Filename.concat dir name) in - let config_dir = List.find find_config (Minilib.coqide_config_dirs ()) in + let config_dir = List.find find_config dirs in Filename.concat config_dir name -(* Small hack to handle v8.3 to v8.4 change in configuration file *) -let loaded_pref_file = - try get_config_file "coqiderc" - with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqiderc" - -let loaded_accel_file = - try get_config_file "coqide.keys" - with Not_found -> Filename.concat (Option.default "" (Glib.get_home_dir ())) ".coqide.keys" - let get_unicode_bindings_local_file () = - try Some (get_config_file "coqide.bindings") + try Some (get_config_file [Minilib.coqide_config_home ()] "coqide.bindings") with Not_found -> None let get_unicode_bindings_default_file () = @@ -648,30 +637,78 @@ let tag_button () = let box = GPack.hbox () in new tag_button (Gobject.unsafe_cast box#as_widget) -let save_pref () = +(** Loading/saving preferences *) + +let pref_file = Filename.concat (Minilib.coqide_config_home ()) "coqiderc" +let accel_file = Filename.concat (Minilib.coqide_config_home ()) "coqide.keys" + +let save_accel_pref () = + if not (Sys.file_exists (Minilib.coqide_config_home ())) + then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; + GtkData.AccelMap.save accel_file + +let save_rc_pref () = if not (Sys.file_exists (Minilib.coqide_config_home ())) then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; - let () = try GtkData.AccelMap.save accel_file with _ -> () in let add = Util.String.Map.add in let fold key obj accu = add key (obj.get ()) accu in let prefs = Util.String.Map.fold fold !preferences Util.String.Map.empty in let prefs = Util.String.Map.fold Util.String.Map.add !unknown_preferences prefs in Config_lexer.print_file pref_file prefs -let load_pref () = - (* Load main preference file *) - let () = - let m = Config_lexer.load_file loaded_pref_file in +let save_pref () = + save_accel_pref (); + save_rc_pref () + +let try_load_pref_file loader warn file = + try + loader file + with + e -> warn ~delay:5000 ("Could not load " ^ file ^ " ("^Printexc.to_string e^")") + +let load_pref_file loader warn name = + try + let user_file = get_config_file [Minilib.coqide_config_home ()] name in + warn ~delay:2000 ("Loading " ^ user_file); + try_load_pref_file loader warn user_file + with Not_found -> + try + let system_wide_file = get_config_file (Minilib.coqide_system_config_dirs ()) name in + warn ~delay:5000 ("No user " ^ name ^ ", using system wide configuration"); + try_load_pref_file loader warn system_wide_file + with Not_found -> + (* Compatibility with oldest versions of CoqIDE (<= 8.4) *) + try + let old_user_file = get_config_file [Option.default "" (Glib.get_home_dir ())] ("."^name) in + warn ~delay:5000 ("No " ^ name ^ ", trying to recover from an older version of CoqIDE"); + try_load_pref_file loader warn old_user_file + with Not_found -> + (* Built-in configuration *) + try + let default_file = get_config_file [Minilib.coqide_default_config_dir ()] name in + warn ~delay:5000 ("No " ^ name ^ ", using default configuration file"); + try_load_pref_file loader warn default_file + with Not_found -> + warn ~delay:5000 ("No " ^ name ^ ", using default internal configuration") + +let load_accel_pref ~warn = + load_pref_file GtkData.AccelMap.load warn "coqide.keys" + +let load_rc_pref ~warn = + let loader file = + let m = Config_lexer.load_file file in let iter name v = if Util.String.Map.mem name !preferences then try (Util.String.Map.find name !preferences).set v with _ -> () else unknown_preferences := Util.String.Map.add name v !unknown_preferences in Util.String.Map.iter iter m in - (* Load file for bindings *) + load_pref_file loader warn "coqiderc"; attach_modifiers_callback () - let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in - () + +let load_pref ~warn = + load_rc_pref ~warn; + load_accel_pref ~warn let pstring name p = string ~f:p#set name p#get let pbool name p = bool ~f:p#set name p#get diff --git a/ide/preferences.mli b/ide/preferences.mli index 490756d4f2..6da6228545 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -107,7 +107,7 @@ val user_queries : (string * string) list preference val diffs : string preference val save_pref : unit -> unit -val load_pref : unit -> unit +val load_pref : warn:(delay:int -> string -> unit) -> unit val configure : ?apply:(unit -> unit) -> GWindow.window -> unit -- cgit v1.2.3 From 0cb8482b51f25b2f705f4da28f08424f48fa9c93 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 3 Nov 2018 15:55:20 +0100 Subject: Hack to have the "ready" status bar message not hiding flash notices. --- ide/coqide.ml | 1 - ide/coqide_main.ml | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/ide/coqide.ml b/ide/coqide.ml index 9cdfd0dc21..fb08195308 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1247,7 +1247,6 @@ let build_ui () = let () = refresh_notebook_pos () in let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in let () = lower_hbox#pack ~expand:true status#coerce in - let () = push_info ("Ready"^ if microPG#get then ", [μPG]" else "") in (* Location display *) let l = GMisc.label diff --git a/ide/coqide_main.ml b/ide/coqide_main.ml index 6f4c0ece31..1e04d269f6 100644 --- a/ide/coqide_main.ml +++ b/ide/coqide_main.ml @@ -52,6 +52,7 @@ let load_prefs () = Preferences.load_pref ~warn:(fun ~delay -> Ideutils.flash_info ~delay) let () = + Ideutils.push_info ("Ready"^ if Preferences.microPG#get then ", [μPG]" else ""); load_prefs (); let argl = List.tl (Array.to_list Sys.argv) in let argl = Coqide.read_coqide_args argl in -- cgit v1.2.3 From 00603110458a40b1fe4bd4d51545a3e9b685e83c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 3 Nov 2018 17:07:30 +0100 Subject: Using GTK+ PRIMARY to factorize CoqIDE keys between MacOS and others. This concerns zooming, undoing, displaying preferences. --- ide/MacOS/default_accel_map | 4 ++-- ide/coqide.ml | 10 +++++----- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map index 6bcf3b438f..4093d2012b 100644 --- a/ide/MacOS/default_accel_map +++ b/ide/MacOS/default_accel_map @@ -47,7 +47,7 @@ (gtk_accel_path "/View/Display notations" "n") ; (gtk_accel_path "/Tactics/Tactic fail" "") ; (gtk_accel_path "/Tactics/Tactic left" "") -(gtk_accel_path "/Edit/Undo" "u") +; (gtk_accel_path "/Edit/Undo" "u") ; (gtk_accel_path "/Templates/Template Infix" "") ; (gtk_accel_path "/Tactics/Tactic functional induction" "") ; (gtk_accel_path "/Tactics/Tactic clear" "") @@ -219,7 +219,7 @@ ; (gtk_accel_path "/Templates/Template Remark" "") ; (gtk_accel_path "/Templates/Template Set Undo" "") ; (gtk_accel_path "/Templates/Template Inductive" "") -(gtk_accel_path "/Edit/Preferences" "VoidSymbol") +; (gtk_accel_path "/Edit/Preferences" ",") ; (gtk_accel_path "/Export/Html" "") ; (gtk_accel_path "/Templates/Template Extraction Inline" "") ; (gtk_accel_path "/Tactics/Tactic absurd" "") diff --git a/ide/coqide.ml b/ide/coqide.ml index fb08195308..e0ae18dddc 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1016,7 +1016,7 @@ let build_ui () = menu edit_menu [ item "Edit" ~label:"_Edit"; - item "Undo" ~accel:"u" ~stock:`UNDO + item "Undo" ~accel:"u" ~stock:`UNDO ~callback:(cb_on_current_term (fun t -> t.script#undo ())); item "Redo" ~stock:`REDO ~callback:(cb_on_current_term (fun t -> t.script#redo ())); @@ -1035,7 +1035,7 @@ let build_ui () = ~callback:(cb_on_current_term (fun t -> t.finder#find_backward ())); item "External editor" ~label:"External editor" ~stock:`EDIT ~callback:(External.editor ~parent:w); - item "Preferences" ~accel:"comma" ~stock:`PREFERENCES + item "Preferences" ~accel:"comma" ~stock:`PREFERENCES ~callback:(fun _ -> begin try Preferences.configure ~apply:refresh_notebook_pos w @@ -1053,19 +1053,19 @@ let build_ui () = item "Next tab" ~label:"_Next tab" ~accel:"Right" ~stock:`GO_FORWARD ~callback:(fun _ -> notebook#next_page ()); - item "Zoom in" ~label:"_Zoom in" ~accel:("plus") + item "Zoom in" ~label:"_Zoom in" ~accel:("plus") ~stock:`ZOOM_IN ~callback:(fun _ -> let ft = Pango.Font.from_string text_font#get in Pango.Font.set_size ft (Pango.Font.get_size ft + Pango.scale); text_font#set (Pango.Font.to_string ft); save_pref ()); - item "Zoom out" ~label:"_Zoom out" ~accel:("minus") + item "Zoom out" ~label:"_Zoom out" ~accel:("minus") ~stock:`ZOOM_OUT ~callback:(fun _ -> let ft = Pango.Font.from_string text_font#get in Pango.Font.set_size ft (Pango.Font.get_size ft - Pango.scale); text_font#set (Pango.Font.to_string ft); save_pref ()); - item "Zoom fit" ~label:"_Zoom fit" ~accel:("0") + item "Zoom fit" ~label:"_Zoom fit" ~accel:("0") ~stock:`ZOOM_FIT ~callback:(cb_on_current_term MiscMenu.zoom_fit); toggle_item "Show Toolbar" ~label:"Show _Toolbar" ~active:(show_toolbar#get) -- cgit v1.2.3 From d338a42c261287439dd6e9bc07b40a68f2a71786 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 26 Sep 2018 22:18:00 +0200 Subject: Moving configuration of coqide.keys to the coqide executable. --- .gitignore | 2 + Makefile.ide | 5 +- ide/MacOS/default_accel_map | 366 -------------------------------------------- ide/preferences.ml | 17 +- 4 files changed, 12 insertions(+), 378 deletions(-) delete mode 100644 ide/MacOS/default_accel_map diff --git a/.gitignore b/.gitignore index 93b874eae3..587a6191ab 100644 --- a/.gitignore +++ b/.gitignore @@ -191,3 +191,5 @@ theories/*/*/*/dune /user-contrib/Ltac2/dune *.install !Makefile.install + +ide/coqide.keys diff --git a/Makefile.ide b/Makefile.ide index 0a11f83a18..081d15a1a2 100644 --- a/Makefile.ide +++ b/Makefile.ide @@ -59,7 +59,7 @@ IDEBINDINGS:=ide/default.bindings IDEBINDINGSSRC:=ide/default_bindings_src.ml IDEBINDINGSEXE:=ide/default_bindings_src.exe -IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png ide/MacOS/default_accel_map $(IDEBINDINGS) +IDEFILES=$(wildcard ide/*.lang) ide/coq_style.xml ide/coq.png $(IDEBINDINGS) ## GTK for Coqide MacOS bundle @@ -175,7 +175,6 @@ $(IDEBINDINGSEXE): $(IDEBINDINGSSRC) $(IDEBINDINGS): $(IDEBINDINGSEXE) $< $@ - #################### ## Install targets #################### @@ -224,7 +223,6 @@ install-ide-files: #Please update $(COQIDEAPP)/Contents/Resources/ at the same t $(MKDIR) $(FULLDATADIR) $(INSTALLLIB) ide/coq.png ide/*.lang ide/coq_style.xml $(IDEBINDINGS) $(FULLDATADIR) $(MKDIR) $(FULLCONFIGDIR) - if [ $(IDEINT) = QUARTZ ] ; then $(INSTALLLIB) ide/mac_default_accel_map $(FULLCONFIGDIR)/coqide.keys ; fi install-ide-info: $(MKDIR) $(FULLDOCDIR) @@ -271,7 +269,6 @@ $(COQIDEAPP)/Contents/Resources/immodules: $(COQIDEAPP)/Contents $(COQIDEAPP)/Contents/Resources/etc: $(COQIDEAPP)/Contents/Resources/lib $(MKDIR) $@/xdg/coq - $(INSTALLLIB) ide/MacOS/default_accel_map $@/xdg/coq/coqide.keys $(MKDIR) $@/gtk-3.0 { "$(PIXBUFBIN)/gdk-pixbuf-query-loaders" $@/../loaders/*.so |\ sed -e "s!/.*\(/loaders/.*.so\)!@executable_path/../Resources/\1!"; } \ diff --git a/ide/MacOS/default_accel_map b/ide/MacOS/default_accel_map deleted file mode 100644 index 4093d2012b..0000000000 --- a/ide/MacOS/default_accel_map +++ /dev/null @@ -1,366 +0,0 @@ -; coqide GtkAccelMap rc-file -*- scheme -*- -; this file is an automated accelerator map dump -; -; (gtk_accel_path "/Templates/Template Read Module" "") -; (gtk_accel_path "/Tactics/Tactic pattern" "") -(gtk_accel_path "/Templates/Definition" "d") -; (gtk_accel_path "/Templates/Template Program Lemma" "") -(gtk_accel_path "/Templates/Lemma" "l") -; (gtk_accel_path "/Templates/Template Fact" "") -; (gtk_accel_path "/Tactics/Tactic fold" "") -; (gtk_accel_path "/Help/About Coq" "") -; (gtk_accel_path "/Templates/Template Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. " "") -; (gtk_accel_path "/Templates/Template Hypothesis" "") -; (gtk_accel_path "/Tactics/Tactic repeat" "") -; (gtk_accel_path "/Templates/Template Unset Extraction Optimize" "") -; (gtk_accel_path "/Templates/Template Add Printing Constructor" "") -; (gtk_accel_path "/Windows/Detach View" "") -; (gtk_accel_path "/Tactics/Tactic inversion" "") -; (gtk_accel_path "/Templates/Template Write State" "") -; (gtk_accel_path "/Export/Export to" "") -; (gtk_accel_path "/Tactics/Tactic inversion--clear" "") -; (gtk_accel_path "/Templates/Template Implicit Arguments" "") -; (gtk_accel_path "/Edit/Copy" "c") -; (gtk_accel_path "/Tactics/Tactic inversion -- using" "") -; (gtk_accel_path "/View/Previous tab" "Left") -; (gtk_accel_path "/Tactics/Tactic change -- in" "") -; (gtk_accel_path "/Tactics/Tactic jp" "") -; (gtk_accel_path "/Tactics/Tactic red" "") -; (gtk_accel_path "/Templates/Template Coercion" "") -; (gtk_accel_path "/Templates/Template CoFixpoint" "") -; (gtk_accel_path "/Tactics/Tactic intros until" "") -; (gtk_accel_path "/Templates/Template Derive Dependent Inversion" "") -; (gtk_accel_path "/Tactics/Tactic eapply" "") -; (gtk_accel_path "/View/View" "") -; (gtk_accel_path "/Tactics/Tactic change" "") -; (gtk_accel_path "/Tactics/Tactic firstorder using" "") -; (gtk_accel_path "/Tactics/Tactic decompose sum" "") -; (gtk_accel_path "/Tactics/Tactic cut" "") -; (gtk_accel_path "/Templates/Template Remove Printing Let" "") -; (gtk_accel_path "/Templates/Template Structure" "") -; (gtk_accel_path "/Tactics/Tactic compute in" "") -; (gtk_accel_path "/Queries/Locate" "") -; (gtk_accel_path "/Templates/Template Save." "") -; (gtk_accel_path "/Templates/Template Canonical Structure" "") -; (gtk_accel_path "/Tactics/Tactic compare" "") -; (gtk_accel_path "/Templates/Template Next Obligation" "") -(gtk_accel_path "/View/Display notations" "n") -; (gtk_accel_path "/Tactics/Tactic fail" "") -; (gtk_accel_path "/Tactics/Tactic left" "") -; (gtk_accel_path "/Edit/Undo" "u") -; (gtk_accel_path "/Templates/Template Infix" "") -; (gtk_accel_path "/Tactics/Tactic functional induction" "") -; (gtk_accel_path "/Tactics/Tactic clear" "") -; (gtk_accel_path "/Templates/Template End Silent." "") -; (gtk_accel_path "/Tactics/Tactic intros" "") -; (gtk_accel_path "/Tactics/Tactic constructor -- with" "") -; (gtk_accel_path "/Tactics/Tactic destruct" "") -; (gtk_accel_path "/Tactics/Tactic intro after" "") -; (gtk_accel_path "/Tactics/Tactic abstract" "") -; (gtk_accel_path "/Compile/Compile buffer" "") -; (gtk_accel_path "/Queries/About" "F5") -; (gtk_accel_path "/Templates/Template CoInductive" "") -; (gtk_accel_path "/Templates/Template Test Printing Wildcard" "") -; (gtk_accel_path "/Templates/Template Unset Hyps--limit" "") -; (gtk_accel_path "/Templates/Template Transparent" "") -; (gtk_accel_path "/Export/Ps" "") -; (gtk_accel_path "/Tactics/Tactic elim" "") -; (gtk_accel_path "/Templates/Template Extract Constant" "") -; (gtk_accel_path "/Tactics/Tactic assert (--:--)" "") -; (gtk_accel_path "/Templates/Template Add Rec LoadPath" "") -; (gtk_accel_path "/Edit/Redo" "") -; (gtk_accel_path "/Tactics/Tactic compute" "") -; (gtk_accel_path "/Compile/Next error" "F7") -; (gtk_accel_path "/Templates/Template Add ML Path" "") -; (gtk_accel_path "/Templates/Template Test Printing If" "") -; (gtk_accel_path "/Templates/Template Load Verbose" "") -; (gtk_accel_path "/Templates/Template Reset Extraction Inline" "") -; (gtk_accel_path "/Templates/Template Set Implicit Arguments" "") -; (gtk_accel_path "/Templates/Template Test Printing Let" "") -; (gtk_accel_path "/Windows/Windows" "") -; (gtk_accel_path "/Templates/Template Defined." "") -(gtk_accel_path "/Templates/match" "c") -; (gtk_accel_path "/Tactics/Tactic set (--:=--)" "") -; (gtk_accel_path "/Templates/Template Proof." "") -; (gtk_accel_path "/Compile/Make" "F6") -; (gtk_accel_path "/Templates/Template Module Type" "") -; (gtk_accel_path "/Tactics/Tactic apply -- with" "") -; (gtk_accel_path "/File/Save as" "") -; (gtk_accel_path "/Templates/Template Set Hyps--limit" "") -; (gtk_accel_path "/Templates/Template Global Variable" "") -; (gtk_accel_path "/Templates/Template Remove Printing Constructor" "") -; (gtk_accel_path "/Templates/Template Add Setoid" "") -; (gtk_accel_path "/Edit/Find Next" "F3") -; (gtk_accel_path "/Edit/Find" "f") -; (gtk_accel_path "/Templates/Template Add Relation" "") -; (gtk_accel_path "/Queries/Print" "F4") -; (gtk_accel_path "/Templates/Template Obligations Tactic" "") -; (gtk_accel_path "/Tactics/Tactic trivial" "") -; (gtk_accel_path "/Tactics/Tactic first" "") -; (gtk_accel_path "/Tactics/Tactic case" "") -; (gtk_accel_path "/Templates/Template Hint Constructors" "") -; (gtk_accel_path "/Templates/Template Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T." "") -; (gtk_accel_path "/Templates/Template Coercion Local" "") -(gtk_accel_path "/View/Show Query Pane" "Escape") -; (gtk_accel_path "/Tactics/Tactic cbv" "") -; (gtk_accel_path "/Tactics/Tactic inversion--clear -- in" "") -; (gtk_accel_path "/Templates/Template Add Rec ML Path" "") -; (gtk_accel_path "/Tactics/Tactic apply" "") -; (gtk_accel_path "/Export/Latex" "") -; (gtk_accel_path "/Tactics/Tactic inversion -- using -- in" "") -; (gtk_accel_path "/Tactics/Tactic generalize" "") -(gtk_accel_path "/Navigation/Backward" "Up") -; (gtk_accel_path "/Tactics/Tactic p" "") -(gtk_accel_path "/Navigation/Hide" "h") -; (gtk_accel_path "/File/Close buffer" "w") -; (gtk_accel_path "/Tactics/Tactic induction" "") -; (gtk_accel_path "/Tactics/Tactic eauto with" "") -(gtk_accel_path "/View/Display raw matching expressions" "m") -; (gtk_accel_path "/Tactics/Tactic d" "") -; (gtk_accel_path "/Tactics/Tactic u" "") -; (gtk_accel_path "/Templates/Templates" "") -; (gtk_accel_path "/Tactics/Tactic s" "") -; (gtk_accel_path "/Tactics/Tactic lapply" "") -; (gtk_accel_path "/Tactics/Tactic t" "") -; (gtk_accel_path "/Tactics/Tactic r" "") -; (gtk_accel_path "/Edit/Replace" "r") -; (gtk_accel_path "/Tactics/Tactic case -- with" "") -; (gtk_accel_path "/Tactics/Tactic eexact" "") -; (gtk_accel_path "/Queries/Check" "F3") -; (gtk_accel_path "/Tactics/Tactic omega" "") -; (gtk_accel_path "/File/New" "n") -; (gtk_accel_path "/Tactics/Tactic l" "") -; (gtk_accel_path "/Tactics/Tactic intro" "") -; (gtk_accel_path "/Tactics/Tactic j" "") -; (gtk_accel_path "/Tactics/Tactic i" "") -; (gtk_accel_path "/Templates/Template Definition" "") -; (gtk_accel_path "/Tactics/Tactic g" "") -; (gtk_accel_path "/Tactics/Tactic f" "") -; (gtk_accel_path "/Tactics/Tactic e" "") -; (gtk_accel_path "/Tactics/Tactic c" "") -(gtk_accel_path "/File/Rehighlight" "l") -; (gtk_accel_path "/Tactics/Tactic simple inversion" "") -; (gtk_accel_path "/Tactics/Tactic a" "") -; (gtk_accel_path "/Templates/Template Mutual Inductive" "") -; (gtk_accel_path "/Templates/Template Extraction NoInline" "") -(gtk_accel_path "/Templates/Theorem" "t") -; (gtk_accel_path "/Templates/Template Derive Dependent Inversion--clear" "") -; (gtk_accel_path "/Tactics/Tactic unfold" "") -; (gtk_accel_path "/Tactics/Tactic red in" "") -; (gtk_accel_path "/Tactics/Tactic rewrite <- -- in" "") -; (gtk_accel_path "/Templates/Template Hint Extern" "") -; (gtk_accel_path "/Templates/Template Unfocus" "") -; (gtk_accel_path "/Tactics/Tactic dependent inversion--clear" "") -; (gtk_accel_path "/Help/Browse Coq Library" "") -; (gtk_accel_path "/Tactics/Tactic lazy" "") -; (gtk_accel_path "/Templates/Template Scheme" "") -(gtk_accel_path "/Tactics/tauto" "p") -; (gtk_accel_path "/Tactics/Tactic cutrewrite" "") -; (gtk_accel_path "/Tactics/Tactic contradiction" "") -; (gtk_accel_path "/Templates/Template Set Printing Wildcard" "") -; (gtk_accel_path "/Templates/Template Add LoadPath" "") -(gtk_accel_path "/Navigation/Previous" "less") -; (gtk_accel_path "/Templates/Template Require" "") -; (gtk_accel_path "/Tactics/Tactic simpl" "") -; (gtk_accel_path "/Templates/Template Require Import" "") -; (gtk_accel_path "/Templates/Template Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T." "") -(gtk_accel_path "/Navigation/Forward" "Down") -; (gtk_accel_path "/Tactics/Tactic rename -- into" "") -; (gtk_accel_path "/Compile/Compile" "") -; (gtk_accel_path "/File/Save all" "") -; (gtk_accel_path "/Tactics/Tactic fix" "") -; (gtk_accel_path "/Templates/Template Parameter" "") -; (gtk_accel_path "/Tactics/Tactic assert" "") -; (gtk_accel_path "/Tactics/Tactic do" "") -; (gtk_accel_path "/Tactics/Tactic ring" "") -; (gtk_accel_path "/Export/Pdf" "") -; (gtk_accel_path "/Tactics/Tactic quote" "") -; (gtk_accel_path "/Tactics/Tactic symmetry in" "") -; (gtk_accel_path "/Help/Help" "") -(gtk_accel_path "/Templates/Inductive" "i") -; (gtk_accel_path "/Tactics/Tactic idtac" "") -; (gtk_accel_path "/Templates/Template Syntax" "") -; (gtk_accel_path "/Tactics/Tactic intro -- after" "") -; (gtk_accel_path "/Tactics/Tactic fold -- in" "") -; (gtk_accel_path "/Templates/Template Program Definition" "") -; (gtk_accel_path "/Templates/Template Hint Resolve" "") -; (gtk_accel_path "/Templates/Template Set Extraction Optimize" "") -; (gtk_accel_path "/File/Revert all buffers" "") -; (gtk_accel_path "/Tactics/Tactic subst" "") -; (gtk_accel_path "/Tactics/Tactic autorewrite" "") -; (gtk_accel_path "/Tactics/Tactic pose" "") -; (gtk_accel_path "/Tactics/Tactic simplify--eq" "") -; (gtk_accel_path "/Tactics/Tactic clearbody" "") -; (gtk_accel_path "/Tactics/Tactic eauto" "") -; (gtk_accel_path "/Templates/Template Grammar" "") -; (gtk_accel_path "/Tactics/Tactic exact" "") -; (gtk_accel_path "/Templates/Template Unset Implicit Arguments" "") -; (gtk_accel_path "/Templates/Template Extract Inductive" "") -(gtk_accel_path "/View/Display implicit arguments" "i") -; (gtk_accel_path "/Tactics/Tactic symmetry" "") -; (gtk_accel_path "/Templates/Template Add Printing Let" "") -; (gtk_accel_path "/Help/Help for keyword" "h") -; (gtk_accel_path "/File/Save" "s") -; (gtk_accel_path "/Compile/Make makefile" "") -; (gtk_accel_path "/Templates/Template Remove LoadPath" "") -(gtk_accel_path "/Navigation/Interrupt" "Break") -(gtk_accel_path "/Navigation/End" "End") -; (gtk_accel_path "/Templates/Template Add Morphism" "") -; (gtk_accel_path "/Tactics/Tactic field" "") -; (gtk_accel_path "/Templates/Template Axiom" "") -; (gtk_accel_path "/Tactics/Tactic solve" "") -; (gtk_accel_path "/Tactics/Tactic casetype" "") -; (gtk_accel_path "/Tactics/Tactic cbv in" "") -; (gtk_accel_path "/Templates/Template Load" "") -; (gtk_accel_path "/Templates/Template Goal" "") -; (gtk_accel_path "/Tactics/Tactic exists" "") -; (gtk_accel_path "/Tactics/Tactic decompose record" "") -(gtk_accel_path "/Navigation/Go to" "Right") -; (gtk_accel_path "/Templates/Template Remark" "") -; (gtk_accel_path "/Templates/Template Set Undo" "") -; (gtk_accel_path "/Templates/Template Inductive" "") -; (gtk_accel_path "/Edit/Preferences" ",") -; (gtk_accel_path "/Export/Html" "") -; (gtk_accel_path "/Templates/Template Extraction Inline" "") -; (gtk_accel_path "/Tactics/Tactic absurd" "") -; (gtk_accel_path "/Tactics/Tactic simple induction" "") -; (gtk_accel_path "/Queries/Queries" "") -; (gtk_accel_path "/Tactics/Tactic rewrite -- in" "") -; (gtk_accel_path "/Templates/Template Hint Rewrite" "") -; (gtk_accel_path "/Templates/Template Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]." "") -; (gtk_accel_path "/Navigation/Navigation" "") -; (gtk_accel_path "/Help/Browse Coq Manual" "") -; (gtk_accel_path "/Tactics/Tactic transitivity" "") -; (gtk_accel_path "/Tactics/Tactic auto" "") -; (gtk_accel_path "/Tactics/Tactic dependent inversion -- with" "") -; (gtk_accel_path "/Tactics/Tactic assumption" "") -; (gtk_accel_path "/Templates/Template Notation" "") -; (gtk_accel_path "/Edit/Cut" "x") -; (gtk_accel_path "/Templates/Template Theorem" "") -; (gtk_accel_path "/Tactics/Tactic constructor" "") -; (gtk_accel_path "/Tactics/Tactic elim -- with" "") -; (gtk_accel_path "/Templates/Template Identity Coercion" "") -(gtk_accel_path "/View/Display all low-level contents" "l") -; (gtk_accel_path "/Tactics/Tactic right" "") -; (gtk_accel_path "/Edit/Find Previous" "F3") -; (gtk_accel_path "/Tactics/Tactic cofix" "") -; (gtk_accel_path "/Templates/Template Restore State" "") -; (gtk_accel_path "/Templates/Template Lemma" "") -; (gtk_accel_path "/Tactics/Tactic refine" "") -; (gtk_accel_path "/Templates/Template Section" "") -; (gtk_accel_path "/Tactics/Tactic assert (--:=--)" "") -; (gtk_accel_path "/Templates/Template Unset Printing Wildcard" "") -; (gtk_accel_path "/Tactics/Tactic progress" "") -; (gtk_accel_path "/Templates/Template Add Printing If" "") -; (gtk_accel_path "/Templates/Template Chapter" "") -(gtk_accel_path "/File/Print..." "p") -; (gtk_accel_path "/Templates/Template Record" "") -; (gtk_accel_path "/Tactics/Tactic info" "") -; (gtk_accel_path "/Tactics/Tactic firstorder with" "") -; (gtk_accel_path "/Templates/Template Hint Unfold" "") -; (gtk_accel_path "/Templates/Template Set Silent." "") -; (gtk_accel_path "/Templates/Template Program Theorem" "") -; (gtk_accel_path "/Templates/Template Declare ML Module" "") -; (gtk_accel_path "/Tactics/Tactic lazy in" "") -; (gtk_accel_path "/Tactics/Tactic unfold -- in" "") -; (gtk_accel_path "/Edit/Paste" "v") -; (gtk_accel_path "/Templates/Template Remove Printing If" "") -; (gtk_accel_path "/Tactics/Tactic intuition" "") -; (gtk_accel_path "/Queries/SearchAbout" "F2") -; (gtk_accel_path "/Tactics/Tactic dependent rewrite ->" "") -; (gtk_accel_path "/Templates/Template Module" "") -; (gtk_accel_path "/Templates/Template Unset Extraction AutoInline" "") -(gtk_accel_path "/Templates/Scheme" "s") -; (gtk_accel_path "/Templates/Template V" "") -; (gtk_accel_path "/Templates/Template Variable" "") -; (gtk_accel_path "/Tactics/Tactic decide equality" "") -; (gtk_accel_path "/Tactics/Tactic instantiate (--:=--)" "") -; (gtk_accel_path "/Templates/Template Syntactic Definition" "") -; (gtk_accel_path "/Templates/Template Set Extraction AutoInline" "") -; (gtk_accel_path "/Templates/Template Unset Undo" "") -; (gtk_accel_path "/Tactics/Tactic dependent inversion" "") -; (gtk_accel_path "/Tactics/Tactic setoid--rewrite" "") -; (gtk_accel_path "/Templates/Template Add Field" "") -; (gtk_accel_path "/Templates/Template Require Export" "") -; (gtk_accel_path "/Tactics/Tactic rewrite <-" "") -; (gtk_accel_path "/Tactics/Tactic split" "") -; (gtk_accel_path "/File/Quit" "q") -(gtk_accel_path "/View/Display existential variable instances" "e") -(gtk_accel_path "/Navigation/Start" "Home") -; (gtk_accel_path "/Tactics/Tactic dependent rewrite <-" "") -; (gtk_accel_path "/Templates/Template U" "") -; (gtk_accel_path "/Templates/Template Variables" "") -; (gtk_accel_path "/Templates/Template S" "") -; (gtk_accel_path "/Tactics/Tactic move -- after" "") -; (gtk_accel_path "/Templates/Template Unset Silent." "") -; (gtk_accel_path "/Templates/Template Local" "") -; (gtk_accel_path "/Templates/Template T" "") -; (gtk_accel_path "/Tactics/Tactic reflexivity" "") -; (gtk_accel_path "/Templates/Template R" "") -; (gtk_accel_path "/Templates/Template Time" "") -; (gtk_accel_path "/Templates/Template P" "") -; (gtk_accel_path "/Tactics/Tactic decompose" "") -; (gtk_accel_path "/Templates/Template N" "") -; (gtk_accel_path "/Templates/Template Eval" "") -; (gtk_accel_path "/Tactics/Tactic congruence" "") -; (gtk_accel_path "/Templates/Template O" "") -; (gtk_accel_path "/Templates/Template E" "") -; (gtk_accel_path "/Templates/Template I" "") -; (gtk_accel_path "/Templates/Template H" "") -; (gtk_accel_path "/Templates/Template Extraction Language" "") -; (gtk_accel_path "/Templates/Template M" "") -; (gtk_accel_path "/Templates/Template Derive Inversion" "") -; (gtk_accel_path "/Tactics/Tactic double induction" "") -; (gtk_accel_path "/Templates/Template L" "") -; (gtk_accel_path "/Templates/Template Derive Inversion--clear" "") -(gtk_accel_path "/View/Display universe levels" "u") -; (gtk_accel_path "/Templates/Template G" "") -; (gtk_accel_path "/Templates/Template F" "") -; (gtk_accel_path "/Tactics/Tactic dependent inversion--clear -- with" "") -; (gtk_accel_path "/Templates/Template D" "") -; (gtk_accel_path "/Edit/Edit" "") -; (gtk_accel_path "/Tactics/Tactic firstorder" "") -; (gtk_accel_path "/Templates/Template C" "") -; (gtk_accel_path "/Tactics/Tactic replace -- with" "") -; (gtk_accel_path "/Templates/Template A" "") -; (gtk_accel_path "/Templates/Template Remove Printing Record" "") -; (gtk_accel_path "/Templates/Template Qed." "") -; (gtk_accel_path "/Templates/Template Program Fixpoint" "") -(gtk_accel_path "/View/Display coercions" "c") -; (gtk_accel_path "/Tactics/Tactic hnf" "") -; (gtk_accel_path "/Tactics/Tactic injection" "") -; (gtk_accel_path "/Tactics/Tactic rewrite" "") -; (gtk_accel_path "/Templates/Template Opaque" "") -; (gtk_accel_path "/Templates/Template Focus" "") -; (gtk_accel_path "/Templates/Template Ltac" "") -; (gtk_accel_path "/Tactics/Tactic simple destruct" "") -(gtk_accel_path "/View/Display all basic low-level contents" "a") -; (gtk_accel_path "/Tactics/Tactic jp " "") -; (gtk_accel_path "/Templates/Template Test Printing Synth" "") -; (gtk_accel_path "/Tactics/Tactic set" "") -; (gtk_accel_path "/Edit/External editor" "") -; (gtk_accel_path "/View/Show Toolbar" "") -; (gtk_accel_path "/Tactics/Tactic try" "") -; (gtk_accel_path "/Tactics/Tactic discriminate" "") -(gtk_accel_path "/Templates/Fixpoint" "f") -(gtk_accel_path "/Edit/Complete Word" "slash") -(gtk_accel_path "/Navigation/Next" "greater") -; (gtk_accel_path "/Tactics/Tactic elimtype" "") -; (gtk_accel_path "/Templates/Template End" "") -; (gtk_accel_path "/Templates/Template Fixpoint" "") -; (gtk_accel_path "/View/Next tab" "Right") -; (gtk_accel_path "/File/File" "") -; (gtk_accel_path "/Tactics/Tactic setoid--replace" "") -; (gtk_accel_path "/Tactics/Tactic generalize dependent" "") -; (gtk_accel_path "/Tactics/Tactic fix -- with" "") -; (gtk_accel_path "/Tactics/Tactic pose --:=--)" "") -; (gtk_accel_path "/Tactics/Tactic auto with" "") -; (gtk_accel_path "/Templates/Template Add Printing Record" "") -; (gtk_accel_path "/Tactics/Tactic inversion -- in" "") -; (gtk_accel_path "/File/Open" "o") -; (gtk_accel_path "/Tactics/Tactic elim -- using" "") -; (gtk_accel_path "/Templates/Template Hint" "") -; (gtk_accel_path "/Tactics/Tactic tauto" "") -; (gtk_accel_path "/Export/Dvi" "") -; (gtk_accel_path "/Tactics/Tactic simpl -- in" "") -; (gtk_accel_path "/Templates/Template Hint Immediate" "") diff --git a/ide/preferences.ml b/ide/preferences.ml index 10d779263b..2cc98e6927 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -321,17 +321,23 @@ let attach_modifiers (pref : string preference) prefix = in pref#connect#changed ~callback:cb +let select_arch m m_osx = + if Coq_config.arch = "Darwin" then m_osx else m + let modifier_for_navigation = - new preference ~name:["modifier_for_navigation"] ~init:"" ~repr:Repr.(string) + new preference ~name:["modifier_for_navigation"] + ~init:(select_arch "" "") ~repr:Repr.(string) let modifier_for_templates = new preference ~name:["modifier_for_templates"] ~init:"" ~repr:Repr.(string) let modifier_for_tactics = - new preference ~name:["modifier_for_tactics"] ~init:"" ~repr:Repr.(string) + new preference ~name:["modifier_for_tactics"] + ~init:(select_arch "" "") ~repr:Repr.(string) let modifier_for_display = - new preference ~name:["modifier_for_display"] ~init:"" ~repr:Repr.(string) + new preference ~name:["modifier_for_display"] + ~init:(select_arch "" "")~repr:Repr.(string) let modifier_for_queries = new preference ~name:["modifier_for_queries"] ~init:"" ~repr:Repr.(string) @@ -684,11 +690,6 @@ let load_pref_file loader warn name = try_load_pref_file loader warn old_user_file with Not_found -> (* Built-in configuration *) - try - let default_file = get_config_file [Minilib.coqide_default_config_dir ()] name in - warn ~delay:5000 ("No " ^ name ^ ", using default configuration file"); - try_load_pref_file loader warn default_file - with Not_found -> warn ~delay:5000 ("No " ^ name ^ ", using default internal configuration") let load_accel_pref ~warn = -- cgit v1.2.3 From f612bee8c1723b4d66fe1ba93dbb23f5bd201ae6 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 5 Apr 2019 19:53:48 +0200 Subject: Moving a standard string function (is_prefix) from Minilib to CString. --- clib/cString.ml | 4 ++++ clib/cString.mli | 3 +++ ide/coqide.ml | 2 +- ide/minilib.ml | 10 ---------- ide/minilib.mli | 3 --- 5 files changed, 8 insertions(+), 14 deletions(-) diff --git a/clib/cString.ml b/clib/cString.ml index 60915efe86..99fb7d2b78 100644 --- a/clib/cString.ml +++ b/clib/cString.ml @@ -24,6 +24,7 @@ sig val conjugate_verb_to_be : int -> string val ordinal : int -> string val is_sub : string -> string -> int -> bool + val is_prefix : string -> string -> bool module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set module List : CList.MonoS with type elt = t @@ -101,6 +102,9 @@ let is_sub p s off = in aux 0 +let is_prefix p s = + is_sub p s 0 + let plural n s = if n<>1 then s^"s" else s let conjugate_verb_to_be n = if n<>1 then "are" else "is" diff --git a/clib/cString.mli b/clib/cString.mli index 8a4fe62a1c..d02be2d15f 100644 --- a/clib/cString.mli +++ b/clib/cString.mli @@ -51,6 +51,9 @@ sig val is_sub : string -> string -> int -> bool (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *) + val is_prefix : string -> string -> bool + (** [is_prefix p s] tests whether [p] is a prefix of [s]. *) + (** {6 Generic operations} **) module Set : Set.S with type elt = t diff --git a/ide/coqide.ml b/ide/coqide.ml index e0ae18dddc..70fa61b208 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1371,7 +1371,7 @@ let read_coqide_args argv = |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; filter_coqtop coqtop project_files bindings_files out args - |arg::args when out = [] && Minilib.is_prefix_of "-psn_" arg -> + |arg::args when out = [] && CString.is_prefix "-psn_" arg -> (* argument added by MacOS during .app launch *) filter_coqtop coqtop project_files bindings_files out args |arg::args -> filter_coqtop coqtop project_files bindings_files (arg::out) args diff --git a/ide/minilib.ml b/ide/minilib.ml index 04beb212ab..926ad27abc 100644 --- a/ide/minilib.ml +++ b/ide/minilib.ml @@ -68,13 +68,3 @@ let coqide_config_dirs () = coqide_config_home () :: coqide_system_config_dirs () @ [coqide_default_config_dir ()] - -let is_prefix_of pre s = - let i = ref 0 in - let () = while (!i < (String.length pre) - && !i < (String.length s) - && pre.[!i] = s.[!i]) do - incr i - done - in !i = String.length pre - diff --git a/ide/minilib.mli b/ide/minilib.mli index 7022d7d256..a9d26ee7d2 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -43,6 +43,3 @@ val coqide_config_dirs : unit -> string list (* The ordered list of directories where a data file is searched by default *) val coqide_data_dirs : unit -> string list - -(* Misc *) -val is_prefix_of : string -> string -> bool -- cgit v1.2.3 From d5af8a969cfbd32484b4939bfeff153c86fc2fe2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 10 Sep 2019 15:16:29 +0200 Subject: CoqIDE: removing option contextual menu on goal, inactive since 2da5db43c. --- ide/preferences.ml | 7 +------ ide/preferences.mli | 1 - 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/ide/preferences.ml b/ide/preferences.ml index 2cc98e6927..7b667027fc 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -379,9 +379,6 @@ let text_font = let show_toolbar = new preference ~name:["show_toolbar"] ~init:true ~repr:Repr.(bool) -let contextual_menus_on_goal = - new preference ~name:["contextual_menus_on_goal"] ~init:true ~repr:Repr.(bool) - let window_width = new preference ~name:["window_width"] ~init:800 ~repr:Repr.(int) @@ -982,9 +979,7 @@ let configure ?(apply=(fun () -> ())) parent = cmd_browse#get in - let contextual_menus_on_goal = pbool "Contextual menus on goal" contextual_menus_on_goal in - - let misc = [contextual_menus_on_goal;stop_before;reset_on_tab_switch; + let misc = [stop_before;reset_on_tab_switch; vertical_tabs;opposite_tabs] in (* diff --git a/ide/preferences.mli b/ide/preferences.mli index 6da6228545..4b04326cec 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -79,7 +79,6 @@ val cmd_browse : string preference val cmd_editor : string preference val text_font : string preference val show_toolbar : bool preference -val contextual_menus_on_goal : bool preference val window_width : int preference val window_height : int preference val auto_complete : bool preference -- cgit v1.2.3 From 36bc8d2b666457c18436c1801d7ba811ed2c2067 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 26 Apr 2019 20:54:29 +0200 Subject: Fixing coqide doc about location of "coqiderc" and "coqide.bindings". --- doc/sphinx/practical-tools/coqide.rst | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 7d6171285e..92b7fd403c 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -179,10 +179,13 @@ compilation, printing, web browsing. In the browser command, you may use `%s` to denote the URL to open, for example: `firefox -remote "OpenURL(%s)"`. -Notice that these settings are saved in the file `.coqiderc` of your -home directory. +Notice that these settings are saved in the file ``coqiderc`` in the +``coq`` subdirectory of the user configuration directory which +is the value of ``$XDG_CONFIG_HOME`` if this environment variable is +set and which otherwise is ``$HOME/.config/``. -A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It +A Gtk2 accelerator keymap is saved under the name ``coqide.keys`` in +the same ``coq`` subdirectory of the user configuration directory. It is not recommended to edit this file manually: to modify a given menu shortcut, go to the corresponding menu item without releasing the mouse button, press the key you want for the new shortcut, and release @@ -259,8 +262,9 @@ Adding custom bindings ~~~~~~~~~~~~~~~~~~~~~~ To extend the default set of bindings, create a file named ``coqide.bindings`` -and place it in the same folder as ``coqide.keys``. On Linux, this would be -the folder ``~/.config/coq``. The file `coqide.bindings` should contain one +and place it in the same folder as ``coqide.keys``. This would be +the folder ``$XDG_CONFIG_HOME/coq``, defaulting to ``~/.config/coq`` +if ``XDG_CONFIG_HOME`` is unset. The file `coqide.bindings` should contain one binding per line, in the form ``\key value``, followed by an optional priority integer. (The key and value should not contain any space character.) -- cgit v1.2.3 From bc10e4566cefcab6449fb97b47cf23a431c5e8bb Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 16 Jun 2019 13:58:41 +0200 Subject: Refman: To be compatible gtk2/gtk3, not mentioning GTK+ version explicitely. --- doc/sphinx/practical-tools/coqide.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 92b7fd403c..b1f392c337 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -184,7 +184,7 @@ Notice that these settings are saved in the file ``coqiderc`` in the is the value of ``$XDG_CONFIG_HOME`` if this environment variable is set and which otherwise is ``$HOME/.config/``. -A Gtk2 accelerator keymap is saved under the name ``coqide.keys`` in +A GTK+ accelerator keymap is saved under the name ``coqide.keys`` in the same ``coq`` subdirectory of the user configuration directory. It is not recommended to edit this file manually: to modify a given menu shortcut, go to the corresponding menu item without releasing the -- cgit v1.2.3