From 5c19fc553c94e2b96e8e2a22a97a58a4f1d6b152 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 May 2006 08:22:10 +0000 Subject: [PATCH] better exception --- helm/software/components/cic/libraryObjects.ml | 14 +++++++------- helm/software/components/cic/libraryObjects.mli | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/helm/software/components/cic/libraryObjects.ml b/helm/software/components/cic/libraryObjects.ml index e1c9e1396..223b24edd 100644 --- a/helm/software/components/cic/libraryObjects.ml +++ b/helm/software/components/cic/libraryObjects.ml @@ -53,7 +53,7 @@ let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI] (**** SET_DEFAULT ****) -exception NotRecognized;; +exception NotRecognized of string;; (* insert an element in front of the list, removing from the list all the previous elements with the same key associated *) @@ -76,7 +76,7 @@ let set_default what l = false_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref | "absurd",[absurd_URI] -> absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref - | _,_ -> raise NotRecognized + | _,_ -> raise (NotRecognized what) let reset_defaults () = eq_URIs_ref := default_eq_URIs; @@ -96,7 +96,7 @@ let is_eq_ind_URI uri = let is_eq_ind_r_URI uri = List.exists (fun (_,_,_,_,eq_ind_r) -> UriManager.eq eq_ind_r uri) !eq_URIs_ref -let is_trans_eq_URI uri = +let is_trans_eq_URI uri = List.exists (fun (_,_,trans_eq,_,_) -> UriManager.eq trans_eq uri) !eq_URIs_ref let is_sym_eq_URI uri = List.exists (fun (_,sym_eq,_,_,_) -> UriManager.eq sym_eq uri) !eq_URIs_ref @@ -104,22 +104,22 @@ let is_sym_eq_URI uri = let sym_eq_URI ~eq:uri = try let _,x,_,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise NotRecognized + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let trans_eq_URI ~eq:uri = try let _,_,x,_,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise NotRecognized + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_ind_URI ~eq:uri = try let _,_,_,x,_ = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise NotRecognized + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let eq_ind_r_URI ~eq:uri = try let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x - with Not_found -> raise NotRecognized + with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri)) let true_URI () = List.hd !true_URIs_ref let false_URI () = List.hd !false_URIs_ref diff --git a/helm/software/components/cic/libraryObjects.mli b/helm/software/components/cic/libraryObjects.mli index db15cdff8..1fa0dcc83 100644 --- a/helm/software/components/cic/libraryObjects.mli +++ b/helm/software/components/cic/libraryObjects.mli @@ -34,7 +34,7 @@ val is_eq_ind_r_URI : UriManager.uri -> bool val is_trans_eq_URI : UriManager.uri -> bool val is_sym_eq_URI : UriManager.uri -> bool -exception NotRecognized;; +exception NotRecognized of string;; val eq_ind_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri -- 2.39.2