From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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