diff options
| -rw-r--r-- | ide/command_windows.ml | 9 | ||||
| -rw-r--r-- | ide/coq_commands.ml | 52 | ||||
| -rw-r--r-- | ide/coqide.ml | 12 |
3 files changed, 40 insertions, 33 deletions
diff --git a/ide/command_windows.ml b/ide/command_windows.ml index 444495ee1..0d1b9fa75 100644 --- a/ide/command_windows.ml +++ b/ide/command_windows.ml @@ -147,10 +147,15 @@ object(self) result#misc#set_can_focus true; (* false causes problems for selection *) result#set_editable false; let callback () = - let phrase = combo#entry#text ^ " " ^ entry#text ^" . " in + let com = combo#entry#text in + let phrase = + if String.get com (String.length com - 1) = '.' + then com ^ " " else com ^ " " ^ entry#text ^" . " + in try ignore(Coq.interp phrase); - result#buffer#set_text (Ideutils.read_stdout ()) + result#buffer#set_text + ("Result for command " ^ phrase ^ ":\n" ^ Ideutils.read_stdout ()) with e -> let (s,loc) = Coq.process_exn e in assert (Glib.Utf8.validate s); diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index 190702581..aefae8fbb 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -10,8 +10,8 @@ let commands = [ [(* "Abort"; *) - "Add Abstract Ring"; - "Add Abstract Semi Ring"; + "Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T."; + "Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T."; "Add Field"; "Add LoadPath"; "Add ML Path"; @@ -20,15 +20,13 @@ let commands = [ "Add Printing Let"; "Add Rec LoadPath"; "Add Rec ML Path"; - "Add Ring"; - "Add Semi Ring"; - "Add Semi Ring"; + "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. "; + "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ]."; "Add Setoid"; "Axiom";]; - ["Back"; - "Begin Silent";]; + [(* "Back"; *) ]; ["Canonical Structure"; - "Cd"; + (* "Cd"; *) "Chapter"; (* "Check"; *) "Coercion"; @@ -37,7 +35,7 @@ let commands = [ "CoInductive"; (* "Correctness"; *)]; ["Declare ML Module"; - "Defined"; + "Defined."; "Definition"; "Derive Dependent Inversion"; "Derive Dependent Inversion_clear"; @@ -45,9 +43,8 @@ let commands = [ "Derive Inversion_clear"; (* "Drop"; *)]; ["End"; - "End Silent"; + "End Silent."; "Eval"; - "Explicitation of implicit arguments"; "Extract Constant"; "Extract Inductive"; "Extraction"; @@ -64,29 +61,27 @@ let commands = [ ["Hint"; "Hint Constructors"; "Hint Unfold"; - "Hint"; "Hint Rewrite"; "Hints Extern"; "Hints Immediate"; "Hints Resolve"; - "Hints Immediate"; - "Hints Resolve"; "Hints Unfold"; "Hypothesis";]; ["Identity Coercion"; - "Implicit Arguments Off"; - "Implicit Arguments On"; + "Implicit Arguments Off."; + "Implicit Arguments On."; "Implicits"; "Inductive"; "Infix"; - "Inspect";]; + (* "Inspect"; *)]; ["Lemma"; "Load"; "Load Verbose"; "Local"; - "Locate"; + (* + "Locate"; "Locate File"; - "Locate Library";]; + "Locate Library"; *)]; ["Module"; "Module Type"; "Mutual Inductive";]; @@ -112,9 +107,9 @@ let commands = [ "Print Section"; "Print Table Printing If"; "Print Table Printing Let";*) - "Proof"; + "Proof."; (*"Pwd";*)]; - ["Qed"; + ["Qed."; (* "Quit";*)]; ["Read Module"; "Record"; @@ -130,9 +125,9 @@ let commands = [ "Reset Extraction Inline"; (* "Reset Initial"; *) (* "Restart"; *) - "Restore State"; - "Resume";]; - [ "Save"; + "Restore State"; + (* "Resume"; *)]; + [ "Save."; "Scheme"; (*"Search"; "Search ... inside ..."; @@ -153,6 +148,7 @@ let commands = [ "Set Printing Coercions"; "Set Printing Synth"; "Set Printing Wildcard"; + "Set Silent."; "Set Undo"; (*"Show"; "Show Conjectures"; @@ -185,6 +181,7 @@ let commands = [ "Unset Printing Coercions"; "Unset Printing Synth"; "Unset Printing Wildcard"; + "Unset Silent."; "Unset Undo";]; ["Variable"; "Variables";]; @@ -194,13 +191,14 @@ let commands = [ let state_preserving = [ "Check"; "Eval"; + "Eval compute in"; "Extraction"; "Extraction Library"; "Extraction Module"; "Inspect"; "Locate"; "Print"; - "Print All"; + "Print All."; "Print Classes"; "Print Coercion Paths"; "Print Coercions"; @@ -219,7 +217,7 @@ let state_preserving = [ "Print Table Printing If"; "Print Table Printing Let"; - "Pwd"; + "Pwd."; "Recursive Extraction"; "Recursive Extraction Library"; @@ -242,6 +240,4 @@ let state_preserving = [ "Test Printing Let"; "Test Printing Synth"; "Test Printing Wildcard"; - - "Recursive Extraction"; ] diff --git a/ide/coqide.ml b/ide/coqide.ml index 508193337..dcb3228fb 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2429,6 +2429,12 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); let add_simple_template (factory: GMenu.menu GMenu.factory) (menu_text, text) = + let text = + let l = String.length text - 1 in + if String.get text l = '.' + then text ^"\n" + else text ^" " + in ignore (factory#add_item menu_text ~callback: (do_if_not_computing @@ -2453,9 +2459,9 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); List.iter (fun l -> match l with - |[s] -> add_simple_template templates_factory ("_"^s, s^" ") | [] -> () - | s::r -> + | [s] -> add_simple_template templates_factory ("_"^s, s) + | s::_ -> let a = "_@..." in a.[1] <- s.[0]; let f = templates_factory#add_submenu a in @@ -2467,7 +2473,7 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S); ((String.sub x 0 1)^ "_"^ (String.sub x 1 (String.length x - 1)), - x^" ")) + x)) l ) Coq_commands.commands; |