diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq-ssreflect.lang | 2 | ||||
| -rw-r--r-- | ide/idetop.ml | 8 | ||||
| -rw-r--r-- | ide/preferences.ml | 23 |
3 files changed, 19 insertions, 14 deletions
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 543ff924bd..38839f3488 100644 --- a/ide/idetop.ml +++ b/ide/idetop.ml @@ -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 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 |