aboutsummaryrefslogtreecommitdiff
path: root/ide
diff options
context:
space:
mode:
Diffstat (limited to 'ide')
-rw-r--r--ide/coq_commands.ml195
-rw-r--r--ide/coq_commands.mli1
-rw-r--r--ide/coqide.ml13
-rw-r--r--ide/coqide_ui.ml5
-rw-r--r--ide/idetop.ml1
-rw-r--r--ide/preferences.ml10
-rw-r--r--ide/preferences.mli1
-rw-r--r--ide/protocol/interface.ml2
-rw-r--r--ide/protocol/xmlprotocol.ml10
9 files changed, 7 insertions, 231 deletions
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index bfd99e7ce3..5b9ea17ba7 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -228,198 +228,3 @@ let state_preserving = [
"Test Printing Wildcard";
]
-
-
-let tactics =
- [
- [
- "abstract";
- "absurd";
- "apply";
- "apply __ with";
- "assert";
- "assert (__:__)";
- "assert (__:=__)";
- "assumption";
- "auto";
- "auto with";
- "autorewrite";
- ];
-
- [
- "case";
- "case __ with";
- "casetype";
- "cbv";
- "cbv in";
- "change";
- "change __ in";
- "clear";
- "clearbody";
- "cofix";
- "compare";
- "compute";
- "compute in";
- "congruence";
- "constructor";
- "constructor __ with";
- "contradiction";
- "cut";
- "cutrewrite";
- ];
-
- [
- "decide equality";
- "decompose";
- "decompose record";
- "decompose sum";
- "dependent inversion";
- "dependent inversion __ with";
- "dependent inversion__clear";
- "dependent inversion__clear __ with";
- "dependent rewrite ->";
- "dependent rewrite <-";
- "destruct";
- "discriminate";
- "do";
- "double induction";
- ];
-
- [
- "eapply";
- "eauto";
- "eauto with";
- "eexact";
- "elim";
- "elim __ using";
- "elim __ with";
- "elimtype";
- "exact";
- "exists";
- ];
-
- [
- "fail";
- "field";
- "first";
- "firstorder";
- "firstorder using";
- "firstorder with";
- "fix";
- "fix __ with";
- "fold";
- "fold __ in";
- "functional induction";
- ];
-
- [
- "generalize";
- "generalize dependent";
- ];
-
- [
- "hnf";
- ];
-
- [
- "idtac";
- "induction";
- "info";
- "injection";
- "instantiate (__:=__)";
- "intro";
- "intro after";
- "intro __ after";
- "intros";
- "intros until";
- "intuition";
- "inversion";
- "inversion __ in";
- "inversion __ using";
- "inversion __ using __ in";
- "inversion__clear";
- "inversion__clear __ in";
- ];
-
- [
- "jp <n>";
- "jp";
- ];
-
- [
- "lapply";
- "lazy";
- "lazy in";
- "left";
- ];
-
- [
- "move __ after";
- ];
-
- [
- "omega";
- ];
-
- [
- "pattern";
- "pose";
- "pose __:=__)";
- "progress";
- ];
-
- [
- "quote";
- ];
-
- [
- "red";
- "red in";
- "refine";
- "reflexivity";
- "rename __ into";
- "repeat";
- "replace __ with";
- "rewrite";
- "rewrite __ in";
- "rewrite <-";
- "rewrite <- __ in";
- "right";
- "ring";
- ];
-
- [
- "set";
- "set (__:=__)";
- "setoid__replace";
- "setoid__rewrite";
- "simpl";
- "simpl __ in";
- "simple destruct";
- "simple induction";
- "simple inversion";
- "simplify__eq";
- "solve";
- "split";
-(* "split__Rabs";
- "split__Rmult";
-*)
- "subst";
- "symmetry";
- "symmetry in";
- ];
-
- [
- "tauto";
- "transitivity";
- "trivial";
- "try";
- ];
-
- [
- "unfold";
- "unfold __ in";
- ];
-]
-
-
diff --git a/ide/coq_commands.mli b/ide/coq_commands.mli
index 5f8ce30901..c8c11f77af 100644
--- a/ide/coq_commands.mli
+++ b/ide/coq_commands.mli
@@ -8,6 +8,5 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val tactics : string list list
val commands : string list list
val state_preserving : string list
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 918c196968..ccf6d40b2b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -977,7 +977,6 @@ let build_ui () =
let view_menu = GAction.action_group ~name:"View" () in
let export_menu = GAction.action_group ~name:"Export" () in
let navigation_menu = GAction.action_group ~name:"Navigation" () in
- let tactics_menu = GAction.action_group ~name:"Tactics" () in
let templates_menu = GAction.action_group ~name:"Templates" () in
let tools_menu = GAction.action_group ~name:"Tools" () in
let queries_menu = GAction.action_group ~name:"Queries" () in
@@ -985,7 +984,7 @@ let build_ui () =
let windows_menu = GAction.action_group ~name:"Windows" () in
let help_menu = GAction.action_group ~name:"Help" () in
let all_menus = [
- file_menu; edit_menu; view_menu; export_menu; navigation_menu; tactics_menu;
+ file_menu; edit_menu; view_menu; export_menu; navigation_menu;
templates_menu; tools_menu; queries_menu; compile_menu; windows_menu;
help_menu; ] in
@@ -996,8 +995,6 @@ let build_ui () =
item "Save" ~callback:(File.save ~parent:w) ~stock:`SAVE ~tooltip:"Save current buffer";
item "Save as" ~label:"S_ave as" ~stock:`SAVE_AS ~callback:(File.saveas ~parent:w);
item "Save all" ~label:"Sa_ve all" ~callback:File.saveall;
- item "Revert all buffers" ~label:"_Revert all buffers"
- ~callback:(File.revert_all ~parent:w) ~stock:`REVERT_TO_SAVED;
item "Close buffer" ~label:"_Close buffer" ~stock:`CLOSE
~callback:(File.close_buffer ~parent:w) ~tooltip:"Close current buffer";
item "Print..." ~label:"_Print..."
@@ -1121,11 +1118,6 @@ let build_ui () =
("Force", "_Force", `EXECUTE, Nav.join_document, "Fully check the document", "f");
] end;
- menu tactics_menu [
- item "Tactics" ~label:"_Tactics";
- ];
- alpha_items tactics_menu "Tactic" Coq_commands.tactics;
-
menu templates_menu [
item "Templates" ~label:"Te_mplates";
template_item ("Lemma new_lemma : .\nProof.\n\nQed.\n", 6,9, "J");
@@ -1209,7 +1201,6 @@ let build_ui () =
Coqide_ui.ui_m#insert_action_group edit_menu 0;
Coqide_ui.ui_m#insert_action_group view_menu 0;
Coqide_ui.ui_m#insert_action_group navigation_menu 0;
- Coqide_ui.ui_m#insert_action_group tactics_menu 0;
Coqide_ui.ui_m#insert_action_group templates_menu 0;
Coqide_ui.ui_m#insert_action_group tools_menu 0;
Coqide_ui.ui_m#insert_action_group queries_menu 0;
@@ -1368,7 +1359,7 @@ let read_coqide_args argv =
|"-debug"::args ->
Minilib.debug := true;
Flags.debug := true;
- Backtrace.record_backtrace true;
+ Exninfo.record_backtrace true;
filter_coqtop coqtop project_files bindings_files ("-debug"::out) args
|"-coqtop-flags" :: flags :: args->
Coq.ideslave_coqtop_flags := Some flags;
diff --git a/ide/coqide_ui.ml b/ide/coqide_ui.ml
index f056af6703..f22821c6ea 100644
--- a/ide/coqide_ui.ml
+++ b/ide/coqide_ui.ml
@@ -36,7 +36,6 @@ let init () =
\n <menuitem action='Save' />\
\n <menuitem action='Save as' />\
\n <menuitem action='Save all' />\
-\n <menuitem action='Revert all buffers' />\
\n <menuitem action='Close buffer' />\
\n <menuitem action='Print...' />\
\n <menu action='Export to'>\
@@ -100,9 +99,6 @@ let init () =
\n <menuitem action='Previous' />\
\n <menuitem action='Next' />\
\n </menu>\
-\n <menu action='Tactics'>\
-\n %s\
-\n </menu>\
\n <menu action='Templates'>\
\n <menuitem action='Lemma' />\
\n <menuitem action='Theorem' />\
@@ -165,7 +161,6 @@ let init () =
\n</toolbar>\
\n</ui>"
(if Coq_config.gtk_platform <> `QUARTZ then "<menuitem action='Quit' />" else "")
- (Buffer.contents (list_items "Tactic" Coq_commands.tactics))
(Buffer.contents (list_items "Template" Coq_commands.commands))
(Buffer.contents (list_queries "User-Query" Preferences.user_queries#get))
in
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 7d92cff365..ae2301a0a7 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -360,7 +360,6 @@ let import_option_value = function
let export_option_state s = {
Interface.opt_sync = true;
Interface.opt_depr = s.Goptions.opt_depr;
- Interface.opt_name = s.Goptions.opt_name;
Interface.opt_value = export_option_value s.Goptions.opt_value;
}
diff --git a/ide/preferences.ml b/ide/preferences.ml
index d3cf08e90e..af1759b0bb 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -331,10 +331,6 @@ let modifier_for_navigation =
let modifier_for_templates =
new preference ~name:["modifier_for_templates"] ~init:"<Control><Shift>" ~repr:Repr.(string)
-let modifier_for_tactics =
- new preference ~name:["modifier_for_tactics"]
- ~init:(select_arch "<Control><Alt>" "<Control><Primary>") ~repr:Repr.(string)
-
let modifier_for_display =
new preference ~name:["modifier_for_display"]
~init:(select_arch "<Alt><Shift>" "<Primary><Shift>")~repr:Repr.(string)
@@ -347,7 +343,6 @@ let attach_modifiers_callback () =
(* To be done after the preferences are loaded *)
let _ = attach_modifiers modifier_for_navigation "<Actions>/Navigation/" in
let _ = attach_modifiers modifier_for_templates "<Actions>/Templates/" in
- let _ = attach_modifiers modifier_for_tactics "<Actions>/Tactics/" in
let _ = attach_modifiers modifier_for_display "<Actions>/View/" in
let _ = attach_modifiers modifier_for_queries "<Actions>/Queries/" in
()
@@ -951,9 +946,6 @@ let configure ?(apply=(fun () -> ())) parent =
(string_of_project_behavior read_project#get)
in
let project_file_name = pstring "Default name for project file" project_file_name in
- let modifier_for_tactics =
- pmodifiers "Global change of modifiers for Tactics Menu" modifier_for_tactics
- in
let modifier_for_templates =
pmodifiers "Global change of modifiers for Templates Menu" modifier_for_templates
in
@@ -1056,7 +1048,7 @@ let configure ?(apply=(fun () -> ())) parent =
[cmd_coqtop;cmd_coqc;cmd_make;cmd_coqmakefile; cmd_coqdoc;
cmd_print;cmd_editor;cmd_browse]);
Section("Shortcuts", Some `PREFERENCES,
- [modifiers_valid; modifier_for_tactics;
+ [modifiers_valid;
modifier_for_templates; modifier_for_display; modifier_for_navigation;
modifier_for_queries (*; user_queries *)]);
Section("Misc", Some `ADD,
diff --git a/ide/preferences.mli b/ide/preferences.mli
index 7b43079b4f..754f15c575 100644
--- a/ide/preferences.mli
+++ b/ide/preferences.mli
@@ -71,7 +71,6 @@ val automatic_tactics : string list preference
val cmd_print : string preference
val modifier_for_navigation : string preference
val modifier_for_templates : string preference
-val modifier_for_tactics : string preference
val modifier_for_display : string preference
val modifier_for_queries : string preference
val modifiers_valid : string preference
diff --git a/ide/protocol/interface.ml b/ide/protocol/interface.ml
index 362833743e..be5e305ad3 100644
--- a/ide/protocol/interface.ml
+++ b/ide/protocol/interface.ml
@@ -71,8 +71,6 @@ type option_state = {
(** Whether an option is synchronous *)
opt_depr : bool;
(** Whether an option is deprecated *)
- opt_name : string;
- (** A short string that is displayed when using [Test] *)
opt_value : option_value;
(** The current value of the option *)
}
diff --git a/ide/protocol/xmlprotocol.ml b/ide/protocol/xmlprotocol.ml
index cad65cc5d6..a2c80ea118 100644
--- a/ide/protocol/xmlprotocol.ml
+++ b/ide/protocol/xmlprotocol.ml
@@ -79,13 +79,11 @@ let of_option_state s =
Element ("option_state", [], [
of_bool s.opt_sync;
of_bool s.opt_depr;
- of_string s.opt_name;
of_option_value s.opt_value])
let to_option_state = function
- | Element ("option_state", [], [sync; depr; name; value]) -> {
+ | Element ("option_state", [], [sync; depr; value]) -> {
opt_sync = to_bool sync;
opt_depr = to_bool depr;
- opt_name = to_string name;
opt_value = to_option_value value }
| x -> raise (Marshal_error("option_state",x))
@@ -429,8 +427,8 @@ end = struct
| StringOptValue (Some s) -> s
| BoolValue b -> if b then "true" else "false"
let pr_option_state (s : option_state) =
- Printf.sprintf "sync := %b; depr := %b; name := %s; value := %s\n"
- s.opt_sync s.opt_depr s.opt_name (pr_option_value s.opt_value)
+ Printf.sprintf "sync := %b; depr := %b; value := %s\n"
+ s.opt_sync s.opt_depr (pr_option_value s.opt_value)
let pr_list pr l = "["^String.concat ";" (List.map pr l)^"]"
let pr_option pr = function None -> "None" | Some x -> "Some("^pr x^")"
let pr_coq_object (o : 'a coq_object) = "FIXME"
@@ -513,7 +511,7 @@ end = struct
"type which contains a flattened n-tuple. We provide one example.\n");
Printf.printf "%s:\n\n%s\n\n" (print_val_t Option_state)
(pr_xml (of_option_state { opt_sync = true; opt_depr = false;
- opt_name = "name1"; opt_value = IntValue (Some 37) }));
+ opt_value = IntValue (Some 37) }));
end
open ReifType
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 23:02:02 +0000