Added an hook useful in many situations.

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 9b08ba6dc5a662dcc0f6dd2865f686ad7374a4f9..c71c24f11c109f46458ceb7c030a8e374b5f0bcf 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/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/helm/software/components/library/librarySync.mli b/helm/software/components/library/librarySync.mli
index 980e4724a990de49ba049a97c7b6bcf3ca2c3f5c..d8e432e75b9035888478ed3d1277dbe730344dcc 100644 (file)
--- a/helm/software/components/library/librarySync.mli
+++ b/helm/software/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