From: Claudio Sacerdoti Coen Date: Fri, 2 Nov 2007 16:02:52 +0000 (+0000) Subject: Added an hook useful in many situations. X-Git-Tag: 0.4.95@7852~68 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f38af523cd051d4c1d0dceeb59ce2fbbfc87367d;p=helm.git Added an hook useful in many situations. --- diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 9b08ba6dc..c71c24f11 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -25,6 +25,10 @@ (* $Id$ *) +let object_declaration_hook = ref (fun _ _ -> ());; +let set_object_declaration_hook f = + object_declaration_hook := f + exception AlreadyDefined of UriManager.uri let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29 @@ -160,6 +164,10 @@ let add_single_obj uri obj refinement_toolkit = try (*3*) let new_stuff = save_object_to_disk uri obj ugraph univlist in + (* EXPERIMENTAL: pretty print the object in natural language *) + (try !object_declaration_hook uri obj + with exc -> + prerr_endline "Error: object_declaration_hook failed"); try HLog.message (Printf.sprintf "%s defined" (UriManager.string_of_uri uri)) diff --git a/components/library/librarySync.mli b/components/library/librarySync.mli index 980e4724a..d8e432e75 100644 --- a/components/library/librarySync.mli +++ b/components/library/librarySync.mli @@ -25,6 +25,8 @@ exception AlreadyDefined of UriManager.uri +val set_object_declaration_hook : (UriManager.uri -> Cic.obj -> unit) -> unit + (* this is a pointer to the function which builds the inversion principle *) val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) list) ref