diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | ide/coq.ml | 100 | ||||
| -rw-r--r-- | ide/coq.mli | 12 | ||||
| -rw-r--r-- | ide/coq_commands.ml | 2 | ||||
| -rw-r--r-- | ide/coqide.ml | 66 | ||||
| -rw-r--r-- | ide/highlight.mll | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
7 files changed, 180 insertions, 16 deletions
@@ -34,7 +34,9 @@ Vernacular commands - Added option "Set Equality Scheme" to make automatic the declaration of the boolean equality when possible. - Source of universe inconsistencies now printed when option - "Set Printing Universes" is activated, + "Set Printing Universes" is activated. +- New option "Set Printing Existential Instances" for making the display of + existential variable instances explicit. - Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the "compute"/"cbv" reduction strategy, respectively meaning reduce only, or everything but, the constants id1 ... idn. "lazy" alone or followed by @@ -283,6 +285,7 @@ Tools - CoqIDE font defaults to monospace so as indentation to be meaningful. - CoqIDE supports Definition/Parameter/Inductive in middle of a proof. - Undoing non-tactic commands in CoqIDE works faster. +- New CoqIDE buttons for activating display of various implicit informations. Miscellaneous diff --git a/ide/coq.ml b/ide/coq.ml index 17f80b0ec..0022eeb92 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -110,8 +110,74 @@ let is_in_proof_mode () = let user_error_loc l s = raise (Stdpp.Exc_located (l, Util.UserError ("CoqIde", s))) +type printing_state = { + mutable printing_implicit : bool; + mutable printing_coercions : bool; + mutable printing_raw_matching : bool; + mutable printing_no_notation : bool; + mutable printing_all : bool; + mutable printing_evar_instances : bool; + mutable printing_universes : bool +} + +let printing_state = { + printing_implicit = false; + printing_coercions = false; + printing_raw_matching = false; + printing_no_notation = false; + printing_all = false; + printing_evar_instances = false; + printing_universes = false; +} + +let printing_implicit_data = ["Printing";"Implicit"], false +let printing_coercions_data = ["Printing";"Coercions"], false +let printing_raw_matching_data = ["Printing";"Matching"], true +let printing_no_synth_data = ["Printing";"Synth"], true +let printing_no_notation_data = ["Printing";"Notations"], true +let printing_all_data = ["Printing";"All"], false +let printing_evar_instances_data = ["Printing";"Existential";"Instances"],false +let printing_universes_data = ["Printing";"Universes"], false + +let known_options = ref [] + +let prepare_option (l,dft) = + known_options := l :: !known_options; + let set = (String.concat " " ("Set"::l)) ^ "." in + let unset = (String.concat " " ("Unset"::l)) ^ "." in + if dft then unset,set else set,unset + +let coqide_known_option = function + | Goptions.TertiaryTable (a,b,c) -> List.mem [a;b;c] !known_options + | Goptions.SecondaryTable (a,b) -> List.mem [a;b] !known_options + | Goptions.PrimaryTable a -> List.mem [a] !known_options + +let with_printing_implicit = prepare_option printing_implicit_data +let with_printing_coercions = prepare_option printing_coercions_data +let with_printing_raw_matching = prepare_option printing_raw_matching_data +let with_printing_no_synth = prepare_option printing_no_synth_data +let with_printing_no_notation = prepare_option printing_no_notation_data +let with_printing_all = prepare_option printing_all_data +let with_printing_evar_instances = prepare_option printing_evar_instances_data +let with_printing_universes = prepare_option printing_universes_data + +let make_option_commands () = + let p = printing_state in + (if p.printing_implicit then [with_printing_implicit] else [])@ + (if p.printing_coercions then [with_printing_coercions] else [])@ + (if p.printing_raw_matching then [with_printing_raw_matching;with_printing_no_synth] else [])@ + (if p.printing_no_notation then [with_printing_no_notation] else [])@ + (if p.printing_all then [with_printing_all] else [])@ + (if p.printing_evar_instances then [with_printing_evar_instances] else [])@ + (if p.printing_universes then [with_printing_universes] else []) + +let make_option_commands () = + let l = make_option_commands () in + List.iter (fun (a,b) -> prerr_endline a; prerr_endline b) l; + l + type command_attribute = - NavigationCommand | QueryCommand | DebugCommand + NavigationCommand | QueryCommand | DebugCommand | KnownOptionCommand | OtherStatePreservingCommand | GoalStartingCommand | SolveCommand let rec attribute_of_vernac_command = function @@ -203,8 +269,9 @@ let rec attribute_of_vernac_command = function | VernacSetOpacity _ -> [] | VernacSetOption (Goptions.SecondaryTable ("Ltac","Debug"), _) -> [DebugCommand] + | VernacSetOption (o,BoolValue true) | VernacUnsetOption o -> + if coqide_known_option o then [KnownOptionCommand] else [] | VernacSetOption _ -> [] - | VernacUnsetOption _ -> [] | VernacRemoveOption _ -> [] | VernacAddOption _ -> [] | VernacMemOption _ -> [QueryCommand] @@ -255,6 +322,9 @@ let is_vernac_navigation_command com = let is_vernac_query_command com = List.mem QueryCommand (attribute_of_vernac_command com) +let is_vernac_known_option_command com = + List.mem KnownOptionCommand (attribute_of_vernac_command com) + let is_vernac_debug_command com = List.mem DebugCommand (attribute_of_vernac_command com) @@ -315,14 +385,18 @@ let reset_to = function prerr_endline ("Reset called with "^(string_of_id id)); Vernacentries.abort_refine Lib.reset_name (Util.dummy_loc,id) | ResetToState sp -> + prerr_endline + ("Reset called with state "^(Libnames.string_of_path (fst sp))); Vernacentries.abort_refine Lib.reset_to_state sp let reset_to_mod id = prerr_endline ("Reset called to Mod/Sect with "^(string_of_id id)); Vernacentries.abort_refine Lib.reset_mod (Util.dummy_loc,id) +let raw_interp s = + Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)) -let interp verbosely s = +let interp_with_options verbosely options s = prerr_endline "Starting interp..."; prerr_endline s; let pa = Pcoq.Gram.parsable (Stream.of_string s) in @@ -336,6 +410,8 @@ let interp verbosely s = user_error_loc loc (str "Debug mode not available within CoqIDE"); if is_vernac_navigation_command vernac then user_error_loc loc (str "Use CoqIDE navigation instead"); + if is_vernac_known_option_command vernac then + user_error_loc loc (str "Use CoqIDE buttons instead"); if is_vernac_query_command vernac then !flash_info "Warning: query commands should not be inserted in scripts"; @@ -343,11 +419,16 @@ let interp verbosely s = (* Verbose if in small step forward and not a tactic *) Flags.make_silent (not verbosely); let reset_info = compute_reset_info vernac in - Vernac.raw_do_vernac (Pcoq.Gram.parsable (Stream.of_string s)); + List.iter (fun (set_option,_) -> raw_interp set_option) options; + raw_interp s; Flags.make_silent true; + List.iter (fun (_,unset_option) -> raw_interp unset_option) options; prerr_endline ("...Done with interp of : "^s); reset_info,last +let interp verbosely phrase = + interp_with_options verbosely (make_option_commands ()) phrase + let interp_and_replace s = let result = interp false s in let msg = read_stdout () in @@ -447,11 +528,18 @@ let prepare_hyps sigma env = in List.rev hyps -let prepare_goal sigma g = +let prepare_goal_main sigma g = let env = evar_env g in (prepare_hyps sigma env, (env, sigma, g.evar_concl, msg (pr_ltype_env_at_top env g.evar_concl))) +let prepare_goal sigma g = + let options = make_option_commands () in + List.iter (fun (set_option,_) -> raw_interp set_option) options; + let x = prepare_goal_main sigma g in + List.iter (fun (_,unset_option) -> raw_interp unset_option) options; + x + let get_current_pm_goal () = let pfts = get_pftreestate () in let gls = try nth_goal_of_pftreestate 1 pfts with _ -> raise Not_found in @@ -588,5 +676,3 @@ let current_status () = try path ^ ", proving " ^ (Names.string_of_id (Pfedit.get_current_proof_name ())) with _ -> path - - diff --git a/ide/coq.mli b/ide/coq.mli index 5ded2b573..cbc763df8 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -15,6 +15,18 @@ open Evd val version : unit -> string +type printing_state = { + mutable printing_implicit : bool; + mutable printing_coercions : bool; + mutable printing_raw_matching : bool; + mutable printing_no_notation : bool; + mutable printing_all : bool; + mutable printing_evar_instances : bool; + mutable printing_universes : bool +} + +val printing_state : printing_state + type reset_mark = | ResetToId of Names.identifier | ResetToState of Libnames.object_name diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml index a8edc4061..fdaee4508 100644 --- a/ide/coq_commands.ml +++ b/ide/coq_commands.ml @@ -156,6 +156,8 @@ let commands = [ let state_preserving = [ "Check"; "Eval"; + "Eval lazy in"; + "Eval vm_compute in"; "Eval compute in"; "Extraction"; "Extraction Library"; diff --git a/ide/coqide.ml b/ide/coqide.ml index 4e5223b02..856880eb7 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -16,7 +16,7 @@ open Ideutils let cb_ = ref None let cb () = ((Option.get !cb_):GData.clipboard) let last_cb_content = ref "" - + let (message_view:GText.view option ref) = ref None let (proof_view:GText.view option ref) = ref None @@ -1422,7 +1422,7 @@ Please restart and report NOW."; | {reset_info=ResetAtFrozenState (sp, {contents=true})} -> ignore (pop ()); - Lib.reset_to_state sp; + reset_to (ResetToState sp); sync update_input () | {reset_info=ResetAtSegmentStart (id, {contents=true})} -> ignore (pop ()); @@ -1865,7 +1865,7 @@ let main files = (* Toolbar *) let toolbar = GButton.toolbar ~orientation:`HORIZONTAL - ~style:`ICONS + ~style:`BOTH ~tooltips:true ~packing:(* handle#add *) (vbox#pack ~expand:false ~fill:false) @@ -2535,7 +2535,7 @@ let main files = end; ignore (toolbar#insert_button ~tooltip - ~text:tooltip +(* ~text:tooltip*) ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR icon) ~callback ()) @@ -2583,8 +2583,7 @@ let main files = ~tooltip:"Interrupt computations" ~key:GdkKeysyms._Break ~callback:break - `STOP - ; + `STOP; (* Tactics Menu *) let tactics_menu = factory#add_submenu "_Try Tactics" in @@ -2658,6 +2657,59 @@ let main files = ); + ignore (toolbar#insert_space ()); + + ignore (toolbar#insert_toggle_button + ~tooltip:"Toggle printing of implicit arguments" + ~text:"Impl" + ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) + ~callback:(fun () -> printing_state.printing_implicit <- not printing_state.printing_implicit; do_or_activate (fun a -> a#show_goals) ()) + ()); + + ignore (toolbar#insert_toggle_button + ~tooltip:"Toggle printing of coercions" + ~text:"Coer" + ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) + ~callback:(fun () -> printing_state.printing_coercions <- not printing_state.printing_coercions; do_or_activate (fun a -> a#show_goals) ()) + ()); + + ignore (toolbar#insert_toggle_button + ~tooltip:"Toggle printing of raw matching expressions" + ~text:"Match" + ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) + ~callback:(fun () -> printing_state.printing_raw_matching <- not printing_state.printing_raw_matching; do_or_activate (fun a -> a#show_goals) ()) + ()); + + ignore (toolbar#insert_toggle_button + ~tooltip:"Toggle deactivation of notations" + ~text:"Nota" + ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) + ~callback:(fun () -> printing_state.printing_no_notation <- not printing_state.printing_no_notation; do_or_activate (fun a -> a#show_goals) ()) + ()); + + ignore (toolbar#insert_toggle_button + ~tooltip:"Toggle full low-level printing" + ~text:"All" + ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) + ~callback:(fun () -> printing_state.printing_all <- not printing_state.printing_all; do_or_activate (fun a -> a#show_goals) ()) + ()); + + ignore (toolbar#insert_toggle_button + ~tooltip:"Toggle printing of existential variable instances" + ~text:"Evars" + ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) + ~callback:(fun () -> printing_state.printing_evar_instances <- not printing_state.printing_evar_instances; do_or_activate (fun a -> a#show_goals) ()) + ()); + + ignore (toolbar#insert_toggle_button + ~tooltip:"Toggle printing of universe levels" + ~text:"Univ" + ~icon:(stock_to_widget ~size:`LARGE_TOOLBAR `DIALOG_WARNING) + ~callback:(fun () -> printing_state.printing_universes <- not printing_state.printing_universes; do_or_activate (fun a -> a#show_goals) ()) + ()); + + ignore (toolbar#insert_space ()); + ignore (toolbar#insert_button ~tooltip:"Proof Wizard" ~text:"Wizard" @@ -2667,6 +2719,8 @@ let main files = )) ()); + + ignore (tactics_factory#add_item "<Proof _Wizard>" ~key:GdkKeysyms._dollar ~callback:(do_if_active (fun a -> a#tactic_wizard diff --git a/ide/highlight.mll b/ide/highlight.mll index cbbaa112e..c01ec1a81 100644 --- a/ide/highlight.mll +++ b/ide/highlight.mll @@ -24,7 +24,7 @@ let h = Hashtbl.create 97 in List.iter (fun s -> Hashtbl.add h s ()) [ "Add" ; "Check"; "Eval"; "Extraction" ; - "Load" ; "Undo"; + "Load" ; "Undo"; "Goal"; "Proof" ; "Print"; "Qed" ; "Defined" ; "Save" ; "End" ; "Section"; "Chapter"; "Transparent"; "Opaque"; "Comments" ]; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8c92329e5..49690256c 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -773,6 +773,13 @@ let _ = let _ = declare_bool_option { optsync = true; + optname = "printing of existential variable instances"; + optkey = (TertiaryTable ("Printing","Existential","Instances")); + optread = (fun () -> !Constrextern.print_evar_arguments); + optwrite = (:=) Constrextern.print_evar_arguments } +let _ = + declare_bool_option + { optsync = true; optname = "implicit arguments printing"; optkey = (SecondaryTable ("Printing","Implicit")); optread = (fun () -> !Constrextern.print_implicits); @@ -870,7 +877,7 @@ let _ = declare_bool_option { optsync=true; optkey=SecondaryTable("Printing","Universes"); - optname="the printing of universes"; + optname="printing of universes"; optread=(fun () -> !Constrextern.print_universes); optwrite=(fun b -> Constrextern.print_universes:=b) } |