Bertrand's conjecture (weak), some work in progress

[helm.git] / helm / software / matita / matitacLib.ml

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 83e833ebe2e26c8e083f22b903cc9b9726a6a2fd..fc64479f12fd8fce2e896a628028cf7c9a597b05 100644 (file)
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -109,12 +109,28 @@ let get_include_paths options =
     include_paths
 ;;
 
+let activate_extraction baseuri fname =
+ if false then
+  let mangled_baseuri =
+   let baseuri = String.sub baseuri 5 (String.length baseuri - 5) in
+     let baseuri = Pcre.replace ~pat:"/" ~templ:"_" baseuri in
+      String.uncapitalize baseuri in
+  let f =
+    open_out
+     (Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
+   LibrarySync.set_object_declaration_hook
+    (fun _ obj ->
+      output_string f (CicExportation.ppobj baseuri obj);
+      flush f);
+;;
+
 let compile options fname =
   let matita_debug = Helm_registry.get_bool "matita.debug" in
   let include_paths = get_include_paths options in
   let root,baseuri,fname,_tgt = 
     Librarian.baseuri_of_script ~include_paths fname in
   if Http_getter_storage.is_read_only baseuri then assert false;
+  activate_extraction baseuri fname ;
   let grafite_status = GrafiteSync.init baseuri in
   let lexicon_status = 
     CicNotation2.load_notation ~include_paths:[]