diff options
| author | Hugo Herbelin | 2018-11-19 16:37:38 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2019-03-19 08:40:18 +0000 |
| commit | 09fb7dbd2ca87fcd64a3d6d99eb5e537aadd0c06 (patch) | |
| tree | 77f03f6be92252ef852cf0dec1857adfb66ca11e /ide/preferences.ml | |
| parent | 06fc3fa551aeb53fbe06acad5d42b61201927c22 (diff) | |
CoqIDE: Deactivating the user queries and wizard tactics configuration.
They rely on list and strings from configwin which themselves rely on
gtk2 only widgets.
Diffstat (limited to 'ide/preferences.ml')
| -rw-r--r-- | ide/preferences.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/ide/preferences.ml b/ide/preferences.ml index 1f4b9ced2d..7e53dee351 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -921,6 +921,7 @@ let configure ?(apply=(fun () -> ())) parent = else cmd_browse#get]) cmd_browse#get in +(* let automatic_tactics = strings ~f:automatic_tactics#set @@ -929,12 +930,14 @@ let configure ?(apply=(fun () -> ())) parent = automatic_tactics#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; vertical_tabs;opposite_tabs] in +(* let add_user_query () = let input_string l v = match GToolbox.input_string ~title:l v with @@ -964,6 +967,7 @@ let configure ?(apply=(fun () -> ())) parent = user_queries#get in +*) (* ATTENTION !!!!! L'onglet Fonts doit etre en premier pour eviter un bug !!!! (shame on Benjamin) *) @@ -987,12 +991,14 @@ let configure ?(apply=(fun () -> ())) parent = Section("Externals", None, [cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc; cmd_print;cmd_editor;cmd_browse]); +(* Section("Tactics Wizard", None, [automatic_tactics]); +*) Section("Shortcuts", Some `PREFERENCES, [modifiers_valid; modifier_for_tactics; modifier_for_templates; modifier_for_display; modifier_for_navigation; - modifier_for_queries; user_queries]); + modifier_for_queries (*; user_queries *)]); Section("Misc", Some `ADD, misc)] in |