From f38af523cd051d4c1d0dceeb59ce2fbbfc87367d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Nov 2007 16:02:52 +0000 Subject: [PATCH] Added an hook useful in many situations. --- components/library/librarySync.ml | 8 ++++++++ components/library/librarySync.mli | 2 ++ 2 files changed, 10 insertions(+) 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 -- 2.39.2