diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 1 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 10 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 3 | ||||
| -rw-r--r-- | toplevel/search.ml | 31 | ||||
| -rw-r--r-- | toplevel/search.mli | 35 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 57 |
7 files changed, 70 insertions, 69 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 7065bd265..b4e44e7d3 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -305,7 +305,6 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props else if Flags.is_auto_intros () then Pfedit.by (Refiner.tclDO len Tactics.intro); (match tac with Some tac -> Pfedit.by tac | None -> ())) (); - Flags.if_verbose (msg $$ Printer.pr_open_subgoals) (); id) end) diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index 2256d1b1d..e13b80dc7 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -296,18 +296,16 @@ let cache_ml_module_object (_,{mnames=mnames}) = if not (module_is_known mname) then if has_dynlink then let fname = file_of_name mname in + let info = str"[Loading ML file " ++ str fname ++ str" ..." in try - if_verbose - msg (str"[Loading ML file " ++ str fname ++ str" ..."); load_ml_object mname fname; - if_verbose msgnl (str" done]"); + if_verbose msgnl (info ++ str" done]"); add_loaded_module mname with e -> - if_verbose msgnl (str" failed]"); + if_verbose msgnl (info ++ str" failed]"); raise e else - (if_verbose msgnl (str" failed]"); - error ("Dynamic link not supported (module "^name^")")) + error ("Dynamic link not supported (module "^name^")") else init_ml_object mname) mnames diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 61cc6b348..5f07001ca 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -801,8 +801,7 @@ let rec solve_obligation prg num tac = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Printer.pr_constr_env (Global.env ()) obl.obl_type); Pfedit.by (snd (get_default_tactic ())); - Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac; - Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () + Option.iter (fun tac -> Pfedit.set_end_tac (Tacinterp.interp tac)) tac | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) diff --git a/toplevel/search.ml b/toplevel/search.ml index e5b2ffbaf..fbfa83d08 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -24,6 +24,9 @@ open Libnames open Globnames open Nametab +type filter_function = global_reference -> env -> constr -> bool +type display_function = global_reference -> env -> constr -> unit + module SearchBlacklist = Goptions.MakeStringTable (struct @@ -107,10 +110,10 @@ let rec head c = let xor a b = (a or b) & (not (a & b)) -let plain_display ref a c = +let plain_display accu ref a c = let pc = pr_lconstr_env a c in let pr = pr_global ref in - msg (hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl ()) + accu := !accu ++ hov 2 (pr ++ str":" ++ spc () ++ pc) ++ fnl () let filter_by_module (module_list:dir_path list) (accept:bool) (ref:global_reference) _ _ = @@ -193,14 +196,20 @@ let raw_search search_function extra_filter display_function pat = display_function gr env typ ) (search_function pat) -let text_pattern_search extra_filter = - raw_search Libtypes.search_concl extra_filter plain_display +let text_pattern_search extra_filter pat = + let ans = ref (mt ()) in + raw_search Libtypes.search_concl extra_filter (plain_display ans) pat; + !ans -let text_search_rewrite extra_filter = - raw_search (Libtypes.search_eq_concl c_eq) extra_filter plain_display +let text_search_rewrite extra_filter pat = + let ans = ref (mt ()) in + raw_search (Libtypes.search_eq_concl c_eq) extra_filter (plain_display ans) pat; + !ans -let text_search_by_head extra_filter = - raw_search Libtypes.search_head_concl extra_filter plain_display +let text_search_by_head extra_filter pat = + let ans = ref (mt ()) in + raw_search Libtypes.search_head_concl extra_filter (plain_display ans) pat; + !ans let filter_by_module_from_list = function | [], _ -> (fun _ _ _ -> true) @@ -244,5 +253,7 @@ let raw_search_about filter_modules display_function l = in gen_filtered_search filter display_function -let search_about ref inout = - raw_search_about (filter_by_module_from_list inout) plain_display ref +let search_about reference inout = + let ans = ref (mt ()) in + raw_search_about (filter_by_module_from_list inout) (plain_display ans) reference; + !ans diff --git a/toplevel/search.mli b/toplevel/search.mli index d248a9faa..daca39f66 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -20,33 +20,28 @@ type glob_search_about_item = | GlobSearchSubPattern of constr_pattern | GlobSearchString of string -val search_by_head : constr -> dir_path list * bool -> unit -val search_rewrite : constr -> dir_path list * bool -> unit -val search_pattern : constr -> dir_path list * bool -> unit +type filter_function = global_reference -> env -> constr -> bool +type display_function = global_reference -> env -> constr -> unit + +val search_by_head : constr -> dir_path list * bool -> std_ppcmds +val search_rewrite : constr -> dir_path list * bool -> std_ppcmds +val search_pattern : constr -> dir_path list * bool -> std_ppcmds val search_about : - (bool * glob_search_about_item) list -> dir_path list * bool -> unit + (bool * glob_search_about_item) list -> dir_path list * bool -> std_ppcmds (** The filtering function that is by standard search facilities. It can be passed as argument to the raw search functions. It is used in pcoq. *) -val filter_by_module_from_list : - dir_path list * bool -> global_reference -> env -> 'a -> bool +val filter_by_module_from_list : dir_path list * bool -> filter_function -val filter_blacklist : global_reference -> env -> constr -> bool +val filter_blacklist : filter_function (** raw search functions can be used for various extensions. They are also used for pcoq. *) -val gen_filtered_search : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> unit -val filtered_search : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> global_reference -> unit -val raw_pattern_search : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr_pattern -> unit -val raw_search_rewrite : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr_pattern -> unit -val raw_search_about : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> - (bool * glob_search_about_item) list -> unit -val raw_search_by_head : (global_reference -> env -> constr -> bool) -> - (global_reference -> env -> constr -> unit) -> constr_pattern -> unit +val gen_filtered_search : filter_function -> display_function -> unit +val filtered_search : filter_function -> display_function -> global_reference -> unit +val raw_pattern_search : filter_function -> display_function -> constr_pattern -> unit +val raw_search_rewrite : filter_function -> display_function -> constr_pattern -> unit +val raw_search_about : filter_function -> display_function -> (bool * glob_search_about_item) list -> unit +val raw_search_by_head : filter_function -> display_function -> constr_pattern -> unit diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 8aaa82a3b..6d37e0d78 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -192,7 +192,7 @@ let pr_new_syntax loc ocom = | Some com -> pr_vernac com | None -> mt() in if !beautify_file then - msg (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) + pp (hov 0 (comment (fst loc) ++ com ++ comment (snd loc))) else msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com))); States.unfreeze fs; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index dd8f1cd0e..db3877dff 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -91,8 +91,7 @@ let show_top_evars () = let pfts = get_pftreestate () in let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in - msg (pr_evars_int 1 (Evarutil.non_instantiated sigma)) - + msg_info (pr_evars_int 1 (Evarutil.non_instantiated sigma)) let show_prooftree () = (* Spiwack: proof tree is currently not working *) @@ -102,7 +101,7 @@ let enable_goal_printing = ref true let print_subgoals () = if !enable_goal_printing && is_verbose () - then msg (pr_open_subgoals ()) + then msg_info (pr_open_subgoals ()) let try_print_subgoals () = Pp.flush_all(); @@ -164,7 +163,7 @@ let show_match id = let pr_branch l = str "| " ++ hov 1 (prlist_with_sep spc str l) ++ str " =>" in - msg (v 1 (str "match # with" ++ fnl () ++ + msg_info (v 1 (str "match # with" ++ fnl () ++ prlist_with_sep fnl pr_branch patterns ++ fnl ())) (* "Print" commands *) @@ -380,7 +379,7 @@ let vernac_end_proof = function admit () | Proved (is_opaque,idopt) -> let prf = Pfedit.get_current_proof_name () in - if is_verbose () && !qed_display_script then (show_script (); msg (fnl())); + if is_verbose () && !qed_display_script then show_script (); begin match idopt with | None -> save_named is_opaque | Some ((_,id),None) -> save_anonymous is_opaque id @@ -1204,13 +1203,13 @@ let vernac_check_may_eval redexp glopt rc = match redexp with | None -> if !pcoq <> None then (Option.get !pcoq).print_check env j - else msg (print_judgment env j) + else msg_info (print_judgment env j) | Some r -> let (sigma',r_interp) = interp_redexp env sigma' r in let redfun = fst (reduction_of_red_expr r_interp) in if !pcoq <> None then (Option.get !pcoq).print_eval redfun env sigma' rc j - else msg (print_eval redfun env sigma' rc j) + else msg_info (print_eval redfun env sigma' rc j) let vernac_declare_reduction locality s r = declare_red_expr locality s (snd (interp_redexp (Global.env()) Evd.empty r)) @@ -1222,23 +1221,23 @@ let vernac_global_check c = let c = interp_constr evmap env c in let senv = Global.safe_env() in let j = Safe_typing.typing senv c in - msg (print_safe_judgment env j) + msg_info (print_safe_judgment env j) let vernac_print = function - | PrintTables -> print_tables () - | PrintFullContext-> msg (print_full_context_typ ()) - | PrintSectionContext qid -> msg (print_sec_context_typ qid) - | PrintInspect n -> msg (inspect n) + | PrintTables -> msg_info (print_tables ()) + | PrintFullContext-> msg_info (print_full_context_typ ()) + | PrintSectionContext qid -> msg_info (print_sec_context_typ qid) + | PrintInspect n -> msg_info (inspect n) | PrintGrammar ent -> Metasyntax.print_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir - | PrintModules -> msg (print_modules ()) + | PrintModules -> msg_info (print_modules ()) | PrintModule qid -> print_module qid | PrintModuleType qid -> print_modtype qid | PrintMLLoadPath -> Mltop.print_ml_path () | PrintMLModules -> Mltop.print_ml_modules () | PrintName qid -> if !pcoq <> None then (Option.get !pcoq).print_name qid - else msg (print_name qid) + else msg_info (print_name qid) | PrintGraph -> ppnl (Prettyp.print_graph()) | PrintClasses -> ppnl (Prettyp.print_classes()) | PrintTypeClasses -> ppnl (Prettyp.print_typeclasses()) @@ -1253,25 +1252,25 @@ let vernac_print = function let univ = if b then Univ.sort_universes univ else univ in pp (Univ.pr_universes univ) | PrintUniverses (b, Some s) -> dump_universes b s - | PrintHint r -> Auto.print_hint_ref (smart_global r) - | PrintHintGoal -> Auto.print_applicable_hint () - | PrintHintDbName s -> Auto.print_hint_db_by_name s + | PrintHint r -> msg_info (Auto.pr_hint_ref (smart_global r)) + | PrintHintGoal -> msg_info (Auto.pr_applicable_hint ()) + | PrintHintDbName s -> msg_info (Auto.pr_hint_db_by_name s) | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s - | PrintHintDb -> Auto.print_searchtable () + | PrintHintDb -> msg_info (Auto.pr_searchtable ()) | PrintScopes -> pp (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr)) | PrintScope s -> pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s) | PrintVisibility s -> pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s) - | PrintAbout qid -> msg (print_about qid) - | PrintImplicit qid -> msg (print_impargs qid) + | PrintAbout qid -> msg_info (print_about qid) + | PrintImplicit qid -> msg_info (print_impargs qid) | PrintAssumptions (o,r) -> (* Prints all the axioms and section variables used by a term *) let cstr = constr_of_global (smart_global r) in let st = Conv_oracle.get_transp_state () in let nassums = Assumptions.assumptions st ~add_opaque:o cstr in - msg (Printer.pr_assumptionset (Global.env ()) nassums) + msg_info (Printer.pr_assumptionset (Global.env ()) nassums) let global_module r = let (loc,qid) = qualid_of_reference r in @@ -1310,15 +1309,15 @@ let vernac_search s r = match s with | SearchPattern c -> let (_,c) = interp_open_constr_patvar Evd.empty (Global.env()) c in - Search.search_pattern c r + msg_info (Search.search_pattern c r) | SearchRewrite c -> let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in - Search.search_rewrite pat r + msg_info (Search.search_rewrite pat r) | SearchHead c -> let _,pat = interp_open_constr_patvar Evd.empty (Global.env()) c in - Search.search_by_head pat r + msg_info (Search.search_by_head pat r) | SearchAbout sl -> - Search.search_about (List.map (on_snd interp_search_about_item) sl) r + msg_info (Search.search_about (List.map (on_snd interp_search_about_item) sl) r) let vernac_locate = function | LocateTerm (AN qid) -> msgnl (print_located_qualid qid) @@ -1420,7 +1419,7 @@ let vernac_unfocus () = let vernac_unfocused () = let p = Proof_global.give_me_the_proof () in if Proof.unfocused p then - msg (str"The proof is indeed fully unfocused.") + msg_info (str"The proof is indeed fully unfocused.") else error "The proof is not fully unfocused." @@ -1458,14 +1457,14 @@ let vernac_bullet (bullet:Proof_global.Bullet.t) = let vernac_show = function | ShowGoal goalref -> if !pcoq <> None then (Option.get !pcoq).show_goal goalref - else msg (match goalref with + else msg_info (match goalref with | OpenSubgoals -> pr_open_subgoals () | NthGoal n -> pr_nth_open_subgoal n | GoalId id -> pr_goal_by_id id) | ShowGoalImplicitly None -> - Constrextern.with_implicits msg (pr_open_subgoals ()) + Constrextern.with_implicits msg_info (pr_open_subgoals ()) | ShowGoalImplicitly (Some n) -> - Constrextern.with_implicits msg (pr_nth_open_subgoal n) + Constrextern.with_implicits msg_info (pr_nth_open_subgoal n) | ShowProof -> show_proof () | ShowNode -> show_node () | ShowScript -> show_script () |