diff options
-rw-r--r-- | checker/check.ml | 5 | ||||
-rw-r--r-- | dev/top_printers.ml | 2 | ||||
-rw-r--r-- | lib/pp.ml4 | 1 | ||||
-rw-r--r-- | lib/pp.mli | 20 | ||||
-rw-r--r-- | library/goptions.ml | 53 | ||||
-rw-r--r-- | library/goptions.mli | 2 | ||||
-rw-r--r-- | plugins/cc/ccalgo.ml | 17 | ||||
-rw-r--r-- | plugins/extraction/g_extraction.ml4 | 2 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 1 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 2 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 | ||||
-rw-r--r-- | plugins/funind/invfun.ml | 4 | ||||
-rw-r--r-- | plugins/rtauto/proof_search.ml | 2 | ||||
-rw-r--r-- | plugins/rtauto/proof_search.mli | 2 | ||||
-rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 | ||||
-rw-r--r-- | proofs/refiner.ml | 2 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 6 | ||||
-rw-r--r-- | tactics/auto.ml | 67 | ||||
-rw-r--r-- | tactics/auto.mli | 15 | ||||
-rw-r--r-- | tactics/extratactics.ml4 | 3 | ||||
-rw-r--r-- | tactics/rewrite.ml4 | 3 | ||||
-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 |
28 files changed, 179 insertions, 177 deletions
diff --git a/checker/check.ml b/checker/check.ml index 3194b2681..5b8507304 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -106,7 +106,8 @@ let check_one_lib admit (dir,m) = (Flags.if_verbose msgnl (str "Checking library: " ++ pr_dirpath dir); Safe_typing.import file md dig); - Flags.if_verbose msg(fnl()); + Flags.if_verbose pp (fnl()); + pp_flush (); register_loaded_library m (*************************************************************************) @@ -287,7 +288,7 @@ let name_clash_message dir mdir f = let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = - Flags.if_verbose msg (str"[intern "++str f++str" ..."); + Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); let (md,table,digest) = try let ch = with_magic_number_check raw_intern_library f in diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 2a2833caa..b3ede70bf 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -222,7 +222,7 @@ let constr_display csr = | Anonymous -> "Anonymous" in - msg (str (term_display csr) ++fnl ()) + Pp.pp (str (term_display csr) ++fnl ()); Pp.pp_flush () open Format;; diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 0a3466859..35621a5d7 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -327,6 +327,7 @@ let flush_all() = flush stderr; flush stdout; pp_flush() (* pretty printing functions WITH FLUSH *) let msg x = msg_with !std_ft x let msgnl x = msgnl_with !std_ft x +let msg_info x = msgnl x let msgerr x = msg_with !err_ft x let msgerrnl x = msgnl_with !err_ft x let msg_warning x = msg_warning_with !err_ft x diff --git a/lib/pp.mli b/lib/pp.mli index da37a1153..135343092 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -96,6 +96,9 @@ val msgnl_with : Format.formatter -> std_ppcmds -> unit (** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *) +(** These functions are low-level interace to printing and should not be used + in usual code. Consider using the [msg_*] function family instead. *) + val pp : std_ppcmds -> unit val ppnl : std_ppcmds -> unit val pperr : std_ppcmds -> unit @@ -104,19 +107,22 @@ val message : string -> unit (** = pPNL *) val pp_flush : unit -> unit val flush_all: unit -> unit -(** {6 Pretty-printing functions {% \emph{%}with flush{% }%} on [stdout] and [stderr]. } *) +(** {6 Sending messages to the user } *) -val msg : std_ppcmds -> unit -val msgnl : std_ppcmds -> unit -val msgerr : std_ppcmds -> unit -val msgerrnl : std_ppcmds -> unit +val msg_info : std_ppcmds -> unit val msg_warning : std_ppcmds -> unit - -(** Same specific display in emacs as warning, but without the "Warning:" **) val msg_debug : std_ppcmds -> unit val string_of_ppcmds : std_ppcmds -> string +(** {6 Deprecated functions} *) + +(** DEPRECATED. Do not use in newly written code. *) +val msg : std_ppcmds -> unit +val msgnl : std_ppcmds -> unit +val msgerr : std_ppcmds -> unit +val msgerrnl : std_ppcmds -> unit + (** {6 Location management. } *) type loc = Loc.t diff --git a/library/goptions.ml b/library/goptions.ml index 1a490c8ce..47aa401b6 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -106,7 +106,7 @@ module MakeTable = (fun c -> t := MySet.remove c !t)) let print_table table_name printer table = - msg (str table_name ++ + pp (str table_name ++ (hov 0 (if MySet.is_empty table then str "None" ++ fnl () else MySet.fold @@ -120,7 +120,7 @@ module MakeTable = method mem x = let y = A.encode x in let answer = MySet.mem y !t in - msg (A.member_message y answer ++ fnl ()) + msg_info (A.member_message y answer) method print = print_table A.title A.printer !t end @@ -354,11 +354,9 @@ let print_option_value key = let s = read () in match s with | BoolValue b -> - msg (str ("The "^name^" mode is "^(if b then "on" else "off")) ++ - fnl ()) + msg_info (str ("The "^name^" mode is "^(if b then "on" else "off"))) | _ -> - msg (str ("Current value of "^name^" is ") ++ - msg_option_value (name,s) ++ fnl ()) + msg_info (str ("Current value of "^name^" is ") ++ msg_option_value (name, s)) let get_tables () = @@ -380,27 +378,26 @@ let print_tables () = if depr then msg ++ str " [DEPRECATED]" ++ fnl () else msg ++ fnl () in - msg - (str "Synchronous options:" ++ fnl () ++ - OptionMap.fold - (fun key (name, depr, (sync,read,_,_,_)) p -> - if sync then p ++ print_option key name (read ()) depr - else p) - !value_tab (mt ()) ++ - str "Asynchronous options:" ++ fnl () ++ - OptionMap.fold - (fun key (name, depr, (sync,read,_,_,_)) p -> - if sync then p - else p ++ print_option key name (read ()) depr) - !value_tab (mt ()) ++ - str "Tables:" ++ fnl () ++ - List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) - !string_table (mt ()) ++ - List.fold_right - (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) - !ref_table (mt ()) ++ - fnl () - ) + str "Synchronous options:" ++ fnl () ++ + OptionMap.fold + (fun key (name, depr, (sync,read,_,_,_)) p -> + if sync then p ++ print_option key name (read ()) depr + else p) + !value_tab (mt ()) ++ + str "Asynchronous options:" ++ fnl () ++ + OptionMap.fold + (fun key (name, depr, (sync,read,_,_,_)) p -> + if sync then p + else p ++ print_option key name (read ()) depr) + !value_tab (mt ()) ++ + str "Tables:" ++ fnl () ++ + List.fold_right + (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + !string_table (mt ()) ++ + List.fold_right + (fun (nickkey,_) p -> p ++ str (" "^nickkey) ++ fnl ()) + !ref_table (mt ()) ++ + fnl () + diff --git a/library/goptions.mli b/library/goptions.mli index a90689dfc..29b6adb6e 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -164,6 +164,6 @@ val set_string_option_value : option_name -> string -> unit val print_option_value : option_name -> unit val get_tables : unit -> Interface.option_state OptionMap.t -val print_tables : unit -> unit +val print_tables : unit -> std_ppcmds val error_undeclared_key : option_name -> 'a diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 7434f5e8a..699f1f3df 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -696,14 +696,15 @@ type explanation = let check_disequalities state = let uf=state.uf in let rec check_aux = function - dis::q -> - debug (fun () -> msg - (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++ - pr_idx_term state dis.rhs ++ str " ... ")) (); - if find uf dis.lhs=find uf dis.rhs then - begin debug msgnl (str "Yes");Some dis end - else - begin debug msgnl (str "No");check_aux q end + | dis::q -> + let (info, ans) = + if find uf dis.lhs = find uf dis.rhs then (str "Yes", Some dis) + else (str "No", check_aux q) + in + let _ = debug (fun () -> msg_debug + (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++ + pr_idx_term state dis.rhs ++ str " ... " ++ info)) () in + ans | [] -> None in check_aux state.diseq diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 4438c5897..fe86e1ae1 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -99,7 +99,7 @@ END VERNAC COMMAND EXTEND PrintExtractionInline | [ "Print" "Extraction" "Inline" ] - -> [ print_extraction_inline () ] + -> [ msg_info (print_extraction_inline ()) ] END VERNAC COMMAND EXTEND ResetExtractionInline diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index ecedc9002..0efdbbb6b 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -606,7 +606,6 @@ let extraction_inline b l = let print_extraction_inline () = let (i,n)= !inline_table in let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in - msg (str "Extraction Inline:" ++ fnl () ++ Refset'.fold (fun r p -> diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 7505664a6..978760e8e 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -177,7 +177,7 @@ val find_custom_match : ml_branch array -> string val extraction_language : lang -> unit val extraction_inline : bool -> reference list -> unit -val print_extraction_inline : unit -> unit +val print_extraction_inline : unit -> Pp.std_ppcmds val reset_extraction_inline : unit -> unit val extract_constant_inline : bool -> reference -> string list -> string -> unit diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index d1fc8ef33..a169c2826 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -16,10 +16,10 @@ let observe strm = if do_observe () then Pp.msgnl strm else () -let observennl strm = +(*let observennl strm = if do_observe () then Pp.msg strm - else () + else ()*) type binder_type = diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b0897c61e..b463b6c27 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -55,10 +55,10 @@ let observe strm = then Pp.msgnl strm else () -let observennl strm = +(*let observennl strm = if do_observe () then begin Pp.msg strm;Pp.pp_flush () end - else () + else ()*) let do_observe_tac s tac g = diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index d772279f1..a1ab6cd30 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -472,7 +472,7 @@ and pp_atom= function | Atom n -> int n | f -> str "(" ++ hv 2 (pp_form f) ++ str ")" -let pr_form f = msg (pp_form f) +let pr_form f = pp_form f let pp_intmap map = let pp=ref (str "") in diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index 275e94cde..738f3f230 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -40,7 +40,7 @@ val success: state -> bool val pp: state -> Pp.std_ppcmds -val pr_form : form -> unit +val pr_form : form -> Pp.std_ppcmds val reset_info : unit -> unit diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 783aebafd..a095c545f 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -128,10 +128,10 @@ TACTIC EXTEND closed_term END ;; -TACTIC EXTEND echo +(* TACTIC EXTEND echo | [ "echo" constr(t) ] -> [ Pp.msg (Termops.print_constr t); Tacinterp.eval_tactic (TacId []) ] -END;; +END;;*) (* let closed_term_ast l = diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 221c46a92..cb588af2d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -89,7 +89,7 @@ let tclIDTAC gls = goal_goal_list gls (* the message printing identity tactic *) let tclIDTAC_MESSAGE s gls = - msg (hov 0 s); tclIDTAC gls + pp (hov 0 s); pp_flush (); tclIDTAC gls (* General failure tactic *) let tclFAIL_s s gls = errorlabstrm "Refiner.tclFAIL_s" (str s) diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index b23f361c7..d09c7f05a 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.ml @@ -60,7 +60,7 @@ let help () = let goal_com g tac = begin db_pr_goal g; - msg (str "Going to execute:" ++ fnl () ++ !prtac tac ++ fnl ()) + msgnl (str "Going to execute:" ++ fnl () ++ !prtac tac) end let skipped = ref 0 @@ -105,14 +105,14 @@ let run ini = for i=1 to 2 do print_char (Char.chr 8);print_char (Char.chr 13) done; - msg (str "Executed expressions: " ++ int !skipped ++ fnl() ++ fnl()) + msgnl (str "Executed expressions: " ++ int !skipped ++ fnl()) end; incr skipped (* Prints the prompt *) let rec prompt level = begin - msg (fnl () ++ str "TcDebug (" ++ int level ++ str ") > "); + pp (fnl () ++ str "TcDebug (" ++ int level ++ str ") > "); flush stdout; let exit () = skip:=0;skipped:=0;raise Sys.Break in let inst = try read_line () with End_of_file -> exit () in diff --git a/tactics/auto.ml b/tactics/auto.ml index 404516279..96cef72b4 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -411,6 +411,10 @@ module Hint_db = struct f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat); Constr_map.iter (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map + let fold f db accu = + let accu = f None (List.map (fun x -> snd (snd x)) db.hintdb_nopat) accu in + Constr_map.fold (fun k (l,l',_) -> f (Some k) (List.map snd (l@l'))) db.hintdb_map accu + let transparent_state db = db.hintdb_state let set_transparent_state db st = @@ -921,7 +925,6 @@ let pr_hint_list_for_head c = let pr_hint_ref ref = pr_hint_list_for_head ref (* Print all hints associated to head id in any database *) -let print_hint_ref ref = ppnl(pr_hint_ref ref) let pr_hint_term cl = try @@ -949,53 +952,51 @@ let pr_hint_term cl = let error_no_such_hint_database x = error ("No such Hint database: "^x^".") -let print_hint_term cl = ppnl (pr_hint_term cl) - (* print all hints that apply to the concl of the current goal *) -let print_applicable_hint () = +let pr_applicable_hint () = let pts = get_pftreestate () in let glss = Proof.V82.subgoals pts in match glss.Evd.it with | [] -> Errors.error "No focused goal." | g::_ -> let gl = { Evd.it = g; sigma = glss.Evd.sigma } in - print_hint_term (pf_concl gl) + pr_hint_term (pf_concl gl) (* displays the whole hint database db *) -let print_hint_db db = +let pr_hint_db db = + let content = + let fold head hintlist accu = + let goal_descr = match head with + | None -> str "For any goal" + | Some head -> str "For " ++ pr_global head + in + let hints = pr_hint_list (List.map (fun x -> (0, x)) hintlist) in + let hint_descr = hov 0 (goal_descr ++ str " -> " ++ hints) in + accu ++ hint_descr + in + Hint_db.fold fold db (mt ()) + in let (ids, csts) = Hint_db.transparent_state db in - msgnl (hov 0 - ((if Hint_db.use_dn db then str"Discriminated database" - else str"Non-discriminated database"))); - msgnl (hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids)); - msgnl (hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts)); - msgnl (hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db))); - Hint_db.iter - (fun head hintlist -> - match head with - | Some head -> - msg (hov 0 - (str "For " ++ pr_global head ++ str " -> " ++ - pr_hint_list (List.map (fun x -> (0,x)) hintlist))) - | None -> - msg (hov 0 - (str "For any goal -> " ++ - pr_hint_list (List.map (fun x -> (0, x)) hintlist)))) - db - -let print_hint_db_by_name dbname = + hov 0 + ((if Hint_db.use_dn db then str"Discriminated database" + else str"Non-discriminated database")) ++ fnl () ++ + hov 2 (str"Unfoldable variable definitions: " ++ pr_idpred ids) ++ fnl () ++ + hov 2 (str"Unfoldable constant definitions: " ++ pr_cpred csts) ++ fnl () ++ + hov 2 (str"Cut: " ++ pp_hints_path (Hint_db.cut db)) ++ fnl () ++ + content + +let pr_hint_db_by_name dbname = try - let db = searchtable_map dbname in print_hint_db db + let db = searchtable_map dbname in pr_hint_db db with Not_found -> error_no_such_hint_database dbname (* displays all the hints of all databases *) -let print_searchtable () = - Hintdbmap.iter - (fun name db -> - msg (str "In the database " ++ str name ++ str ":" ++ fnl ()); - print_hint_db db) - !searchtable +let pr_searchtable () = + let fold name db accu = + str "In the database " ++ str name ++ str ":" ++ fnl () ++ pr_hint_db db + in + Hintdbmap.fold fold !searchtable (mt ()) (**************************************************************************) (* Automatic tactics *) diff --git a/tactics/auto.mli b/tactics/auto.mli index 67e4dac97..792900984 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -19,6 +19,7 @@ open Globnames open Vernacexpr open Mod_subst open Misctypes +open Pp (** Auto and related automation tactics *) @@ -124,15 +125,11 @@ val add_hints : locality_flag -> hint_db_name list -> hints_entry -> unit val prepare_hint : env -> open_constr -> constr -val print_searchtable : unit -> unit - -val print_applicable_hint : unit -> unit - -val print_hint_ref : global_reference -> unit - -val print_hint_db_by_name : hint_db_name -> unit - -val print_hint_db : Hint_db.t -> unit +val pr_searchtable : unit -> std_ppcmds +val pr_applicable_hint : unit -> std_ppcmds +val pr_hint_ref : global_reference -> std_ppcmds +val pr_hint_db_by_name : hint_db_name -> std_ppcmds +val pr_hint_db : Hint_db.t -> std_ppcmds (** [make_exact_entry pri (c, ctyp)]. [c] is the term given as an exact proof to solve the goal; diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 82b08289d..cdb192ffa 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -779,6 +779,5 @@ END VERNAC COMMAND EXTEND GrabEvars [ "Grab" "Existential" "Variables" ] -> [ let p = Proof_global.give_me_the_proof () in - Proof.V82.grab_evars p; - Flags.if_verbose (fun () -> Pp.msg (Printer.pr_open_subgoals ())) () ] + Proof.V82.grab_evars p ] END diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 16eb595ea..665ab5b39 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1742,8 +1742,7 @@ let add_morphism_infer glob m n = glob (ConstRef cst)); declare_projection n instance_id (ConstRef cst) | _ -> assert false); - Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) (); - Flags.if_verbose (fun x -> msg (Printer.pr_open_subgoals x)) () + Pfedit.by (Tacinterp.interp <:tactic< Coq.Classes.SetoidTactics.add_morphism_tactic>>)) () let add_morphism glob binders m s n = init_setoid (); 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 () |