From de038270f72214b169d056642eb7144a79e6f126 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 7 Jul 2016 04:56:24 +0200 Subject: Unify location handling of error functions. In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier. --- stm/lemmas.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index fb2f0351d2..4552ba8c68 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -222,7 +222,7 @@ let compute_proof_name locality = function if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then - user_err_loc (loc,"",pr_id id ++ str " already exists."); + user_err ~loc "" (pr_id id ++ str " already exists."); id, pl | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None @@ -331,7 +331,7 @@ let get_proof proof do_guard hook opacity = let check_exist = List.iter (fun (loc,id) -> if not (Nametab.exists_cci (Lib.make_path id)) then - user_err_loc (loc,"",pr_id id ++ str " does not exist.") + user_err ~loc "" (pr_id id ++ str " does not exist.") ) let universe_proof_terminator compute_guard hook = -- cgit v1.2.3 From 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 01:58:04 +0200 Subject: Remove errorlabstrm in favor of user_err As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch. --- stm/stm.ml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'stm') diff --git a/stm/stm.ml b/stm/stm.ml index 9f86597dce..ff4688480d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1038,7 +1038,7 @@ end = struct (* {{{ *) | _ -> VtUnknown, VtNow with | Not_found -> - CErrors.errorlabstrm "undo_vernac_classifier" + CErrors.user_err "undo_vernac_classifier" (str "Cannot undo") end (* }}} *) @@ -1106,7 +1106,7 @@ let proof_block_delimiters = ref [] let register_proof_block_delimiter name static dynamic = if List.mem_assoc name !proof_block_delimiters then - CErrors.errorlabstrm "STM" (str "Duplicate block delimiter " ++ str name); + CErrors.user_err "STM" (str "Duplicate block delimiter " ++ str name); proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters let mk_doc_node id = function @@ -1141,7 +1141,7 @@ let detect_proof_block id name = VCS.create_proof_block decl name end with Not_found -> - CErrors.errorlabstrm "STM" + CErrors.user_err "STM" (str "Unknown proof block delimiter " ++ str name) ) (****************************** THE SCHEDULER *********************************) @@ -1706,7 +1706,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) Evd.(evar_context g)) then - CErrors.errorlabstrm "STM" (strbrk("the par: goal selector supports ground "^ + CErrors.user_err "STM" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin let (i, ast) = r_ast in @@ -1719,7 +1719,7 @@ end = struct (* {{{ *) let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then RespBuiltSubProof (t, Evd.evar_universe_context sigma) - else CErrors.errorlabstrm "STM" (str"The solution is not ground") + else CErrors.user_err "STM" (str"The solution is not ground") end) () with e when CErrors.noncritical e -> RespError (CErrors.print e) @@ -2056,7 +2056,7 @@ let known_state ?(redefine_qed=false) ~cache id = | _ -> assert false end with Not_found -> - CErrors.errorlabstrm "STM" + CErrors.user_err "STM" (str "Unknown proof block delimiter " ++ str name) in @@ -2405,7 +2405,7 @@ let handle_failure (e, info) vcs tty = let snapshot_vio ldir long_f_dot_vo = finish (); if List.length (VCS.branches ()) > 1 then - CErrors.errorlabstrm "stm" (str"Cannot dump a vio with open proofs"); + CErrors.user_err "stm" (str"Cannot dump a vio with open proofs"); Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo (Global.opaque_tables ()) -- cgit v1.2.3 From fc579fdc83b751a44a18d2373e86ab38806e7306 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 19 Aug 2016 02:35:47 +0200 Subject: Make the user_err header an optional parameter. Suggested by @ppedrot --- stm/lemmas.ml | 4 ++-- stm/stm.ml | 14 +++++++------- 2 files changed, 9 insertions(+), 9 deletions(-) (limited to 'stm') diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 4552ba8c68..b08296fb94 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -222,7 +222,7 @@ let compute_proof_name locality = function if Nametab.exists_cci (Lib.make_path id) || is_section_variable id || locality == Global && Nametab.exists_cci (Lib.make_path_except_section id) then - user_err ~loc "" (pr_id id ++ str " already exists."); + user_err ~loc (pr_id id ++ str " already exists."); id, pl | None -> next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None @@ -331,7 +331,7 @@ let get_proof proof do_guard hook opacity = let check_exist = List.iter (fun (loc,id) -> if not (Nametab.exists_cci (Lib.make_path id)) then - user_err ~loc "" (pr_id id ++ str " does not exist.") + user_err ~loc (pr_id id ++ str " does not exist.") ) let universe_proof_terminator compute_guard hook = diff --git a/stm/stm.ml b/stm/stm.ml index ff4688480d..7c5a3bc6a7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1038,7 +1038,7 @@ end = struct (* {{{ *) | _ -> VtUnknown, VtNow with | Not_found -> - CErrors.user_err "undo_vernac_classifier" + CErrors.user_err ~hdr:"undo_vernac_classifier" (str "Cannot undo") end (* }}} *) @@ -1106,7 +1106,7 @@ let proof_block_delimiters = ref [] let register_proof_block_delimiter name static dynamic = if List.mem_assoc name !proof_block_delimiters then - CErrors.user_err "STM" (str "Duplicate block delimiter " ++ str name); + CErrors.user_err ~hdr:"STM" (str "Duplicate block delimiter " ++ str name); proof_block_delimiters := (name, (static,dynamic)) :: !proof_block_delimiters let mk_doc_node id = function @@ -1141,7 +1141,7 @@ let detect_proof_block id name = VCS.create_proof_block decl name end with Not_found -> - CErrors.user_err "STM" + CErrors.user_err ~hdr:"STM" (str "Unknown proof block delimiter " ++ str name) ) (****************************** THE SCHEDULER *********************************) @@ -1706,7 +1706,7 @@ end = struct (* {{{ *) List.for_all (Context.Named.Declaration.for_all (Evarutil.is_ground_term sigma0)) Evd.(evar_context g)) then - CErrors.user_err "STM" (strbrk("the par: goal selector supports ground "^ + CErrors.user_err ~hdr:"STM" (strbrk("the par: goal selector supports ground "^ "goals only")) else begin let (i, ast) = r_ast in @@ -1719,7 +1719,7 @@ end = struct (* {{{ *) let t = Evarutil.nf_evar sigma t in if Evarutil.is_ground_term sigma t then RespBuiltSubProof (t, Evd.evar_universe_context sigma) - else CErrors.user_err "STM" (str"The solution is not ground") + else CErrors.user_err ~hdr:"STM" (str"The solution is not ground") end) () with e when CErrors.noncritical e -> RespError (CErrors.print e) @@ -2056,7 +2056,7 @@ let known_state ?(redefine_qed=false) ~cache id = | _ -> assert false end with Not_found -> - CErrors.user_err "STM" + CErrors.user_err ~hdr:"STM" (str "Unknown proof block delimiter " ++ str name) in @@ -2405,7 +2405,7 @@ let handle_failure (e, info) vcs tty = let snapshot_vio ldir long_f_dot_vo = finish (); if List.length (VCS.branches ()) > 1 then - CErrors.user_err "stm" (str"Cannot dump a vio with open proofs"); + CErrors.user_err ~hdr:"stm" (str"Cannot dump a vio with open proofs"); Library.save_library_to ~todo:(dump_snapshot ()) ldir long_f_dot_vo (Global.opaque_tables ()) -- cgit v1.2.3