X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=c71c24f11c109f46458ceb7c030a8e374b5f0bcf;hb=f38af523cd051d4c1d0dceeb59ce2fbbfc87367d;hp=9b08ba6dc5a662dcc0f6dd2865f686ad7374a4f9;hpb=de36ba96a7d328655885e7bf6fed08cf06faecb6;p=helm.git

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))