diff options
| -rw-r--r-- | interp/notation.ml | 4 | ||||
| -rw-r--r-- | lib/options.ml | 4 | ||||
| -rw-r--r-- | lib/options.mli | 3 | ||||
| -rw-r--r-- | lib/pp.ml4 | 60 | ||||
| -rw-r--r-- | lib/pp.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 10 | ||||
| -rw-r--r-- | parsing/g_natsyntax.ml | 11 | ||||
| -rw-r--r-- | tactics/setoid_replace.ml | 62 | ||||
| -rw-r--r-- | toplevel/command.ml | 5 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 1 |
11 files changed, 90 insertions, 74 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 3989f00727..614c87a0cf 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -299,8 +299,8 @@ let level_of_notation ntn = let declare_notation_interpretation ntn scopt pat df = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in - if Gmap.mem ntn sc.notations && Options.is_verbose () then - msg_warning (str ("Notation "^ntn^" was already used"^ + if Gmap.mem ntn sc.notations then + Options.if_warn msg_warning (str ("Notation "^ntn^" was already used"^ (if scopt = None then "" else " in scope "^scope))); let sc = { sc with notations = Gmap.add ntn (pat,df) sc.notations } in scope_map := Gmap.add scope sc !scope_map; diff --git a/lib/options.ml b/lib/options.ml index e59a19bbb7..848b08611c 100644 --- a/lib/options.ml +++ b/lib/options.ml @@ -63,6 +63,10 @@ let if_verbose f x = if not !silent then f x let hash_cons_proofs = ref true +let warn = ref true +let make_warn flag = warn := flag; () +let if_warn f x = if !warn then f x + (* The number of printed hypothesis in a goal *) let print_hyps_limit = ref (None : int option) diff --git a/lib/options.mli b/lib/options.mli index 7fa55e6367..73962735da 100644 --- a/lib/options.mli +++ b/lib/options.mli @@ -40,6 +40,9 @@ val silently : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit +val make_warn : bool -> unit +val if_warn : ('a -> unit) -> 'a -> unit + val hash_cons_proofs : bool ref (* Temporary activate an option ('c must be an atomic type) *) diff --git a/lib/pp.ml4 b/lib/pp.ml4 index 27ddae00c2..bfabb533ba 100644 --- a/lib/pp.ml4 +++ b/lib/pp.ml4 @@ -130,19 +130,15 @@ let align () = [< 'Ppcmd_print_break (0,0) >] let int n = str (string_of_int n) let real r = str (string_of_float r) let bool b = str (string_of_bool b) - -(* In new syntax only double quote char is escaped by repeating it *) -let rec escape_string s = - let rec escape_at s i = - if i<0 then s - else if s.[i] == '"' then - let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in - escape_at s' (i-1) - else escape_at s (i-1) in - escape_at s (String.length s - 1) - -let qstring s = str ("\""^escape_string s^"\"") -let qs = qstring +let strbrk s = + let rec aux p n = + if n < String.length s then + if s.[n] = ' ' then + if p=n then [< spc (); aux (n+1) (n+1) >] + else [< str (String.sub s p (n-p)); spc (); aux (n+1) (n+1) >] + else aux p (n+1) + else if p=n then [< >] else [< str (String.sub s p (n-p)) >] + in aux 0 0 (* boxing commands *) let h n s = [< 'Ppcmd_box(Pp_hbox n,s) >] @@ -162,6 +158,20 @@ let tclose () = [< 'Ppcmd_close_tbox >] let (++) = Stream.iapp +(* In new syntax only double quote char is escaped by repeating it *) +let rec escape_string s = + let rec escape_at s i = + if i<0 then s + else if s.[i] == '"' then + let s' = String.sub s 0 i^"\""^String.sub s i (String.length s - i) in + escape_at s' (i-1) + else escape_at s (i-1) in + escape_at s (String.length s - 1) + +let qstring s = str ("\""^escape_string s^"\"") +let qs = qstring +let quote s = h 0 (str "\"" ++ s ++ str "\"") + (* This flag tells if the last printed comment ends with a newline, to avoid empty lines *) let com_eol = ref false @@ -252,11 +262,13 @@ let emacs_warning_start_string = String.make 1 (Char.chr 254) let emacs_warning_end_string = String.make 1 (Char.chr 255) let warnstart() = - if not !print_emacs then str "" else str emacs_warning_start_string + if not !print_emacs then mt() else str emacs_warning_start_string let warnend() = - if not !print_emacs then str "" else str emacs_warning_end_string - + if not !print_emacs then mt() else str emacs_warning_end_string + +let warnbody strm = + [< warnstart() ; hov 0 (str "Warning: " ++ strm) ; warnend() >] (* pretty printing functions WITHOUT FLUSH *) let pp_with ft strm = @@ -265,21 +277,17 @@ let pp_with ft strm = let ppnl_with ft strm = pp_dirs ft [< 'Ppdir_ppcmds [< strm ; 'Ppcmd_force_newline >] >] - -let default_warn_with ft pps = - ppnl_with ft [< warnstart() ; str "Warning: " ; pps ; warnend() >] +let default_warn_with ft strm = ppnl_with ft (warnbody strm) let pp_warn_with = ref default_warn_with let set_warning_function pp_warn = pp_warn_with := pp_warn -let warn_with ft pps = !pp_warn_with ft pps +let warn_with ft strm = !pp_warn_with ft strm let warning_with ft string = warn_with ft (str string) -let pp_flush_with ft = - Format.pp_print_flush ft - +let pp_flush_with ft = Format.pp_print_flush ft (* pretty printing functions WITH FLUSH *) let msg_with ft strm = @@ -288,10 +296,8 @@ let msg_with ft strm = let msgnl_with ft strm = pp_dirs ft [< 'Ppdir_ppcmds strm ; 'Ppdir_print_newline >] -let msg_warning_with ft strm= - pp_dirs ft [< 'Ppdir_ppcmds [< warnstart() ; str "Warning: "; strm ; warnend() >]; - 'Ppdir_print_newline >] - +let msg_warning_with ft strm = + msgnl_with ft (warnbody strm) (* pretty printing functions WITHOUT FLUSH *) let pp x = pp_with !std_ft x diff --git a/lib/pp.mli b/lib/pp.mli index a0177d7410..8a5aee7993 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -53,6 +53,8 @@ val real : float -> std_ppcmds val bool : bool -> std_ppcmds val qstring : string -> std_ppcmds val qs : string -> std_ppcmds +val quote : std_ppcmds -> std_ppcmds +val strbrk : string -> std_ppcmds (*s Boxing commands. *) diff --git a/library/library.ml b/library/library.ml index 7e93db65e4..70eac95aec 100644 --- a/library/library.ml +++ b/library/library.ml @@ -86,10 +86,10 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> Nameops.default_root_prefix then - (Options.if_verbose warning (phys_path^" was previously bound to " - ^(string_of_dirpath dir) - ^("\nIt is remapped to "^(string_of_dirpath coq_path))); - flush_all ()); + Options.if_warn msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath dir ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path); remove_load_path phys_path; load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) end @@ -614,7 +614,7 @@ let save_library_to dir f = let di = Digest.file f' in System.marshal_out ch di; close_out ch - with e -> (warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e) + with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e (************************************************************************) (*s Display the memory use of a library. *) diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml index 448c8dc2ca..8b8761cb18 100644 --- a/parsing/g_natsyntax.ml +++ b/parsing/g_natsyntax.ml @@ -32,11 +32,12 @@ open Names let nat_of_int dloc n = if is_pos_or_zero n then begin - if less_than (of_string "5000") n & Options.is_verbose () then begin - warning ("You may experience stack overflow and segmentation fault\ - \nwhile parsing numbers in nat greater than 5000"); - flush_all () - end; + if less_than (of_string "5000") n then + Options.if_warn msg_warning + (strbrk "Stack overflow or segmentation fault happens when " ++ + strbrk "working with large numbers in nat (observed threshold " ++ + strbrk "may vary from 5000 to 70000 depending on your system " ++ + strbrk "limits and on the command executed)."); let ref_O = RRef (dloc, glob_O) in let ref_S = RRef (dloc, glob_S) in let rec mk_nat acc n = diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 99cf25779a..500a7f40d3 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -257,8 +257,8 @@ let default_relation_for_carrier ?(filter=fun _ -> true) a = [] -> Leibniz (Some a) | relation::tl -> if tl <> [] then - ppnl - (str "Warning: There are several relations on the carrier \"" ++ + Options.if_warn msg_warning + (str "There are several relations on the carrier \"" ++ pr_lconstr a ++ str "\". The relation " ++ prrelation relation ++ str " is chosen.") ; Relation relation @@ -345,29 +345,29 @@ let (relation_to_obj, obj_to_relation)= match th.rel_sym with None -> old_relation.rel_sym | Some t -> Some t} in - ppnl - (str "Warning: The relation " ++ prrelation th' ++ - str " is redeclared. The new declaration" ++ + Options.if_warn msg_warning + (strbrk "The relation " ++ prrelation th' ++ + strbrk " is redeclared. The new declaration" ++ (match th'.rel_refl with - None -> str "" - | Some t -> str " (reflevity proved by " ++ pr_lconstr t) ++ + None -> mt () + | Some t -> strbrk " (reflexivity proved by " ++ pr_lconstr t) ++ (match th'.rel_sym with - None -> str "" + None -> mt () | Some t -> - (if th'.rel_refl = None then str " (" else str " and ") ++ - str "symmetry proved by " ++ pr_lconstr t) ++ + (if th'.rel_refl = None then strbrk " (" else strbrk " and ") + ++ strbrk "symmetry proved by " ++ pr_lconstr t) ++ (if th'.rel_refl <> None && th'.rel_sym <> None then str ")" else str "") ++ - str " replaces the old declaration" ++ + strbrk " replaces the old declaration" ++ (match old_relation.rel_refl with None -> str "" - | Some t -> str " (reflevity proved by " ++ pr_lconstr t) ++ + | Some t -> strbrk " (reflexivity proved by " ++ pr_lconstr t) ++ (match old_relation.rel_sym with None -> str "" | Some t -> (if old_relation.rel_refl = None then - str " (" else str " and ") ++ - str "symmetry proved by " ++ pr_lconstr t) ++ + strbrk " (" else strbrk " and ") ++ + strbrk "symmetry proved by " ++ pr_lconstr t) ++ (if old_relation.rel_refl <> None && old_relation.rel_sym <> None then str ")" else str "") ++ str "."); @@ -410,12 +410,12 @@ let morphism_table_add (m,c) = List.find (function mor -> mor.args = c.args && mor.output = c.output) old in - ppnl - (str "Warning: The morphism " ++ prmorphism m old_morph ++ - str " is redeclared. " ++ - str "The new declaration whose compatibility is proved by " ++ - pr_lconstr c.lem ++ str " replaces the old declaration whose" ++ - str " compatibility was proved by " ++ + Options.if_warn msg_warning + (strbrk "The morphism " ++ prmorphism m old_morph ++ + strbrk " is redeclared. " ++ + strbrk "The new declaration whose compatibility is proved by " ++ + pr_lconstr c.lem ++ strbrk " replaces the old declaration whose" ++ + strbrk " compatibility was proved by " ++ pr_lconstr old_morph.lem ++ str ".") with Not_found -> morphism_table := Gmap.add m (c::old) !morphism_table @@ -425,10 +425,10 @@ let default_morphism ?(filter=fun _ -> true) m = [] -> raise Not_found | m1::ml -> if ml <> [] then - ppnl - (str "Warning: There are several morphisms associated to \"" ++ - pr_lconstr m ++ str"\". Morphism " ++ prmorphism m m1 ++ - str " is randomly chosen."); + Options.if_warn msg_warning + (strbrk "There are several morphisms associated to \"" ++ + pr_lconstr m ++ strbrk "\". Morphism " ++ prmorphism m m1 ++ + strbrk " is randomly chosen."); relation_morphism_of_constr_morphism m1 let subst_morph subst morph = @@ -1573,16 +1573,16 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction = (fun i (_,_,mc) -> pr_new_goals i mc) res) | [he] -> he | he::_ -> - ppnl - (str "Warning: The application of the tactic is subject to one of " ++ - str "the \nfollowing set of side conditions that the user needs " ++ - str "to prove:" ++ + Options.if_warn msg_warning + (strbrk "The application of the tactic is subject to one of " ++ + strbrk "the following set of side conditions that the user needs " ++ + strbrk "to prove:" ++ pr_fnl () ++ prlist_with_sepi pr_fnl (fun i (_,_,mc) -> pr_new_goals i mc) res' ++ pr_fnl () ++ - str "The first set is randomly chosen. Use the syntax " ++ - str "\"setoid_rewrite ... generate side conditions ...\" to choose " ++ - str "a different set.") ; + strbrk "The first set is randomly chosen. Use the syntax " ++ + strbrk "\"setoid_rewrite ... generate side conditions ...\" to choose " ++ + strbrk "a different set.") ; he let cic_morphism_context_list_of_list hole_relation hole_direction out_direction diff --git a/toplevel/command.ml b/toplevel/command.ml index d9c91808f7..739a7b47f7 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -144,8 +144,9 @@ let declare_definition ident (local,boxed,dok) bl red_option c typopt hook = let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in definition_message ident; if Pfedit.refining () then - msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ - str" is not visible from current goals"); + Options.if_verbose msg_warning + (str"Local definition " ++ pr_id ident ++ + str" is not visible from current goals"); VarRef ident | (Global|Local) -> declare_global_definition ident ce' local in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 3560bea4ff..305685cc7b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -29,8 +29,6 @@ open Printer open Rawterm open Evd -let quote s = h 0 (str "\"" ++ s ++ str "\"") - let pr_lconstr c = quote (pr_lconstr c) let pr_lconstr_env e c = quote (pr_lconstr_env e c) let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 4090748b3b..eec73e3900 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -174,6 +174,7 @@ and vernac interpfun input = vernac_com interpfun (parse_phrase input) and read_vernac_file verbosely s = + Options.make_warn verbosely; let interpfun = if verbosely then Vernacentries.interp |