diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-06-29 11:48:49 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-06-29 11:48:49 +0200 |
commit | 58b6784fee71a16719bc4f268dc42830c06a5c63 (patch) | |
tree | a9a3859746d2ff97f8c0b8106c96b49f9122a1b7 /toplevel/vernacentries.ml | |
parent | 0e07e69dae3f3f4a99f824533f54a3991aacac6a (diff) | |
parent | dd8d2a1d017d20635f943af205dcb0127a992a59 (diff) |
Merge branch 'warnings' into trunk
Was PR#213: New warnings machinery
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r-- | toplevel/vernacentries.ml | 39 |
1 files changed, 31 insertions, 8 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 82fe9751e..65aa46bc1 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -896,7 +896,11 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (expand path) - with Sys_error err -> Feedback.msg_warning (str "Cd failed: " ++ str err) + with Sys_error err -> + (* Cd is typically used to control the output directory of + extraction. A failed Cd could lead to overwriting .ml files + so we make it an error. *) + Errors.error ("Cd failed: " ^ err) end; if_verbose Feedback.msg_info (str (Sys.getcwd())) @@ -943,6 +947,16 @@ let vernac_declare_implicits locality r l = Impargs.declare_manual_implicits local (smart_global r) ~enriching:false (List.map (List.map (fun (ex,b,f) -> ex, (b,true,f))) imps) +let warn_arguments_assert = + CWarnings.create ~name:"arguments-assert" ~category:"vernacular" + (fun sr -> + strbrk "This command is just asserting the number and names of arguments of " ++ + pr_global sr ++ strbrk". If this is what you want add " ++ + strbrk "': assert' to silence the warning. If you want " ++ + strbrk "to clear implicit arguments add ': clear implicits'. " ++ + strbrk "If you want to clear notation scopes add ': clear scopes'") + + let vernac_declare_arguments locality r l nargs flags = let extra_scope_flag = List.mem `ExtraScopes flags in let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in @@ -1071,7 +1085,7 @@ let vernac_declare_arguments locality r l nargs flags = some_scopes_specified || some_simpl_flags_specified) && no_flags then - Feedback.msg_warning (strbrk "This command is just asserting the number and names of arguments of " ++ pr_global sr ++ strbrk". If this is what you want add ': assert' to silence the warning. If you want to clear implicit arguments add ': clear implicits'. If you want to clear notation scopes add ': clear scopes'") + warn_arguments_assert sr let default_env () = { @@ -1342,6 +1356,15 @@ let _ = optread = (fun () -> !Constrintern.parsing_explicit); optwrite = (fun b -> Constrintern.parsing_explicit := b) } +let _ = + declare_string_option + { optsync = true; + optdepr = false; + optname = "warnings display"; + optkey = ["Warnings"]; + optread = CWarnings.get_flags; + optwrite = CWarnings.set_flags } + let vernac_set_strategy locality l = let local = make_locality locality in let glob_ref r = @@ -1855,12 +1878,12 @@ let interp ?proof ~loc locality poly c = | VernacComments l -> if_verbose Feedback.msg_info (str "Comments ok\n") (* The STM should handle that, but LOAD bypasses the STM... *) - | VernacAbort id -> Feedback.msg_warning (str "VernacAbort not handled by Stm") - | VernacAbortAll -> Feedback.msg_warning (str "VernacAbortAll not handled by Stm") - | VernacRestart -> Feedback.msg_warning (str "VernacRestart not handled by Stm") - | VernacUndo _ -> Feedback.msg_warning (str "VernacUndo not handled by Stm") - | VernacUndoTo _ -> Feedback.msg_warning (str "VernacUndoTo not handled by Stm") - | VernacBacktrack _ -> Feedback.msg_warning (str "VernacBacktrack not handled by Stm") + | VernacAbort id -> Errors.errorlabstrm "" (str "Abort cannot be used through the Load command") + | VernacAbortAll -> Errors.errorlabstrm "" (str "AbortAll cannot be used through the Load command") + | VernacRestart -> Errors.errorlabstrm "" (str "Restart cannot be used through the Load command") + | VernacUndo _ -> Errors.errorlabstrm "" (str "Undo cannot be used through the Load command") + | VernacUndoTo _ -> Errors.errorlabstrm "" (str "UndoTo cannot be used through the Load command") + | VernacBacktrack _ -> Errors.errorlabstrm "" (str "Backtrack cannot be used through the Load command") (* Proof management *) | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false |