diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/.merlin.in | 2 | ||||
| -rw-r--r-- | ide/coq-ssreflect.lang | 2 | ||||
| -rw-r--r-- | ide/idetop.ml | 25 | ||||
| -rw-r--r-- | ide/macos_prehook.ml | 6 | ||||
| -rw-r--r-- | ide/preferences.ml | 23 |
5 files changed, 32 insertions, 26 deletions
diff --git a/ide/.merlin.in b/ide/.merlin.in index 4dc6f45550..b8d7953833 100644 --- a/ide/.merlin.in +++ b/ide/.merlin.in @@ -1,4 +1,4 @@ -PKG unix laglgtk2 lablgtk2.sourceview2 +PKG unix laglgtk3 lablgtk3-sourceview3 S utils B utils diff --git a/ide/coq-ssreflect.lang b/ide/coq-ssreflect.lang index bd9cb4bfa2..fc7bc64a68 100644 --- a/ide/coq-ssreflect.lang +++ b/ide/coq-ssreflect.lang @@ -73,11 +73,13 @@ <keyword>suffices</keyword> <keyword>suff</keyword> <keyword>transitivity</keyword> + <keyword>under</keyword> <keyword>without loss</keyword> <keyword>wlog</keyword> </context> <context id="ssr-endtac" style-ref="endtactic"> <keyword>by</keyword> + <keyword>over</keyword> <keyword>exact</keyword> <keyword>reflexivity</keyword> </context> diff --git a/ide/idetop.ml b/ide/idetop.ml index 10b8a2cdc5..38839f3488 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -57,9 +57,9 @@ let coqide_known_option table = List.mem table [ ["Diffs"]] let is_known_option cmd = match Vernacprop.under_control cmd with - | VernacSetOption (_, o, BoolValue true) - | VernacSetOption (_, o, StringValue _) - | VernacUnsetOption (_, o) -> coqide_known_option o + | VernacSetOption (_, o, OptionSetTrue) + | VernacSetOption (_, o, OptionSetString _) + | VernacSetOption (_, o, OptionUnset) -> coqide_known_option o | _ -> false (** Check whether a command is forbidden in the IDE *) @@ -238,7 +238,8 @@ let goals () = Some (export_pre_goals Proof.(data newp) (process_goal_diffs diff_goal_map oldp)) end else Some (export_pre_goals Proof.(data newp) process_goal) - with Vernacstate.Proof_global.NoCurrentProof -> None;; + with Vernacstate.Proof_global.NoCurrentProof -> None + [@@ocaml.warning "-3"];; let evars () = try @@ -251,6 +252,7 @@ let evars () = let el = List.map map_evar exl in Some el with Vernacstate.Proof_global.NoCurrentProof -> None + [@@ocaml.warning "-3"] let hints () = try @@ -264,7 +266,7 @@ let hints () = let hint_hyps = List.rev (Environ.fold_named_context get_hint_hyp env ~init: []) in Some (hint_hyps, concl_next_tac) with Vernacstate.Proof_global.NoCurrentProof -> None - + [@@ocaml.warning "-3"] (** Other API calls *) @@ -297,6 +299,7 @@ let status force = Interface.status_allproofs = allproofs; Interface.status_proofnum = Stm.current_proof_depth ~doc:(get_doc ()); } + [@@ocaml.warning "-3"] let export_coq_object t = { Interface.coq_object_prefix = t.Search.coq_object_prefix; @@ -340,6 +343,7 @@ let search flags = List.map export_coq_object (Search.interface_search ?pstate ( List.map (fun (c, b) -> (import_search_constraint c, b)) flags) ) + [@@ocaml.warning "-3"] let export_option_value = function | Goptions.BoolValue b -> Interface.BoolValue b @@ -366,12 +370,13 @@ let get_options () = Goptions.OptionMap.fold fold table [] let set_options options = + let open Goptions in let iter (name, value) = match import_option_value value with - | BoolValue b -> Goptions.set_bool_option_value name b - | IntValue i -> Goptions.set_int_option_value name i - | StringValue s -> Goptions.set_string_option_value name s - | StringOptValue (Some s) -> Goptions.set_string_option_value name s - | StringOptValue None -> Goptions.unset_option_value_gen name + | BoolValue b -> set_bool_option_value name b + | IntValue i -> set_int_option_value name i + | StringValue s -> set_string_option_value name s + | StringOptValue (Some s) -> set_string_option_value name s + | StringOptValue None -> unset_option_value_gen name in List.iter iter options diff --git a/ide/macos_prehook.ml b/ide/macos_prehook.ml index d668788954..dc8fd0e85d 100644 --- a/ide/macos_prehook.ml +++ b/ide/macos_prehook.ml @@ -24,13 +24,13 @@ let () = Unix.putenv "GTK_DATA_PREFIX" resources_dir let () = Unix.putenv "GTK_EXE_PREFIX" resources_dir let () = Unix.putenv "GTK_PATH" resources_dir let () = - Unix.putenv "GTK2_RC_FILES" (Filename.concat etc_dir "gtk-2.0/gtkrc") + Unix.putenv "GTK3_RC_FILES" (Filename.concat etc_dir "gtk-3.0/gtkrc") let () = Unix.putenv "GTK_IM_MODULE_FILE" - (Filename.concat etc_dir "gtk-2.0/gtk-immodules.loaders") + (Filename.concat etc_dir "gtk-3.0/gtk-immodules.loaders") let () = Unix.putenv "GDK_PIXBUF_MODULE_FILE" - (Filename.concat etc_dir "gtk-2.0/gdk-pixbuf.loaders") + (Filename.concat etc_dir "gtk-3.0/gdk-pixbuf.loaders") let () = Unix.putenv "PANGO_LIBDIR" lib_dir let () = Unix.putenv "PANGO_SYSCONFIGDIR" etc_dir let () = Unix.putenv "CHARSETALIASDIR" lib_dir diff --git a/ide/preferences.ml b/ide/preferences.ml index 47cd4c58b6..3893d023bd 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -263,8 +263,6 @@ let get_unicode_bindings_default_file () = (** Hooks *) -(** New style preferences *) - let cmd_coqtop = new preference ~name:["cmd_coqtop"] ~init:None ~repr:Repr.(option string) @@ -645,8 +643,6 @@ let tag_button () = let box = GPack.hbox () in new tag_button (Gobject.unsafe_cast box#as_widget) -(** Old style preferences *) - let save_pref () = if not (Sys.file_exists (Minilib.coqide_config_home ())) then Unix.mkdir (Minilib.coqide_config_home ()) 0o700; @@ -658,15 +654,18 @@ let save_pref () = 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 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 *) let () = try GtkData.AccelMap.load loaded_accel_file with _ -> () in - - let m = Config_lexer.load_file loaded_pref_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 + () let pstring name p = string ~f:p#set name p#get let pbool name p = bool ~f:p#set name p#get |