Added an hook useful in many situations.

[helm.git] / components / library / librarySync.ml

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 9b08ba6dc5a662dcc0f6dd2865f686ad7374a4f9..c71c24f11c109f46458ceb7c030a8e374b5f0bcf 100644 (file)
--- 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))