From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 21 Jan 2008 17:30:35 +0000 (+0000)
Subject: Hack for code extraction re-linked, but disactivated.
X-Git-Tag: make_still_working~5659
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=156e9d172f3fd2fd7f2d5f0f88c8662c2c0fd796;p=helm.git

Hack for code extraction re-linked, but disactivated.
---

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index 83e833ebe..fc64479f1 100644
--- 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:[]